- From: Miles Sabin <msabin@interx.com>
- Date: Thu, 18 Apr 2002 19:56:13 +0100
- To: <www-rdf-logic@w3.org>
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
Received on Thursday, 18 April 2002 14:56:50 UTC