|From:||Chris Menzel <chris.menzel@xxxxxxxxx>|
|Date:||Sun, 30 Sep 2012 18:41:10 -0500|
On Sun, Sep 30, 2012 at 11:30 AM, William Frank <williamf.frank@xxxxxxxxx> wrote:|
On Sun, Sep 30, 2012 at 10:56 AM, Chris Menzel <chris.menzel@xxxxxxxxx> wrote:
Oh please, don't turn this perfectly understandable fact into some sort of conspiracy theory by scientific elites. That's a one way ticket to Crank City.
Nope, I don't think anyone thinks that.
But nearly everyone thinks that. It is part of what makes the study of first-order PA, r.e. subsystems of second-order PA, etc so interesting. The fact that these systems have nonstandard models shows exactly that they full short of fully expressing arithmetic concepts. This raises fascinating questions about the structure of these non-standard models (e.g., there is, up to isomorphism, only one non-standard countable model of PA), about how much expressibility is gained by starting with weaker systems and adding more axioms, infinitary rules of inference, etc. Your conspiratorial hypothesis is just wildly off the mark.
There is not much that's mechanistically useful about even FOL — it's only r.e. What's nice about that, though, is that you get the marvelous, theoretically rich and useful correlation between semantics and proof theory.
When it comes to representation, you will get no argument from me (and a number of other people in this forum including John and Pat) for using at least full FOL freely, and I would have no objection whatever to using second-order logic if it should prove useful. I myself have serious doubts about that because you can't force a full second-order interpretation of the axioms — but I am of course all for the use of the syntactic apparatus of second-order logic, notably, predicate quantifiers.
As for the "inadequacy" of OWL (by which I assume you mean OWL DL) — I too am skeptical of the insistence on decidability. But if your goal is to be able to represent information in a computer in order, among other things, to be able to invoke automated reasoning tools, then it would be quite pointless to insist on a framework based on second-order logic, as it would have no complete proof theory and, hence, no definite logic to implement.
_________________________________________________________________ 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 (01)
|<Prev in Thread]||Current Thread||[Next in Thread>|
|Previous by Date:||Re: [ontolog-forum] Universal Basic Semantic Structures, Avril Styrman|
|Next by Date:||Re: [ontolog-forum] Universal Basic Semantic Structures, William Frank|
|Previous by Thread:||Re: [ontolog-forum] Universal Basic Semantic Structures, William Frank|
|Next by Thread:||Re: [ontolog-forum] Universal Basic Semantic Structures, William Frank|
|Indexes:||[Date] [Thread] [Top] [All Lists]|