# Re: Propositions

schubert@cs.rochester.edu
Date: Tue, 15 Feb 1994 14:57:50 -0500
From: schubert@cs.rochester.edu
Message-id: <199402151957.OAA20475@cherry.cs.rochester.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU, sowa@turing.pacss.binghamton.edu
Subject: Re: Propositions

Hi John,
I've thought about propositions from a similar perspective (e.g.,
in connection with the problem of deciding what is "true by definition",
given some definitions (and contingent facts). Things seem a little more
complicated to me, though.
For one thing, to get FOL you need to consider equality. For another,
I don't really know how to sort conjuncts (or, as Pat suggests, treat
them as sets). The trouble lies in the variable names. For instance,
the following are intuitively identical propositions
(E x)(E z)~((E v)(E w)~((~(P(x)&P(v)) & ~(P(z)&P(x))) & R(v,w,x))
(E v)(E w)~((E x)(E y)~((~(P(v)&P(w)) & ~(P(y)&P(w))) & R(y,x,w))
(the second is obtained from the first by variable renaming x z v w
w v y x
and permutation of conjuncts). The brute force strategy of trying all
renamings (and sorting the conjuncts for each renaming) would of course
be exponentially complex.
-Len