Re: Propositions
phayes@cs.uiuc.edu
Message-id: <199402152121.AA05675@dante.cs.uiuc.edu>
X-Sender: phayes@dante.cs.uiuc.edu
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Tue, 15 Feb 1994 15:27:49 +0000
To: sowa <sowa@turing.pacss.binghamton.edu>, cg@cs.umn.edu,
interlingua@ISI.EDU
From: phayes@cs.uiuc.edu
Subject: Re: Propositions
John-
>.....
>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. ...
I am sympathetic to your goal here but I think there are some snags. In
particular, 'existential/conjunctive logic' is too weak to play the
required role. It is just the logic of ground atoms. The existential
quantifiers can always be taken to have universal scope (with suitable
changes of variable name), so existentially bound variables have the same
logical status as (skolem) names; and the body of any expression consists
only of a conjunction of ground atoms. Existential scope only comes to have
significance when negations or disjunctions are present.
I don't agree that this is capable of describing anything that exists; in
fact I dont think its capable of describing *anything*. This might
illustrate the difference betwen Fritz Lehmann and I, by the way. Suppose
we had such a 'description' of your office, which would be a big
conjunction of atoms like this:
"On(papersheet1,desk)& On(papersheet2,papersheet1)&...&Color(Wall3,white)&..."
Now, why would this be a description of your office? Because it asserts all
the things which are true of your office, presumably. But this answer
assumes that the predicates On, Color, etc. mean what we intend them to
mean, and what justification do we have for that claim? Fritz would say (I
think) that we need no such justification, and perhaps you would agree.
This is a perfectly rational position, perhaps one well suited to thinking
about databases and interlingua, but I think it misses the core of the Krep
enterprise.
A stronger idea of what constitutes a 'representation' or a description is
that appropriate consequences can be inferred from it (or somehow extracted
>From it: I don't mean here to be taking a position in a
deductive/procedural debate). The more appropriate conclusions that can be
inferred from a representation (without of course inferring inappropriate
ones), the closer it can claim to be an accurate description. A
representation of 'On' must somehow enable the conclusion of
'On(papersheet2, desk) from the above assertions, for example. But such
conclusions are unobtainable in 'existential/conjunctive logic'; in fact,
almost all conclusions are unobtainable! About all we could do is conclude
smaller conjunctions, permute the conjunctive atoms and rename things. That
such a language is tractable is hardly surprising. If we define its
sentences to be sets of atoms, then it has no rules at all. For example,
suppose we take a first-order expression and normalise it according to your
rules, ie put it in clausal form, then decide to use
'existential/conjunctive logic' on it. This amounts to treating P and ~P as
different predicates, since negation is now 'invisible'. Immediately,
resolution is impossible and there are no inferences to be made.
This is my problem with the intermediate-language idea: how to find a
suitably 'intermediate' language. I don't think restricting the vocabulary
of logical symbols is going to really provide a suitable intermediate
level. Without negation, or something which somehow encodes the force of
negation, no nontrivial inferences are going to be possible. Any of the
'modus' rules require an implicit contradiction which is resolved by the
inference. Without the ability to express disagreement betwen parts of
expressions, inference can only consist of rearranging propositions and
free instantiation, neither of which amount to much.
However, this debate might be orthogonal to the idea of using normal form
in a suitable subset of logic to define 'same proposition', and I agree
this idea is worth pursuing. Why did you not suggest positive logic
(allowing universals and disjunctions as well)? I like the idea of 'same
proposition' being somehow sensitive to the relative scopes of universal
and existential quantifiers.
A different approach to an intermediate language might be something like
(eg.) Horn logic, which restricts the syntax of expressions. Horn logic has
some pleasant computational properties but doesnt completely sacrifice
expressiveness. But I suspect it is too close to 1PC to be a suitable
intermediate language here.
.....
>
>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.
>
Can you give an example of two expressions which are variants but don't
have the same normal form? Such examples would be the tests of the idea
that identity of normal form might be a good test of same proposition, and
I cant think of any quickly.
Pat Hayes
PS. This whole discussion may be related to the discussion in logic about
normal forms of proofs. There isn't a clearly accepted definition of an
equivalence on natural-deduction proofs, in spite of attempts such as
Gentzen's to provide one. Consider this hypothesis:
Propositional Projection Lemma
If P1 equiv P2 and P1 entails Q1, then there is a Q2 such that
Q1 equiv Q2 and
there are equivalent proofs of Q1 from P1 and Q2 from P2.
Reasonable definitions of equivalence on sentences and on proofs should
satisfy this. Without the last 'equivalent' it is trivial, of course.
----------------------------------------------------------------------------
Beckman Institute (217)244 1616 office
405 North Mathews Avenue (217)328 3947 or (415)855 9043 home
Urbana, IL. 61801 (217)244 8371 fax
hayes@cs.stanford.edu or Phayes@cs.uiuc.edu