Back to propositions

• Mail folder: Interlingua Mail
• Next message: Matthew L. Ginsberg: "KIF review"
• Previous message: sowa: "Back to propositions"
• In-reply-to: sowa: "Back to propositions"

Date: Mon, 28 Feb 94 08:27:15 -0800
From: John McCarthy <jmc@sail.stanford.edu>
Message-id: <9402281627.AA26875@SAIL.Stanford.EDU>
To: sowa@turing.pacss.binghamton.edu
Cc: cg@cs.umn.edu, interlingua@ISI.EDU, sowa@turing.pacss.binghamton.edu
In-reply-to: <9402281254.AA05940@turing.pacss.binghamton.edu> (sowa@turing.pacss.binghamton.edu)
Subject: Back to propositions
Reply-To: jmc@cs.stanford.edu

I have considered John Sowa's problem a lot, i.e. considering
propositions as equivalence classes of sentences.  My paper
"A First Order Theory of Individual Concepts and Propositions"
treats it.  Here are some opinions derived from the paper and my other
thinking.  This note doesn't address the specific points made in
John Sowa's previous note.

1. If quantified expressions are allowed, finding a normal form
is unsolvable in the technical sense.  This follows from the fact
that it is unsolvable whether the formula has a trivial normal form,
i.e. is valid.

2. There may be some restricted classes of sentences which admit
computable normal form.  It is true for monadic sentences.  Whether
some major class of useful sentences admits a computable normal form
is unknown to me.  Maybe some class of conceptual graphs or even
semantic networks has a computable normal form.  David McAllester
has done work in this direction.

3. The normal form for monadic sentences is not practically computable
in general because if there are  n  predicates, there are  2^(2^n)
cases be considered.

4. Propositional calculus admits several normal forms, e.g.
conjunctive, disjunctive and forms based on trees.  Finding any of the
normal forms is NP-complete, because finding if the formula is a
tautology, i.e. has trivial normal form, is NP-complete.  There is
often an exponential expansion in size in going to the normal form.
Every kind of propositional abbreviation, e.g. introducing iff
as a propositional operator or introducing propositional conditional
expressions, shortens some expressions exponentially, i.e. eliminating
them sometimes causes exponential blowup.

5. As my paper shows, sentences are the tip of the iceberg.
Individual concepts also need a good notation.

6. Contention: bound variables are not avoidable without exponential
inconvenience in general.  As stated in my earlier message, the
syntactic properties of expressions involving them need to be studied,
and context free languages are inadequate - certainly if
used in the usual way.

7. Goedel's paper, "On the Length of Proofs" advances many relevant
considerations, e.g. how stronger languages and the use of lemmas
shorten proofs exponentially.

8. The use of definitions shortens statements in human language,
and eliminating them is impractical.  The same is true of languages
to be used by computers.