[SCL] Re: Observat

[Tanel Tammet]

Hi,

Thanks, Pat and Chris, for clarifying the political picture.

As Pat noted, in the view of ideologies there are clearly
different camps as well. Chris represents the semantics-first camp,
while I represent a somewhat formalist camp (with a specific
tendency to understand different languages via their 
translation to minimal (no equality, nothing fancy) TFOL). 

When you program, you manipulate symbols. No semantics
visible, except as a mental framework you sometimes check in
order to be sure that the symbol manipulations are OK.
This tendency is probably widespread among prover hackers.

Considering the *practical usability* of SCL and 
such in systems for logical inference, I have an
opinion that the "embedding to TFOL", whichever
way we do it, is absolutely necessary, while 
"pure semantics" or "semantics not via
TFOL" is nice to have, but not as crucial as the
semantics via a translation to minimal TFOL.

Most prover hackers would surely check the TFOL embedding
algorithms first, pure semantics second.

Simply because we need to do the translations to TFOL
in order to use SCL and the like in TFOL provers. 
These translations do create semantics as well, of course,
hence they are (in a weak sense) sufficient.

Any time a formula given to a TFOL prover contains subformulas
like "R(P) & (forall x,y,z.  R(x) <=> (x(y,z) <=> x(z,y)))"
we just have to transmogrify (as Chris nicely put
it) to App/Pred . As far as I understand,
no clever semantics will help to avoid this.

I am no fan of transmogrifying. I'd be happy to
avoid it if possible. But I see no way to
always avoid it when we want to feed formulas with
freely used variables to a TFOL prover.

We can, of course, identify subclasses of transmogrified
formulas where we can de-transmogrify:

- A trivial case (no variables at predicate positions) 
  falls there, as well as

- formulas where variable-as-predicate occurs in 
  "nice definitions" like this one:
  "R(P) & (forall x,y,z. R(x) <=> (x(y,z) <=> x(z,y)))". 

  Here we could substitute P into x in the definition,
  remove the definition, and all is well. 

I doubt that we can remove App/Pred in the general case,
though.

Now, once we sometimes have to transmogrify, it would be
IMHO cleaner and better to always transmogrify.

Here is a scenario:

Consider two files: 
- F1 in "simple" TFOL where transmogrification seems superfluous
- F2 in "a variables-at-predicate-positions" language. 

We may well give a semantics where there
is no need to transmogrify F1 with the
App/Pred encoding. 

However, once you want a TFOL prover to check whether 
a conjunction F1 & F2 is satisfiable,
you have to transmogrify also the F1 part.

Which says to me that once you read and parse F1, better
transmogrify it at once: then you can store everything
in the same format. Much cleaner than keeping two languages
in the guts of the implementation.

Transmogrifying F1 the first thing after we see it is
not as bad as it looks even in case we will then be
asked "is just F1 satisfiable?". F1 (with no variables
in the predicate/function position) falls into a very
easily detectable subclass of transmogified formulas
and can be quickly "re-transmogrified" before feeding
to the TFOL prover.

I just cannot believe we can both eat and keep the
proverbial cake of having variables a predicate positions,
at will, yet avoiding transmogrifications.

Regards,
      Tanel Tammet