**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.