sowa <>
Date: Tue, 15 Feb 94 06:21:18 EST
From: sowa <>
Message-id: <>
To:, interlingua@ISI.EDU
Subject: Propositions
Pat and Bob,

There are two extreme cases in the definition of propositions.
One extreme is the identification of propositions with sets of possible
worlds (or possible models).  This leads to the absurd result that
all theorems are equivalent to T.  Therefore, if you believe
2+2=4, then you must also believe every theorem of mathematics.

The other extreme is the identification of propositions with
sentences in some language.  This means that P&Q is a different
proposition from Q&P.

We would like to have some definition that is somewhere between
the two extremes, that is relatively language-independent, and
that makes a reasonable match with plausible intuitions.  I will
tell you my preferred definition, which I am strongly leaning towards,
but which I am willing to modify if someone can give me good reasons
to do so.

First, I begin with a very nice subset of logic, which I call
existential-conjunctive logic.  It is simply first-order predicate
calculus with only one quantifier -- the existential -- and only
one Boolean operator -- conjunction.   No universals, negations,
disjunctions, or implications.

This subset is nice for several reasons:

 1. Existential quantification and conjunction are the two
    least problematical operators of logic.  You can find puzzles,
    paradoxes, and philosophical controversies about every one
    of the others:  universal quantification, implication,
    disjunction, and negation.

 2. Every database system, frame system, and even good old-fashioned
    file system can represent existential-conjunctive logic.

 3. It is capable of describing anything that exists, although it
    cannot state any generalizations or deny that something exists.
    For example, I can describe the complete contents of the room
    I am now sitting in using only existential-conjunctive logic.
    But I can't tell you that there is no hippopotamus in it.
    (Actually, the room next to it does have a hippopotamus -- a
    replica of a blue hippopotamus from the Metropolitan Museum.)

 4. It is an easily decidable subset of logic, and there exists a
    normal form for every proposition that is easily computable
    in (N log N) time.

Normal form:  Simply convert a formula to prenex normal form,
sort all the conjuncts in alphabetical order, delete duplicates, 
and replace the variable names by the standard names x1, x2, x3, ...

For this subset of logic, I define two formulas to be expressions of
the same proposition iff they can be reduced to the same normal form.

This definition has all the nice properties you may like -- and it
happens to coincide with the definition of proposition as a class
of possible worlds or possible models.

Now I would like to extend this definition to all of first-order logic.
I begin by adding just one more operator -- negation.  Then given any
formula in FOL, I make the usual conversions:

 (Ax) -> ~(Ex)~

 (p or q) -> ~(~p & ~q)

 (p implies q) -> ~(p & ~q)

The only simplifications I'll allow are to delete redundant
parentheses and to delete two adjacent negations with nothing
between them; i.e. ~~ becomes blank.

Normal form:  This leads to a normal form for FOL that is as easy
to compute as the normal form for existential-conjunctive logic:
Starting with the innermost parentheses, sort the conjuncts and
delete duplicates; then work your way out of the nested parentheses
doing the sorting and deleting.

Now I will define two formulas to be expressions of the same
proposition iff they reduce to the same normal form by this procedure.

I claim that this definition has lots of nice properties:
easily computable; trivial variations collapse to the same
normal form; most obvious variations collapse to the same form;
but nonobvious variations do not collapse to the same form.

Furthermore, given the same predicate names and alphabetical
sort order, you can define equivalent procedures for languages
as syntactically different as KIF, CGs, vanilla-flavored predicate
calculus, etc.

If you want more than FOL, this procedure can be extended
by allowing the quantifiers to range over whatever you like.

John Sowa