Re: [ontolog-forum] Universal Basic Semantic Structures

[Chris Menzel <chris.menzel@xxxxxxxxx>]

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:

On Sun, Sep 30, 2012 at 8:51 AM, William Frank <williamf.frank@xxxxxxxxx> wrote:

...

I think what you meant was,  'in a first order axiomatization of arithmetic'. 

I did indeed; it didn't even occur to me that you had second-order arithmetic in mind. You are of course correct that, in second-order Peano Arithmetic (PA), addition and multiplication are definable in terms of successor.

It would have been clarifying for you to add the crucial "second-order" qualification; for me (and I'm not alone) the meaning of "arithmetic" defaults to "first-order PA".

That is right, you are **very far** from alone, and having lots of respectable company is something that most scientists take a great deal of comfort in, for good reasons.   This is my underlying point:

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.

 

as first-order systems of arithmetic are the only ones that are relevant to establishing Gödel's theorem and its consequences.  

 
Yes, but the implicit computational cultural bias is that as a 'consequence' (in another sense, using an unexplicit assumption), first order arithmetic better expresses arithmetic concepts.

Nope, I don't think anyone thinks that.

 

I think it shows the opposite, that first order arithmetic cannot adequately express arithmetic concepts.

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.

 — understandably, as there is no complete proof theory for full second-order validity. 

Yes, and this "understandably" is to me the mechanistically-oriented bias of the generally accepted views.  

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.

 

I this attitude is behind the inadequacy of OWL, for just one example.  Why not the opposite conclusion, that people's imagination exceeds their grasp, so let us focus on our imagination, which can be expressed better in higher order languages?

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.

-chris

_________________________________________________________________
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)