Re: universal languages

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 Research

Received on Friday, 2 February 2001 09:02:11 UTC