ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] Foundation ontology, CYC, and Mapping

 To: "[ontolog-forum] " Christopher Menzel Tue, 16 Feb 2010 11:50:19 -0600 <10FDC8E1-A716-45CC-8E7C-02D4B3B0D317@xxxxxxxx>
 ```On Feb 15, 2010, at 4:28 PM, Rob Freeman wrote: > Pat, > > What is clear is that: > > 1) You keep repeating your belief that a single complete > axiomatization (with useful coverage?) is possible. > > 2) You admit you don't know how to prove it is possible. > > 3) You ignore/don't understand that other people have proven it is impossible. > > "A complete and consistent logic complex enough to include arithmetic > was shown by Kurt Goedel to be impossible..."    (01) Better, in characterizing Gödel's theorem, to talk about theories rather than logics. Also better to emphasize simplicity rather than complexity, as one needs only a very modest bit of arithmetic to prove incompleteness in general. That modest bit is usually called Q. Q contains three axioms for the successor function, two of which also axiomatize 0:    (02) 1. ∀x(0 ≠ sx) -- "0 is not the successor of any number." 2. ∀x(x ≠ 0 → ∃y(x = sy)) -- "Every nonzero number has a predecessor" 3. ∀xy(sx = sy → x = y) -- "The successor function is 1-1"    (03) In addition, Q provides the obvious axioms for addition and multiplication:    (04) 4. ∀x(x + 0 = x) 5. ∀xy(x + sy = s(x + y)) 6. ∀x(x • 0 = 0) 7. ∀xy(x • sy = s(x • y))    (05) Finally, it is absolutely critical in a characterization of the theorem to mention recursive axiomatizability (basically, the property a theory has when it is possible (i.e., you can write a program) to list its theorems), since there are in fact complete, consistent (but not recursively axiomatizable) theories that include that modest bit of arithmetic (a trivial example being simply being the theory consisting of all true sentences in the language of arithmetic). So, specifically, what Gödel showed was:    (06) (*) No consistent, complete theory that includes Q is recursively axiomatizable.    (07) And, actually, Gödel didn't prove exactly (*) in his famous 1931 paper, he proved something weaker, although (*) itself can be proved using only the foundations that he laid in that paper (and was done so by Rosser in 1936).    (08) As for charge #3 that you direct at Pat above, Pat has never claimed that a FO would include a complete, consistent, recursive axiomatization of arithmetic. You should be more careful about lecturing others about what they don't understanding.    (09) > I'm also finding references to a guy named Thoralf Skolem. Anyone else > heard of him?    (010) Of course. He's a prominent figure in the history of mathematical logic in the early 20th century, particularly well known for his work in model theory.    (011) > "In the 1922 lecture the Löwenheim-Skolem theorem was applied to a > formalization of set theory. The result was a relativization of the > notion of set, later known as the Skolem paradox: If the axiomatic > system (e.g. as presented by Zermelo) is consistent, i.e. if it is at > all satisfiable, then it must be satisfiable within a countable > ``Denkbereich'' (domain). But does this not contradict Cantor's > theorem of the uncountable, the existence of a never-ending sequence > of transfinite powers? The ``paradox'' of Skolem is no contradiction.    (012) Indeed not. It is a theorem about the expressive limitations of first-order logic.    (013) > Roughly speaking it asserts that there is no complete axiomatization > of mathematics,    (014) Actually, the Löwenheim-Skolem theorem doesn't say that at all. It says that a theory with infinite models has a countable model. In and of itself, that does not imply incompleteness. (If it did, Löwenheim and Skolem would be credited with discovering arithmetical incompleteness in the early 1920s.)    (015) > and that certain concepts must be interpreted relative to > a given axiomatization and its models and thus have no ``absolute'' > meaning."    (016) That's in fact a highly controversial (some would even argue decisively refutable) philosophical interpretation of the the L-S theorem. Regardless of your philosophical view of the theorem, the idea that the notion of set is "relative" to an axiomatization is certainly not a *mathematical* consequence of it.    (017) > "Towards the end of the 1929 paper Skolem expressed some doubts about > the complete axiomatizability of mathematical concepts. His scepticism > was based on the set-theoretic relativism which follows from the > Löwenheim-Skolem theorem. In 1929 he could give only some partial > results, but in a paper from 1934 (and a previous one from 1933) > ``Über die Nichtcharacterisierbarkeit der Zahlenreihe mittels endlich > oder abzählbar unendlich vieler Aussagen mit ausschliesslich > Zahlenvariablen'' he could prove that there is no finite or countably > infinite set of sentences in the language of Peano arithmetic which > characterizes the natural numbers. Today, this follows as a simple > consequence of Gödel's completeness theorem. The technique used by > Skolem was a more direct model-theoretic construction. And this > technique, suitably refined to the so-called ``ultraproduct'' > construction, has been an important tool in recent work on model > theory." > > http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no2/skobio/node1.html > > By the way, my alternative is to work directly with observations of > different kinds, perhaps indexed by labels, and implement > interoperability based on overlaps between sets of these, as the task > demands.    (018) Your alternative to *what*? The above is just a description of certain historical developments in mathematical logic. It doesn't make sense to talk about an "alternative" to it, especially one that involves contemporary notions out of ontological engineering like interoperability.    (019) Chris Menzel    (020) _________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (021) ```
 Current Thread Re: [ontolog-forum] Meanings in an ontology, (continued) Re: [ontolog-forum] Meanings in an ontology, ravi sharma Re: [ontolog-forum] Inconsistent Theories, doug foxvog Re: [ontolog-forum] Inconsistent Theories, Christopher Menzel Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, John F. Sowa [ontolog-forum] Merging Service Ontologies to form Application Ontologies, Rich Cooper Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Rob Freeman Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, John F. Sowa Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Rob Freeman Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Patrick Cassidy Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Rob Freeman Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Christopher Menzel <= Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Patrick Cassidy Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Jawit Kien Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Patrick Cassidy Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, AzamatAbdoullaev Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Rob Freeman Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Patrick Cassidy Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Christopher Menzel Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Rob Freeman Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, David Eddy Re: [ontolog-forum] Foundation ontology, CYC, and Mapping, Rob Freeman