Re: [KIF] Re: SUO: tuples
John wrote:
> Yes, I realize that sequence variables solve an important problem.
> But they introduce a new problem: two kinds of variables, one of
> which has serious restrictions on how it can be used.
What are you categorizing as a problem? And why? Is it merely the fact
that there are two kinds of variable? Why is that any more of a problem
than there being, say, two types of constant (predicate and individual)
in ordinary predicate logic? These are simply different syntactic types
to play different semantic roles. And actually, in full CL, there are
virtually no restrictions at all on how sequence variables can be used.
(Let's use Pat's suggestion of "row" variables, to avoid the appearance
that such variables are simply sorted first-order variables that range
over sequences in the domain.) The restrictions that Pat has suggested
be incorporated into a CL *sublanguage* yield expressive benefits that
don't clobber the possibility of traditional methods of automated
reasoning. But where tractability is not relevant, those restrictions
are not necessary.
> Some of us have suggested that sequences be introduced as first-class
> data types into the CL ontology. But others have objected that they
> would then introduce other major problems in the model-theoretic
> foundations.
I think you are misremembering. Introduction of sequences would involve
no foundational problems at all. Sequences are just another type of
object. The objection (well, my objection) was that row variables
enable one to capture a variety of linguistic and semantical phenomena
without having to introduce sequences into the domain as first-class
objects. But I will make a stronger point here: certain phenomena
CANNOT be captured via a theory of sequences. Row variables are
essential.
> CM> You've lost me here, John. You seem to be suggesting that the
> > distinction between seq variables and ordinary variables in CL is
> > some sort of artifact foisted upon us by our use of set theory in
> > the metatheory, and hence one that we are better off clobbering.
> > By no means. Seq variables are there because they increase the
> > expressive power of the language in useful ways. They are there
> > by choice.
>
> I realize that seq vars are not an artifact of set theory. I was
> merely pointing out that they do not require anything as strong as
> set theory in order to be introduced into the CL framework as an
> ontological assumption instead of a highly restricted syntactic
> convention.
Well, that's true.
> I was not talking about the metatheory, but about the object language.
> We have tried to avoid any kind of ontological assumptions in CL so
> that anyone could use it to support whatever axioms they prefer.
> I agree that set theory is OK for defining the model theory, since
> the use of any particular version of set theory at the metalevel does
> not in any way limit the kinds of theories one might define at the
> object level.
Right; we're on the same page there, then.
> But I am concerned that the desire to outlaw any kind of ontological
> assumptions in the CL object level has forced upon us an even less
> desirable assumption: the introduction of two different kinds of
> variables, one of which has a highly restricted syntax.
To re-emphasize, there are no significant restrictions on row variable
syntax. More to the point, it is misleading to say we have "outlawed"
ontological assumptions (beyond basic logical commitments to "objects"
and the phenomenon of predication) at the object level, when in fact the
avoidance of such commitements in the foundations makes the framework
compatible with pretty much *any* particular ontological assumptions.
> I would much rather introduce the barest minimum of machinery into
> a CL object-level ontology that is needed to define sequences as
> first-class objects. The point of my previous note is that we can
> do so without any conflict with whatever other ontology or axioms
> anyone might want to express in CL.
So you are proposing that we add a first-order theory of sequences to CL
as an alternative to row variables. Well, we could add a theory of
sequences, but no such theory will be expressively equivalent to row
variables. That is easy to show. For example, in CL, as we all know,
there is no notion of a predicate, let alone an n-place predicate.
(There are two reasons for this: (i) relations are not assumed to have
fixed arity, and (ii) relations are first-class objects that can be
arguments to other relations.) Nonetheless, relations can have a fixed
arity. Row variables enable arities to be axiomatized. For instance,
we can axiomatize the notion of a binary relation thus:
(=> (Binary ?R)
(and (not ?R))
(not exists (?x) (?R ?x))
(not exists (?x ?y ?z @s) (?R ?x ?y ?z @s))))
(Note that the null sequence is a possible value of @s.) This says
(in CL's semantics of row variables) that if ?R is binary, then ?R is
not true (and hence is not a 0-ary relation) and ?R doesn't hold of one
thing or between three or more things. Consequences of this axiom and
an assertion (Binary FOO) will be, e.g.,
(not (FOO a b c))
(not (FOO a b c d))
(not (FOO a b c d e))
and so on.
This axiom simply cannot be expressed with a first order theory of
sequences. For instance, if you try to formulate an analog to the above
axiom:
(=> (Binary ?R)
(and (not ?R))
(not exists (?x) (?R ?x))
(not exists (?x ?y ?z ?s)
(and (Sequence ?s)
(?R ?x ?y ?z ?s))))),
you don't get an equivalent proposition. Rather, this formula says that
if ?R is binary, then ?R is not true and ?R doesn't hold of one thing or
of four things where the fourth is a sequence; a completely different
proposition. In particular, it will not have any of the negated
sentences above as consequences. In fact, the only way I can think of
to get some such approach with sequences to work is to allow only unary
predicates in one's language and to force domains to consist of nothing
but sequences of objects.
> Recommendation: I propose that we have three versions of the CL
> framework, each of which is a superset of the one before:
>
> 1. A version without any kind of built-in ontology and without seq
> variables. This version would support a kind of primitive KIF, along
> the lines that Adam Pease wants, and it would not allow the
> definition of polyadic relations.
I have no idea what you mean by "the definition of polyadic relations",
but, ignoring that part, we already have such basic languages as a
special case of the notion of a CL language as defined in the CL spec
(viz., languages where the set of row variables is empty).
> 2. A version with seq variables along the lines that are currently
> being proposed for CL. This version would treat seq variables as a
> special kind of syntactic convention that would not require that
> there existed an object-level datatype called "sequence".
Row variables are *not* a syntactic convention in current CL. They
increase the expressive power of the language.
> 3. A version that introduced an ontology with two primitive data
> types called integers and sequences. The axioms for these data types
> would be limited to the minimum assumptions necessary to define those
> types without presupposing any version of set theory or any kind of
> infinity beyond countability.
Easily done, though, in light of the fact that sequences cannot replace
row variables, the justification of introducing a theory of sequences
into *CL proper* is less than clear. I do agree that it would be handy
to have such theories ready to hand for applications. I would just balk
at considering including them into anything called a Common Logic
standard, as they are not part of what is traditionally considered
logic. They are theories, plain and simple, built on top of some logic.
> For 99.44% of all applications of CL, Version 3 would be the one that
> people would use.
I should think that for most ontologies, version 1 would suffice.
> It might take a couple of extra pages of metatheory to define, but it
> would be the easiest one to introduce to students,
Given that version 3 would include version 1, it is hard to see how that
could possibly be true.
> and it would provide the minimum level of functionality needed for
> applications to computer systems.
I would certainly agree that one would need a theory of sequences and
numbers for computational applications, but in my mind that would be a
paradigm of a *use* of CL -- CL is the logical foundation to which one
adds whatever ontologies are useful to one's purposes.
> Versions 1 and 2 would only be of interest to purists who wanted to
> define their own primitives for theories of nonstandard arithmetic or
> whatever.
Again, I don't see version 3 as a version of anything we'd want to call
CL.
Regards,
-chris