[SCL] Proposed additions to the SCL draft standard

[Chris Menzel]

Hi Tanel,

Will address your response to my comments about annotations separately
later.

> >> Chris mentioned that once we encode predicates using the App/Pred
> >> functions, the formula (forall x. P(x) & -Q(x)) & (forall x,y. x=y) is
> >> NOT valid, while it IS valid in the standard, non-app/pred semantics
> >> of FOL.
> >
> ...Meant "satisfiable". The formula above
> is not satisfiable in SCL, while it is satisfiable in FOL
> (a domain with just one object suffices for satisfiability).
> 
> > Perhaps you are thinking of
> >something like the following:  
> >
> >     (implies
> >        (forall (?x) (iff (P ?x) (not (Q ?x))))
> >        (not (forall (?x ?y) (= ?x ?y))))
> >
> >which is invalid in standard FOL but valid in SCL.  ("P" and "Q" both
> >denote something in SCL, but since those denotations have different
> >extensions, they must denote distinct things.)  I agree we need to think
> >carefully about these issues.  The purpose of the "Ind" predicate was
> >basically to restrict quantifiers to non-relations to get the right
> >sorts of correlations with standard FOL.  Thus, the result of so
> >restricting the quantifiers in the formula above:
> >
> >     (implies
> >        (forall (?x Ind) (iff (P ?x) (not (Q ?x))))
> >        (not (forall (?x ?y Ind) (= ?x ?y))))
> >
> >
> >is NOT valid in SCL.  But again, this is worth a lot of thought.  We
> >need in particular to convince ourselves of the advantages of allowing a
> >"free" syntax in which predicates can occur as arguments to other
> >predicates.
> 
> Another way to look at it is the following question:
> which kind of these two kinds of quantifiers:
> - (forall (?x Ind) ...
> - (forall (?x) ...
> should be the DEFAULT (ie, shorter to express)?

I have made some changes that I believe make this whole question moot.
Let's note a couple of things.  First, our constraints on an SCL lexicon
*permit* but do not *require* that predicate constants also be
individual constants.  Second, I've made sequence variables optional.
(Consider this a proposal, not a decision by fiat from On High, but it
seems pretty trivial to me).  The effect of these two features is that:

(*)  Every traditional first-order language is an SCL language.

Just keep your predicate constants, function symbols, and individual
constants mutually disjoint and don't include sequence variables and
there you go.  You'll have a fully conformant SCL language that is
completely traditional.

Now, an important change -- better, correction -- I've made to the 1.0
document is to clobber the semantic condition that relations constitute
a subset of the individuals in every interpretation of an SCL.  That
does not square with our syntactic conditions above.  The appropriate
condition is that we simply *permit* (partial or complete) overlap
between the two classes; but they can be disjoint, and indeed that would
be the most natural sort of interpretation for traditional first-order
languages.

Semantically, this has a very important consequence for the sorts of
examples we've been looking at:

(**)  For a traditional first-order SCL language L, the class of 
      valid (hence, satisfiable) formulas relative to SCL model theory 
      is exactly the class of valid (hence, satisfiable) formulas
      relative to standard "Tarskian" model theory.

Thus, we can't in general sensibly talk about whether or not a given
formula is or isn't satisfiable independently of a specification of the
signature of the language it purports to belong to.  So, for instance,
In a traditional first-order SCL language in which "P" and "Q" are
predicates only, 

(***)  (forall x. P(x) & -Q(x)) & (forall x,y. x=y)

IS satisfiable; it will in particular be true in interpretations in
which (i) relations are not in the domain of individuals (and hence not
in the range of the quantifiers), (ii) there is only one individual e,
and (iii) e is in the extension of the denotation of "P" but not in the
extension of the denotation of "Q".  The formula is only unsatisfiable
in SCL languages that include some type-freedom and, in particular, that
stipulate that "P" and "Q" both pull double duty as predicate constants
and individual constants.  An interpretation for such a language will be
forced assign a relation to "P" qua predicate constant and an individual
to "P" qua individual constant, and the only way it can do that (since
the denotation function is a *function*) is to assign something to it
that is both a relation and an individual; likewise for "Q".  Hence, any
interpretation of such a language in which the denotation of "P" must
differ from that of "Q" -- as would be required by the first conjunct of
(***) -- will have to contain at least two things (namely, at least, the
denotations of "P" and "Q").

So I don't think any of the fears you expressed are warranted, Tanel:

> This means that it is very hard to use SCL for encoding standard
> logical problems, including a large part of the thousands of problems
> in TPTP, used extensively in the ATP community. People cannot use Id
> in these contexts: they'd have to define their own equality not
> present in SCL and not axiomatisable in pure SCL alone.
> 
> This might be survivable, but is really unpleasant, since it
> unnecessarily limits or confuses our audience.

To the contrary, everything remains as it was for traditional
first-order languages.  Of course, if folks want to start incorporating
sequence variables or some of the type-free features available in SCL,
then of course they will have to alter and extend their automated
reasoners accordingly.  But SCL leaves the existing environments for
first-order ATP etc unperturbed.

SCL 1.01, which incorporates the changes noted as well corrections of a
number of errors spotted by Tanel's eagle eye, can be found at the usual
place:  http://cl.tamu.edu/docs/scl/scl-latest.html .

-chris