[SCL] Folding unnecessary [was: Re: Update to SCL-related work]

[Tanel Tammet]

Hi,

Pat Hayes wrote:

> Tanel, a quick amplification of a point in the last email:
>
>> It runs deeper than this. Its a problem with the size of the 
>> universe. Its true that without equality there is no way to 
>> axiomatically enforce a finite universe, so the examples all use 
>> equality, but the meta-theoretic point they illustrate holds true 
>> even for the logic without equality. What we want is that if some SCL 
>> text is GOFOL, then its FO models are among its SCL models. The 
>> Horrocks sentences illustrate the objection that with the former SCL 
>> semantics, this is not the case (because the relations had to be in 
>> the universe).  It would still be a valid objection in the logic 
>> without equality. That is what was unacceptable (and is now fixed), 
>> not a specific equality issue.
>
>
> To illustrate, consider the single FO sentence in SCL notation
>
> (P a)
>
> and its embedding into FOL using the ECL format:
>
> Atom_2(P, a)
>
> and consider the FO-valid inference rule of existential generalization 
> (in an ND system), which applies to the latter to produce the valid FO 
> consequence
>
> (exists (x) Atom_2(x, a) )
>
> which is NOT a correct translation of any FO consequence of the 
> original sentence. So the translation fails to accurately capture FO 
> logic.
>
> This exhibits the issue without using equality, and illustrates why it 
> is essentially a matter of what is in the universe. By using the 
> relation names as true FO names in a classical FO framework, we have 
> required them to denote something in the universe of quantification.
>
Well, you are certainly right.  But I doubt that the folding semantics - 
at least in
the way it is currently presented in the SCL draft - is the solution.

I have some notes and a longish (yet trivial) suggestion on the issue.

1)  Probably the size of the domain of formulas does not really matter,
     as long as the satisfiability property is exactly the same.

     In particular,  the very moment you introduce integers or strings
     or lists, the domain becomes infinite, and never returns to finite
     spheres. Horrocks sentences fail immediately, also for GOFOL,
     etc.

     Now, do we really expect to use SCL much in the contexts where
     no integers, strings or lists are defined?

2) We deviate from traditional FOL the very moment we declare that
      you are allowed to quantify over predicates  and function symbols.
  
     There is no escaping that. Differences in semantics have to be
     there, it is completely hopeless to hide the differences by complex
      semantical schemas: this way we simply hide the semantics from
     the eyes of the reader, but we cannot change the basic fact that
     there are some differences.

3) Let us suppose that we want pure, unchanged, traditional FOL
    back into SCL, with exactly the same semantics and everything.

     Fortunately, we know that it is already there. The "abstract syntax"
     of ECL, presenting traditional KIF syntax (and (P x) (Q (f x))) as
     Formula_3(and, Atom_2(P,x), Atom_2(Q, Term_2(f,x)))
     is traditional FOL itself.
 
     SCL really amounts to a terminological suggestion: the suggestion
     to call the first arguments of traditional FOL atoms and terms
     as "predicate symbols" and "function symbols". We have done
     nothing more than introduced slightly nontraditional terminology.

     What then prohibits us to use the traditional FOL, when the SCL
     abstract syntax already IS traditional FOL?  Just the conventions
     of the concrete syntaxes: in abstract syntax I could write
     Formula_3(and, P(x), Atom_2(Q, Term_2(f,x)))
     instead of
     Formula_3(and, Atom_2(P,x), Atom_2(Q, Term_2(f,x)))
     but the KIF concrete syntax does not allow this: it forces me
     to write
     (and (P x) (Q (f x)))
     which is always translated to
     Formula_3(and, Atom_2(P,x), Atom_2(Q, Term_2(f,x))).

     It seems that if we want to allow traditional FOL to be used
     in SCL (with exactly traditional semantics), then we ONLY
     need to allow this in concrete syntaxes.

     We already can write
     traditional FOL in the abstract syntax (provided we just drop
     the explicit requirement that the only term/atom constructors
     are called "Term_1, Atom_1, Term_2, Atom_2, ..." which
     is very easy to drop (only the equality axiomatisation needs
     a slight modification)). It has traditional FOL semantics,
     with no changes whatsoever.

      How to allow traditional FOL in concrete syntaxes, then,
      without making the SCL-style function/predicates inconvenient
      to write by forcing abstract syntax Term_N and Atom_N
      to be used?

      Clearly, this is a SYNTACTICAL, not semantical issue.
     
      We should allow two kinds of terms/atoms: those translated
      into Atom_2(P,x) and those translated into P(x).

      There seem to be several options:

       a) Declare that P in the function/predicate position should be
           always translated in the P(x) way, not Atom_2(P,x) way.
           This is possible,  but works very badly when SCL text from
           different sources is integrated.  Essentially, it would be
           a declaration for the parser, and does not have anything
           to do with semantics.

        b) Use two different application syntaxes. We could suggest
             people to use P(x) or (P x), translated to Atom_2(P,x) in
             abstract syntax,
             and to use P[x] or [P x], translated to P(x) in abstract
              syntax.

             Only power users would use the P[x] syntax, and they
              would not mind. Most people would never understand
             or use the P[x] construction.

             We could even have a special "power user" concrete syntax,
              with the () and [] roles switched, where P(x) or (P x) is
              translated to P(x) in abstract syntax,
             while P[x] or [P x] is translated to Atom_2(P,x).
    
        Regardless of which option we use, questions will be rised
       about relations  between P(x) and P[x], translated to
        Atom_2(P,x) and P(x) in abstract syntax, There are several
        options to choose from:
 
        a) Saying that there are no relations whatsoever. P stands for
          completely different things in P(x) and P[x]. I would really
          prefer that option, since anybody sophisticated enough to
          use BOTH P(x) and P[x] would understand the differences
          perfectly and would have a good reason to have two different
          results.


        b) We could axiomatise that Atom_2(P,x) is always
             equivalent to P(x). This is, of course, perfectly possible:
            it would be an axiom schema similar to what we have to
           use to define equality.

           I suspect that this would be similar to the folding
           semantics (is it?) but would have an important advantage
           of - by virtue of being axiomatised - not changing the
           underlying semantics a bit.

            I do not think that it makes sense to axiomatise this,
            but, well, we could do it if we really wanted to.
          
To summarise: I think you have made a good point,
but the folding semantics is not an answer.

Instead, there is a trivial, correct answer which simply
begs to be used and even offers several
options to choose from.

The only "problem" with this answer is that it is
embarrassingly trivial and states very clearly that
SCL is nothing clever and not a single new
logical idea has been introduced.

I really think that this is what horrified both
you and Chris. You should not be horrified,
it is a virtue to avoid new logical ideas in
SCL, not a sin.

SCL is not a project to invent a new logic
(join type theorists, linear logicists or even
DL people for that!), but to use good old
stuff for new purposes.

Whenever we have a perfect, trivial answer to
a question, it is a sin to forget it and
invent your own complex answer instead :)

Regards,
              Tanel Tammet