[Top] [All Lists]

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

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 16 Feb 2010 11:50:19 -0600
Message-id: <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)

<Prev in Thread] Current Thread [Next in Thread>