[SCL] Quantifying over propositions

[Chris Menzel]

On Wed, Aug 10, 2005 at 08:10:44PM -0400, John Sowa wrote:
> In any earlier note, I asked why there was a need
> for a special syntax for propositions, since they
> could be treated as 0-adic relations.
> 
> After pondering the idea, I thought that there
> might be a problem with the model theory:
> 
>   1. An expression of the form (R x y) is true
>      iff the denotation of R includes a tuple
>      with the two values <x,y>.
> 
>   2. But since a 0-adic relation would not have
>      any tuples in its denotation, there would be
>      no way to evaluate an expression (p) to T or F.

No, see below.

> However, it dawned on me that the expression (p)
> would be true iff the denotation of p included a
> tuple of the same length as the list of arguments,
> namely, the tuple < > of length 0.  If (p) were
> false, then the tuple < > would not be in the
> denotation of p.

Good intuitions, John -- the model theory already works that way! ;-)
Syntactically, at atom is defined to be either an equality or a term
with two parts -- a predicate and a finite (hence possibly empty) term
sequence.  Semantically, an atom is true just in case the *sequence*
consisting of the semantic values of the terms in the term sequence, in
order, is in the relational extension of the predicate of the atom.
"(p)" is therefore an atom (in the CL instance KIF) with an empty term
sequence.  Hence, according to the model theory, it is true just in case
the empty sequence is in the relational extension of "p".

>   1. We need to support seqvars of length zero.

I think you mean sequences of length zero -- we've already got them.

>   2. There may be some cases where the only argument of a relation is
>   a seqvar.

That's already accommodated in the syntax.

>   3. Therefore, expressions of the form (R ...x) will occur, and the
>   model theory must be able to handle the case where ...x has length
>   0.

If what you mean is that the model theory must handle cases where "...x"
takes the empty seq as a value, again, it already works that way!

> This seems to imply that 0-adic relations must be supported by the CL
> model theory.

Done! :-)

-chris