[SCL] Obtaining an improved SCL embedding to FOL

[Tanel Tammet]

Hi Chris and Pat,

As you have observed, I am regularly trying to
get your minds off the SCL model theory - for just
a short moment - and into writing the SCL-to-FOL
embedding.

As I understood, you were not sure that the simple
embedding I scribbled down last week was the
embedding you really would like to see (especially
the equality part).

Hence, how about writing a new embedding? You
could even take the text from the last week and
simply modify it in the suitable direction.

Most of the feedback to Pat's question directed
to FOL prover hackers has arrived by now.

I admit to having some suspicions about the possibility
of finding a better embedding than the obvious one
plus two equalities.  Of course, I am not sure
of the impossibility of a better embedding either.


Regards,
           Tanel Tammet