[SCL] Quantifying over propositions

[John F. Sowa]

Pat,

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.

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.

This seems to be a very natural generalization of
the current CL model theory, and it also seems to
be necessary to support sequence variables:

  1. We need to support seqvars of length zero.

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

  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.

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

A final point to note is that Boolean operators with
0 arguments are already supported, namely (and) and (or).
There doesn't seem to be any reason not to support 0-adic
relations, which could then be interpreted as propositions.
(And 0-adic functions would be constants.)

John