ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] Search engine for the ontology

 To: "[ontolog-forum] " Chris Menzel Sun, 2 Mar 2008 15:47:34 -0600 (CST)
 ```On Sun, 2 Mar 2008, John F. Sowa wrote: > Chris and Pat, > > I'm traveling now and I don't have a copy of Goedel's paper > handy, but I'll try to reconstruct as much as I can recall. > > > To expand on Pat's point: Goedel's mapping of the proof theory > > of predicate logic into arithmetic had nothing to do with > > foundational issues. Rather, it was the mechanism that enabled > > him to prove the essential incompleteness of number theory. > > As I recall, Goedel was not trying to prove the incompleteness of > number theory, but the incompleteness of higher-order logic.    (01) Well, first of all, let's be careful. You've got two very different notions of (in)completeness here: negation completeness and semantic completeness. A system S is negation complete if, for any sentence A of the language of S, either A or its negation ~A is a theorem of S. Note that this is a purely proof theoretic notion. A *logic* L -- that is, a language + semantics + proof theory -- is semantically complete if every logical truth of the language of L is a theorem of L. Note that nothing we typically call a system of *logic* is negation complete. For example, in propositional logic, no propositional variable p or its negation ~p is a logical theorem. In predicate logic, neither (x)Px nor ~(x)Px, for example, is a theorem.    (02) That said, Goedel's Theorem (more exactly, his first incompleteness theorem) is simply that every consistent, "sufficiently strong" system of number theory is negation incomplete; for every such system, there is a sentence of the language of the system that is *undecidable* by the system, i.e., neither provable nor refutable by the system. (Actually, in Goedel's formulation you need the somewhat stronger condition known as omega-consistency, but as I noted in a previous msg, Rosser showed that only consistency is needed.) This result holds for first- and higher-order number theories alike.    (03) As for specifics, it is true that the system Principia Mathematica (PM) of Russell and Whitehead that Goedel appeared to be singling out in his 1931 paper was a higher-order logic, indeed, a so-called omega-order logic that encompassed nth-order logic for every n. However, bear in mind that the title of Goedel's paper was "On Formally Undecidable Propositions of Principia Mathematica *and Related Systems*". In fact, Goedel did not use PM to prove his result but one of these related systems. Specifically, he used an *explicitly* number theoretic, higher-order variant that he called "P". The language of P included a constant "0" to denote 0 (in the intended semantics of P), a 1-place function symbol "f" to denote the successor relation, and simply typed variables ranging over natural numbers, classes of natural numbers, classes of classes of natural numbers, etc. It is this system that he explicitly proved to be negation incomplete (his Theorem VI).    (04) However, Goedel goes on to show that the relations that are needed in a system to code the system's own proof theory are all *arithmetical* -- that is to say, they can all be defined in terms of addition, multiplication, and *first-order* quantification (Theorem VII). He then shows that every (omega-)consistent extension P' of P has an undecidable *arithmetical* sentence (Theorem X), i.e., an arithmetical sentence that it neither proves nor refutes. It is immediate from this fact that Goedel's result applies to any *first-order* system that contains the bit of number theory (now often called Robinson Arithmetic) needed to code its proof theory -- basically, this means just a couple of axioms for 0 and the successor function ("0 is no number's successor"; "numbers with the same successor are identical") and the usual axioms for arithmetic and multiplication ("x+0=x", "x+fy = f(x+y)", "x*0=0", "x*fy = x*(x*y)"). In a higher-order system like P, it is possible to *define* addition and multiplication recursively instead of building them in as primitives and characterizing them axiomatically, as would be done in a first-order system. But Goedel's results are entirely independent of his choice of P.    (05) Bottom line: (i) Goedel's intended target was indeed number theory, not higher-order logic per se, and what he showed is that any consistent extension of a particular higher-order system P of number theory is negation incomplete. However, (ii) it follows immediately from several theorems in Goedel's proof that any system of first-order number theory containing just a few basic number theoretic axioms is also negation incomplete. (iii) It is in fact a *consequence* of Goedel's Theorem that every consistent system of second- (and higher-) order logic is *semantically* incomplete. But this was actually proved some years after Goedel's original publication. (Indeed, the modern distinction between first- and higher-order logic was only just becoming clear around 1931.)    (06) > In other words, the point of the proof was to show that HOL is > incomplete, and arithmetic was used as a well-established system whose > consistency was not in doubt.    (07) This is not historically correct.    (08) > To carry out his proof, Goedel made the following assumption: > > The computational methods of ordinary arithmetic are consistent. > > Then he carried out his proof of incompleteness of HOL in the > following stages: > ...[Overview of the proof elided]... > ... > This proof, as I interpret it, does not prove that arithmetic > is incomplete, but that the system of PM is incomplete.    (09) Again, Goedel used a related higher-order system, but it is a simple consequence of his proof that the result holds for any first- or higher-order system containing Robinson Arithmetic.    (010) > Henkin, for example, showed that proofs from Peano's axioms could be > complete if nonstandard models were included.    (011) I think you have a very different result in mind. Henkin showed that higher-order logic with a so-called "general" semantics is *semantically* complete. The trick is to broaden the range of the higher-order variables beyond what is allowed in standard higher-order logic -- therby opening the door to what might be called nonstandard interpretations of the language of higher-order logic. The upshot of this is that higher-order logic with a general semantics is, in effect, just first-order logic in higher-order garb. Henkin's result has no implications whatever for Peano Arithmetic vis-oedvis its negation incompleteness.    (012) -chris    (013) _________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx Shared Files: http://ontolog.cim3.net/file/ Community Wiki: http://ontolog.cim3.net/wiki/ To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (014) ```
 Current Thread Re: [ontolog-forum] Search engine for the ontology, Azamat Re: [ontolog-forum] Search engine for the ontology, Sharma, Ravi Re: [ontolog-forum] Search engine for the ontology, John F. Sowa Re: [ontolog-forum] Search engine for the ontology, John F. Sowa Re: [ontolog-forum] Search engine for the ontology, John F. Sowa Re: [ontolog-forum] Search engine for the ontology, Chris Menzel <= Re: [ontolog-forum] Search engine for the ontology, Chris Menzel Re: [ontolog-forum] Search engine for the ontology, Christopher Menzel Re: [ontolog-forum] Search engine for the ontology, Chris Menzel Re: [ontolog-forum] Search engine for the ontology, rick@xxxxxxxxxxxxxx Re: [ontolog-forum] Search engine for the ontology, Christopher Spottiswoode Re: [ontolog-forum] Search engine for the ontology, John F. Sowa Re: [ontolog-forum] Search engine for the ontology, John F. Sowa Re: [ontolog-forum] Search engine for the ontology, Azamat Re: [ontolog-forum] Search engine for the ontology, Sharma, Ravi Re: [ontolog-forum] Search engine for the ontology, John F. Sowa