From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Fri, 02 Feb 2001 09:01:46 -0500

To: timbl@w3.org

Cc: drew.mcdermott@yale.edu, connolly@w3.org, danbri@w3.org, horrocks@cs.man.ac.uk, www-rdf-logic@w3.org

Message-Id: <20010202090146Y.pfps@research.bell-labs.com>

Date: Fri, 02 Feb 2001 09:01:46 -0500

To: timbl@w3.org

Cc: drew.mcdermott@yale.edu, connolly@w3.org, danbri@w3.org, horrocks@cs.man.ac.uk, www-rdf-logic@w3.org

Message-Id: <20010202090146Y.pfps@research.bell-labs.com>

Tim Berners-Lee <timbl@w3.org> has made the following comment: > > There are many related logics, which use different sets of > axioms and inference rules, but have the (provable) property > that there is a mapping from formulae in one to formulae in > another such that one engine cannot infer something > which mapped across it false in the other system. > > The universal language defines this set of logics, if you like. > It doesn't define which set of axioms any engine should use. > It doesn't define which set of inference rules. > It does require that whatever you do use must be consistent > with some standard set. > > So all expressions of FOPC for example are basically > equivalent. I understand that Conceptual Graphs and KIF > are higher order logics and are equivalent. I think that the above comments severely misrepresent the situation, as least so far as ``representation'' is concerned. Yes, sufficiently powerful formalisms are in some sense universal, but this doesn't matter! FOPC is universal in roughly the same sense that lambda calculus is. KIF is universal even more strongly in this sense. For example, suppose you wanted to represent non-well-founded sets in KIF. (By the way, this is not an arbitrary example. The type relationship in RDFS is very akin to set membership, and it would be very appropriate to represent it as set membership.) How can this be done? You can't use sets built into (some versions of) KIF because this version of sets is well founded. So you have to revert to using the basic logical machinery of KIF, using an uninterpreted predicate and axiomatizing it. But now you have two completely unconnected versions of sets. Similarly, if you wanted to represent statements that had non-boolean truth values (such as confidence factors), you couldn't use the istrue predicate built into (some versions of) KIF. You would have to axiomatize this logic using uninterpreted predicates. I claim that in both cases you are not using KIF as a representation language but instead are using it as an implementation language. You could have used some other Turing-complete formalism, such as the lambda calculus. So what is gained from using a language that is universal in this sense? My view would be ``not much''. But the situation is even worse. Suppose you really wanted to have a universal language. Well there are lots of things that KIF can't state because it is essentially a first-order language, even though it has some constructs that appear to be higher order. For example, KIF can't be used to directly make statements about all propositions. You can't even pull the ``implementation'' mechanism used above because you can't finitely axiomatize higher-order logic. Now there are good reasons to prefer a first-order logic over a higher-order logic. But they have to do with (surprise) implementation and computability issues, not representational issues. If you really want to *represent* everything, you need a more-powerful logic than first-order logic, even with KIF-style extensions! This is why I (rather tongue-in-cheek) proposed Montague logic as a Universal Web Logic. However, even Montague logic is probably insufficient. (By the way, if you really want a Universal Web Logic, Montague logic would be an excellent starting point, in my opinion.) Peter Patel-Schneider Bell Labs ResearchReceived on Friday, 2 February 2001 09:02:11 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:33 UTC
*