RE: A Single Foundational Logic for the Semantic Web

Sandro Hawke wrote,
> In other words, if you can get a machine to do something with 
> logic X, then you can, in essense, get every machine which 
> understands Horn clauses (or Java, or whatever) to do the same 
> thing with logic X.  If you can't get a machine to handle logic 
> X, you're really out of luck in any case.

This is true, but unfortunately not very useful.

I can't remember the details, but in his paper, "A Curious 
Inference", the late George Boolos gives an example of a proof
which is trivial in second order system, and which can be proved in 
first order systems, but only in a completely infeasible number of 
moves.

More generally, it's not just _what_ can be proved which is 
affected by the expressivness of your underlying logic, but also 
what can be proved _practically_.

Cheers,


Miles