Kurt Goedel would have been 87 today, April 28.
Merry Goedelmas, everyone!

To prove: 0 = 1.
multiply both sides with 0:
 0 = 0.

OK.

Don’t laugh.  How often have you teachers seen
"proofs" that work by deducing a truth from a
conjecture?

Isn’t that the way actually science works?
Base predictions on hypotheses and check whether
the predictions bear out?

JWN

I’m looking for the proceedings of a symposium—I don’t konw for sure
whether a proceedings actually ever appeared. The symposium in
question is the 4th annual Frontiers in Computing: Symposium honoring
W. W. Bledose, held in Austin, Nov 1991. Can anyone help me with info
on how/where/if proceedings have appeared?

Thanks,
    Lawrence.

Inference forms such as

A & -A      |- B,
A       |- B v -B,
A       |- A v B,
B       |- A -> B,
etc.

are classically valid, but offend our intuitive sense of relevance. In
each case something is introduced in the consequent which (1) is not
mentioned in the antecedent, and (2) is miscellaneous in that anything
can be substituted for it without spoiling the validity of the
inference. Opionions differ as to exactly which cases offend
intuition, but the general problem is well recognised.

B.H.Slater [1] made an interesting use of the system of truth-trees or
semantic tableaux [see 2,3] in addressing this problem. Essentially
Slater pointed out that if we have an _open_ tree, then its initial
set of sentences entails "any disjunction each of whose disjuncts is
in some branch and for which each branch contains some disjunct".

Since contradictions in the initial set cause the tree to close, this
method will not establish entailents of the offending type A & -A |-
B. And since the construction of truth-trees does not introduce new
sentence-letters, such inferences as A |- A v B will also not be
supported. A limitation of the method as it stands is that the
consequents which can be read off are all in disjunctive form.

I would be interested in comments on this approach to relevance logic,
and in references to any other work attempting to use truth-trees in
this way.

Donald Peterson. Email: D.M.Peter…@cs.bham.ac.uk

References.
[1] B.H.Slater, ‘Direct Tableaux Proofs’, _Analysis_, 1981, pp 192-4.
[2] W. Hodges, _Logic_, 1977.
[3] R. Jeffrey, _Formal Logic: it’s Scope and Limits_, 2nd ed, 1981.

To Whom It May Concern:

The sender is thinking of organizing a conference.  My real interest
is in Quine’s "New Foundations" and related theories, which is a
rather limited area; I’m speculating that the topic of alternate set
theories (set theories other than ZFC and its usual extensions with
strong axioms of infinity) would draw more interest and would be
likely to attract people with some potential interest in NF in any
case.

The location of the conference would be Boise State University in
Boise, Idaho, so far as I know; I am open to alternatives, especially
if they come with some institutional support…  Any suggestions about
sources of funding would also be appreciated.  Anyone who would be
interested in participating in such an event within the next couple of
years is encouraged to respond by e-mail to hol…@math.idbsu.edu —
ditto for those who have suggestions about how to organize and fund
such an event.  

People who respond might mention what their favorite
alternate set theory (foundational theories based on functions rather
than sets are also relevant) happens to be.

–
The opinions expressed          |     –Sincerely,
above are not the "official"  |     M. Randall Holmes
opinions of any person          |     Math. Dept., Boise State Univ.
or institution.                 |     hol…@math.idbsu.edu

I have a question about ordered pairs.

I proved a result a while back (in Inductive Inference)
that IMPLIES the following result about
ordered pairs.  I’m just curious if it is already
known and with an easier proof.
(My guess is that it IS already known with an EASIER proof.)

DEF: A QUERY over [+,<] is a formula with number variables
that are all quanified over and ONE set variable that is
NOT quantified over.
We assume queries are in prenex normal form.

DEF: Two queries are equivalent if they are satisfied by
the same set of functions.

DEF: A query is i-E if it only has $\exists$ quantifiers
and there are exactly $i$ of them.

RESULT:
Let $i\in N$.
There does not exist a recursive procedure that will,
given a query in $(i+1)$-E form, convert it into an
equivalent query in $i$-E form.

                                        bill gasarch

Hi
I’m am  student who is preparing her thesis in Computer Science at the
University of Milan and I’m interested in theorem proving.
I’d like to have infomations about provers for First Order Logic (with
equality).

My email is inz…@ghost.dsi.unimi.it.

Thank you very much indeed!!!!!

                European Journal of Operational Research

        Special Issue on "Decision Technology: the Interface of
          Decision Support and Knowledge-based Systems"

                        CALL FOR PAPERS

In 1994 the European Journal of Operational Research is proposing to publish
a special issue on the theme of knowledge-based technology and its impact
upon the methodologies of decision analysis and decision-support. This issue
is intended to feature current developments in the practice of decision
modelling, knowledge-engineering and intelligent decision systems.
Applications are solicited from a wide range which may span for example,
strategic mapping to medical expert systems and interesting techniques
may range, for example, from influence diagrams, expert-critiquing systems,
interactive multicriteria aids through to object-oriented programming.
Within this broad interpretation, the emphasis should be upon the modelling
process and the way that technology is enhancing the human-computer
interaction capabilities.

Papers should be submitted in triplicate to either:

        Barry Silverman (ba…@seas.gwu.edu)
        Institute for Artificial Intelligence
        School of Engineering and Applied Science
        George Washington University
        2021 K St. NW, Suite 710
        Washignton, D.C. 20006
        U.S.A.

        Derek Bunn
        Decision Sciences
        London Business School
        Sussex Place
        Regent’s Park
        London NW1 4SA
        UK

Deadline for papers is July 1993.

-*—-
Where can I acquire information about the new round of
interactive theorem development systems?  In particular,
I am curious about systems such as:

    Coq
    Lego
    Alf

Mostly, I want an overview of how these systems work (from
the viewpoint of a user) and a description of the research
projects that produced them.  

If there is interest, I will summarize to the net.

Russell