Re: Propositions

sowa <sowa@turing.pacss.binghamton.edu>
Date: Wed, 16 Feb 94 07:29:32 EST
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9402161229.AA15552@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU, phayes@cs.uiuc.edu,
        sowa@turing.pacss.binghamton.edu
Subject: Re: Propositions

Pat,

> ... 'existential/conjunctive logic' is too weak to play the
> required role. It is just the logic of ground atoms.

Yes, it includes ground atoms.  But it also has real quantifiers.
That's what makes it capable of being extended to full FOL with the
addition of just one more operator -- negation.  In defining
"proposition", I started with a definition that was suitable for
this subset.  Then I showed how it could be generalized in a step
by step manner to FOL and then to HOL.

Your discussion of how predicate names are related to things in the
world is the symbol-grounding problem, which is of course important.
But once you have reached a representation of any kind -- FOL, KIF, 
CGs, frames, etc. -- you have made a commitment to some set of names.
A formal definition of proposition in terms of some system of logic
can only be stated in terms of the names that have been chosen by
the knowledge engineer -- the grounding "world" is no longer
available to us.

Re syntax vs. semantics vs. logical consequence:  I stated that
definition in terms of the syntax of formulas -- that is computationally
the most accessible way to start.  But one very pleasant result of
that definition -- which must be a requirement for any definition
of "proposition" -- is that it has desirable semantic and provability
implications:

 1. Re provability:  Any two formulas which express the same
    proposition are provably equivalent -- by a proof that takes
    no more than (N log N) time.  Conversely, two formulas that
    may require exponential time to prove equivalent are not
    in the same equivalence class of "proposition".

 2. Re model theory:  Any two formulas which express the same
    proposition are true of exactly the same set of models.

> Without negation, or something which somehow encodes the force of
> negation, no nontrivial inferences are going to be possible.

Yes, of course.  Please reread my definition:  I started by defining
"proposition" for the existential-conjunctive subset.  Then I added
negation and generalized the definition to that subset, which happened
to give us full FOL.  The reason why I started with the E-C subset
is that it is a very simple subset where the definition of "proposition"
is unproblematical.  In fact, no other definition even seems plausible.
Then I generalized that procedure to the next level, where it applied
to all of FOL.

> ... Why did you not suggest positive logic
> allowing universals and disjunctions as well?

I think that we should consider many different subsets of logic
for many different purposes.  E-C logic is the minimal useful subset 
that has relatively easy decidability results.  There are many
useful subsets between E-C and full FOL, such as positive logic,
Horn-clause logic, etc.

To answer Bob MacGregor's concerns about "checking in and checking out,"
I believe that we should identify a hierarchy of logics of varying
expressive power.  Then you can identify which subset is appropriate
for communications between any pair of languages.  One of the main
reasons why I like E-C logic is that it is in the intersection of
essentially every useful KR language, database language, etc.

> Can you give an example of two expressions which are variants but don't
> have the same normal form? 

Here are two examples:

 1. (p or p) reduces to just p by the following steps:
    (p or p) -> ~(~p & ~p) -> ~~p -> p.

 2. (p implies p) reduces to ~(p & ~p), which cannot be reduced further.

Point #1 implies that many "obvious" equivalences with disjunction
reduce nicely, even though the definition was stated in terms of
conjunctions.

Point #2 implies that (p implies p) and (q implies q), although
both trivial tautologies, do not turn out to be equivalent.
I believe that is a highly desirable property, because p might
be "The sun is shining" and q might be "Grass is green."
Since the subject matter is different, (p implies p) and
(q implies q) talk about different things and should not be
considered "the same proposition."

> PS. This whole discussion may be related to the discussion in logic about
> normal forms of proofs.

Yes, it's probably related.  But the steps permitted in deriving
a normal form are just a subset of the valid rules of inference;
e.g. you can't do modus ponens, for example.  That is important,
because it means that you can never eliminate any predicate names
that appear in a formula: i.e. if you have multiple copies of p
in the starting formula, there must always remain at least one
copy in the normal form.

John