[SCL] Re: SCL 1.02: more reasons to avoid ind pred separation

[Tanel Tammet]

Hi,

pat hayes wrote:

>> As far as I understand, if the user wants
>> to keep clear separation of ind/pred constants,
>> then there are several obvious, intuitive ways
>> to do that.
>>
>> First, one can simply NEVER USE a non-constant
>> term in the first position of the triple.
>>
>> No axioms of the kind
>>
>> (forall x. reflective(x) <=> forall y. z. x(y) <=> z(y)).
>>
>> and no terms in the first position, ie no f(x)(y).
>
>
> But, but.  Consider this *syntactic* case simply as a grammatical 
> restriction on the SCL language - case A - and as a standard FOL in 
> its own right - case B.  Are these the same case? We used to think so, 
> but that was exactly Horrock's point with his example: they are not 
> the same, if we use the 'simple' version of SCL in which all symbols - 
> even those in relation position - denote something in the universe.

Of course, but as I have pointed out earlier, the Horrocks problem stems 
from misinterpretation
of the equality. It happens if you define equality for full SCL and 
expect it to work the
same way as equality works in FOL, where no substitutions into predicate 
symbols can
be done.

The Horrocks problem is about how you are supposed to axiomatise a 
specific predicate,
NOT about the semantics of the core language. The semantics (model 
theory) should not
care about how exactly I am going to axiomatise equality, plus, list 
membership, etc etc.

Now, IF all the atoms in your formulas contain only constant symbols as 
first elements
of any term or atom tuple, then the satisfiability properties of your 
formulas ARE
exactly the same as satisfiability properties of SFOL formulas looking 
like your formulas.

Meaning that

IF

a) all your SCL formulas contain only constant symbols as first elements
   of any term or atom tuple,

b) you translate your SCL formulas to SFOL in a generally incorrect way
   like this:  all SCL atoms like (foo (bar x a) y) are translated  to
   foo(bar(x,a),y) in SFOL.

   Let us call this "subset-translation" of SCL to SFOL, and the correct 
translation
   as "correct-translation" of SCL to SFOL.
  

c) there is NO equality or any other predicate or function symbol with 
special
    meaning in the language.

THEN

satisfiable_in_SCL_MT(SCL formula) if and only if 
satisfiable_in_SFOL(subset-translation(SCL formula))

Proof idea:

We know that by the building of SCL MT (if we do it right, of course!)
satisfiable_in_SCL_MT(SCL formula) if and only if 
satisfiable_in_SFOL(correct_translation(SCL formula))

Hence we need to show that for our fragment of SCL (conditions a and c 
above)
satisfiable_in_SFOL(correct_translation(SCL formula)) if and only 
satisfiable_in_SFOL(subset-translation(SCL formula))

which  is easy to see: for our fragment, any resolution refutation of
correct_translation(SCL formula)
can be converted to the resolution refutation of
 subset-translation(SCL formula)
and vice versa.

Why (on the example):

atom_3(foo,term_3(bar,x,a),y)) in the first refutation tree behaves 
exactly in the same way as
foo(bar(x,a),y)  in the second refutation tree. Why: since any first 
argument of atom_i and term_i
is a constant, we could rewrite
atom_3(foo,term_3(bar,x,a),y))
to
atom_3_foo(term_3_bar(x,a),y)
merging the tuple symbol and the first argument symbol.

Now, you both know this (Pat knew this before I was born :-) but IMHO 
you got
frightened by the Horrocks example, which (properly) shows that 
everything is
not trivial and one has to take care.

Now, one has to take care in WRITING THE AXIOMS for various predicates
and function symbols, equality being one example.

Summary: do not put equality into the core MT and everything is fine, even
the Horrocks examples. Put equality into the equality module and define
it properly, with one full equality for SCL and a weaker equality, 
corresponding
to the SFOL equality.

The question of DENOTING something in the universe is IMHO not
an essential issue. In my formalist view, there is no platonic universe
out there for logic. There is a MT which is an algorithm for computing
truth values, and universe is a construction which happens to be used in 
the MT algorithm.

We may, however, also want to construct an algorithm which constructs
models.

BTW, I have one of the strongest model building programs out there,
regularly winning the yearly CASC satisfiability checking categories,
so I happen to know the model computation aspects :)
I have actually went through all these issues in my real programs,
sometimes using the SCL-kind of encoding of SFOL, and wanting
to both find non-satisfiability (easier) and satisfiability
(non-computable in the general case, hence harder) for both
SFOL and SCL-style-encoded SFOL.

I'll extend on this a bit, for the case where we have finite
models.

It is of course true that in
atom_3(foo,term_3(bar,x,a),y))
both foo and bar denote something in the universe, in any intepretation, 
while in
foo(bar(x,a),y)
they do not.

Hence, for example:
In SCL,
atom_2(foo,a) & -atom2(bar,a)
does not have one-element models, it only has two-element (and 
three-element, etc models).

The two "main" models (others are isomorphic to these two, by renaming 
model elements) are:

foo=0
bar=1
a=0

and the model

foo=0
bar=1
a=1

while in SFOL
foo(a) & -bar(a)
does have a one-element model where

a=0

and foo and bar can be presented as
tables of truth values, in this case,
one row (for element 0) only.

