ontolog-forum
[Top] [All Lists]

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

 To: "[ontolog-forum]" "John F. Sowa" Sun, 02 Mar 2008 10:59:58 -0500 <47CACEFE.2010501@xxxxxxxxxxx>
 ```Chris and Pat,    (01) I'm traveling now and I don't have a copy of Gödel's paper handy, but I'll try to reconstruct as much as I can recall.    (02) > To expand on Pat's point: Gödel'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.    (03) As I recall, Gödel was not trying to prove the incompleteness of number theory, but the incompleteness of higher-order logic. In his PhD dissertation, Gödel (1930) proved the completeness of first-order logic:    (04) From any given set of axioms A stated in FOL, every proposition p that is true in all models of A can be proved from A by the usual rules of inference of FOL.    (05) But in his incompleteness paper, Gödel (1931) proved that any version of higher order logic that is sufficiently expressive to define arithmetic is incomplete.    (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. That approach was important because the proof procedure involved a reductio ad absurdum; i.e., either arithmetic is inconsistent or HOL is incomplete. If Gödel had decided to prove something like "Either ZFC is inconsistent or HOL is incomplete", mathematicians in 1931 would be likely to say "A pox on both houses".    (07) To carry out his proof, Gödel made the following assumption:    (08) The computational methods of ordinary arithmetic are consistent.    (09) Then he carried out his proof of incompleteness of HOL in the following stages:    (010) 1. Choose a particular version of HOL -- the one defined by Whitehead and Russell in the _Principia Mathematica_ (PM).    (011) 2. Define a method of encoding every symbol, formula, and proof in PM into an integer.    (012) 3. Assume common functions over integers and common notions, such as 'prime number', and assume that the published definitions and proofs based on Peano's axioms are correct.    (013) 4. Define various functions over integers, such as    (014) isaFormula(i) -> integer i is an encoding of a PM formula    (015) isaProof(i,j) -> integer i is an encoding of a PM proof of the formula encoded by integer j    (016) isProvable(i) -> integer i is an encoding of a PM formula for which there exists an integer j which encodes a PM proof of the formula encoded by i.    (017) 5. Define an integer k, which encodes a formula that says, in effect, this formula is not provable.    (018) 6. Prove that isProvable(k) is false.    (019) 7. Since the formula encoded by k must be either true or false, there are two options:    (020) (a) k is true, and it correctly states that k is not provable.    (021) (b) k is false, therefore k must be provable, and the system of arithmetic used to encode all the functions defined above must be inconsistent.    (022) Since all mathematicians have for many millennia assumed that arithmetic is consistent, they would naturally prefer option (a), which implies that there are statements in HOL that are true in all possible models, but they are not provable by the rules of inference of HOL.    (023) This proof, as I interpret it, does not prove that arithmetic is incomplete, but that the system of PM is incomplete. Henkin, for example, showed that proofs from Peano's axioms could be complete if nonstandard models were included.    (024) John    (025) _________________________________________________________________ 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    (026) ```
 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