Back to propositions

sowa <sowa@turing.pacss.binghamton.edu>
Date: Mon, 28 Feb 94 07:54:42 EST
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9402281254.AA05940@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU
Subject: Back to propositions
Cc: sowa@turing.pacss.binghamton.edu
This discussion of graphs vs. wffs, variations of variable binding, 
etc., has raised a lot of interesting points.  But I would like to
focus on the original question:  How do we define proposition as
an equivalence class of sentences in some natural, well motivated,
language independent way?  The second question of finding an efficient
algorithm for computing the equivalence is important, but distinct
>From the first.

My suggestion of looking at existential-conjunctive logic as a first
step was intended as motivation.  Ex-con logic has many interesting
properties:

 1. It is equivalent to such widely diverse notations as relational
    databases and most, if not all, of Roger Schank's examples of
    conceptual dependencies.  (I deliberately said "examples", since
    Roger has consistently avoided and even argued against formalization.)

 2. There is only one reasonable definition for defining proposition:
    treat each formula as a set of conjuncts and eliminate duplicates.

 3. This purely syntactic definition happens to have the semantic
    property of being equivalent to the definition of proposition
    as the set of all possible worlds or models for which the
    proposition has denotation True.

 4. By adding just one additional operator, negation, Ex-Con logic
    becomes full FOL.  Furthermore, the "natural" definition of
    proposition for Ex-Con logic generalizes "naturally" to this
    way of writing FOL.

 5. This generalization happens to be equivalent to a definition
    in terms of C. S. Peirce's existential graphs:  Two formulas
    express the same "proposition" iff they map to the same
    existential graph.

As an example of the amount of reduction that is possible, I would
like to cite the following example:

   ((p -> r) & (q -> s)) -> ((p & q) -> (r & s)).

Leibniz called this proposition the Praeclarum Theorema [splendid theorem].
Whitehead and Russell called it Proposition 3.47 in the Principia.

Using the basic 4 Boolean operators (and, or, not, implies),
there are 864 distinct, but logically equivalent formulas that
all map to the same existential graph.  If you allow duplicate
conjuncts, there are an infinite number of formulas.

Considerations of this sort have led me to believe that Peirce's
existential graphs are a very good candidate for a normal form
for defining "proposition".  As I mentioned in an earlier note,
I suggested that to Richard Fikes, but he preferred a definition
that was expressible in KIF without going to any other language.
That is what led me to the first note in this series.

I may have been hasty in saying that this definition of "proposition"
is efficiently computable in all possible cases.  But in most practical
cases, it can be computed quickly, and it can be defined in a
language-independent way (as I did in my first note about "propositions").

John Sowa