So what?

The truth values for sentences computed by MT are the same (model
sizes is a different issue).

Now, if you do not like that in SCL the example above does not have
one-element models, then you can take the SCL model and filter
out the SFOL-style model, simply by removing the  interpretations  of
foo and bar. Then you get from the two SCL models above these
two models:

a=0
and
a=1

which are isomorphic, hence we can safely throw away all but one
of them, if we want. This is easy.

To summarise SFOL finite model building from SCL models:
as far as I understand, in case we actually want to compute models,
then we can easily transform an SCL model to SFOL model (again, I assume
we have an SFOL-corresponding fragment of SCL).

For a naive universal model builder, however, it will be harder to
compute the full SCL model than the SFOL model (more symbols
to interpret, hence more to check). However, we can program
the model builder in a way that if it checks that we really
have an SFOL-corresponding fragment (a trivial check to
do) then it uses this information and computes the SCL model
as if it would compute the SFOL model, and later, if we want
to, it can trivially add the foo and bar predicate symbol
interpretations, mapping each to a different element in
the model.

What gets a little harder in this case (converting SFOL models
to SCL models): in case we have a finite model, then
 we may need (as in the example above) to increase the size of the model
for SCL and intepret all the function and predicate symbols
 (in SCL case, atom_i and term_i). These interpretations can be built
from the SFOL interpretations of predicate and function
symbols (foo and bar predicates in the example).

For example:

a=0 (given from SFOL model)

foo=0 (added)
bar=1 (added, along with the new element 1)

atom_2(0,0)=true (obtained directly from foo(0)=true in SFOL model)
atom_2(0,1)=true (extended from foo(0)=true in SFOL model)     
atom_2(1,0)=false (obtained directly from bar(0)=false in SFOL model)
atom_2(1,1)=false (extended from bar(0)=false in SFOL model)

The nontrivial rows above are the "extended" rows. Why take "true" and 
"false"
as values? There is nothing in the SFOL model which directly indicates
the suitable value. I am pretty sure (but this needs a proof,  and I am
yet not 100% sure) that  in any row where the argument set contains
new, added elements of the domain, we can take a truth value from a
known row where we have element 0 instead of any new domain element.

Observe that in case we we have an infinite model, then the SCL->SFOL model
conversion algorithm is much simpler: no need to extend the domain
(infinite anyway), simply map each predicate and function constant
to a different element in the domain, and construct the
atom_i and function_i interpretations from the corresponding interpretations
of predicate and function symbols in the SFOL model. In case the
first element of atom_i and function_i does NOT correspond to
a predicate or function symbol element in the domain, take the
next one cyclically (if we have two predicates foo and bar, then their
elements are
foo=0
bar=1
atom_2(0,i) obtained from foo(i)
atom_2(1,i) obtained from bar(i)
atom_2(2,i) obtained from foo(i)
atom_2(3,i) obtained from bar(i)
atom_2(4,i) obtained from foo(i)
atom_2(5,i) obtained from bar(i)
etc

All of this has to do with the model building (different from refuting
or proving) aspects of the SFOL-corresponding subset of SCL, hence
it it is pretty specific and should not be of general interest.

If somebody _really_ wants, then I could write out the technical model
building aspects of SCL compared to SFOL in a separate
appendix chapter of SCL spec.  The principal issues
are outlined above here. But, I'd rather hope we do not really
need this technical appendix :)

> I am practically certain that we can present the simple approach
> in the SCL spec in a way that is comprehensible and does NOT
> look like a weird hard-to-understand hack.
>
> It is just a matter of the style or approach of presentation,
> rhetorics, if you will.


 > No, it is more than just that. One has to somehow get the model 
theory to come out right, without begging the question.

 > Put it very simply indeed. We have 2 SCL customers, called H and P, 
and the task is to define SCL syntax and model theory and > a notion of 
a sublanguage so that both of them can be satisfied simultaneously.

 > H wants to just use a conventional FOL subset of SCL - we can easily 
define that syntactically as a sublanguage - and have it
 > have the conventional FO model theory, and he wants to use equality.  
So he wants
 > (x y)((x=y) & P(x)  & not Q(y))
 > to be consistent.

 > P wants to use full SCL, so that he can write things like
 > (r)(symmetric(r) iff (x y)(r(x,y) iff r(y,x) ) )
 > and have them means what they seem to mean.

 > What we need to do is to give a semantics for =, relational atoms and 
the universal quantifier which can satisfy both of these
 > guys at the same time.  Its not a trivial task, since P needs things 
in his universe that will screw up H's intuitions if they are in
 > his universe. How can we tell a single story which satisfies both 
requirements on what is in the universe? Chris' is the only one
 > on the table at the moment, as far as I know.

Before arguing on that, I'd rather wait until I see the new spec draft 
Chris should send us today.
Maybe it looks understandable and does not introduce extra complexities, 
which would be fine.

Writing these recent messages I have taken a risk that I may be 
attacking a straw man.

But maybe not: if the Chris new MT would be simple, he would have 
managed to produce
the new spec in time. He is now BADLY overdue, extending his deadline 
every few days,
explaining that SCL->SFOL translation became a bit tricky. This is why I 
became worried.

Regards,
               Tanel