[SCL] Concrete embedding proposal to TFOL (GOFOL, SFOL)

[Tanel Tammet]

Hi,

While Pat and Chris are busy working out the finer points of the
semantics of SCL, I have been a bit worried about the practical
usability of  SCL by ordinary TFOL (GOFOL) theorem provers.

In my understanding these systems do need an embedding
(transmogrifying, as Chris put it :-) of SCL to TFOL.

In order to check out whether my intuitions about SCL
coincide with other people I wrote such an embedding
of SCL to TFOL (named SFOL for "standard FOL" in
the following).

The embedding is nothing fancy: it is completely
traditional and intuitive, except for (perhaps) the
details of translating equality, where we have had
(and probably still have) different viewpoints.

Please have a look at the following and check out
whether it is basically this embedding you have had
in mind. I do not guarantee you won't find any errors
or omissions.

I have not put the finer extensions of SCL like tuple variables
and integer  types in the embedding. Adding these should
be the next step after we agree on the basic embedding
(the one below or a modified form of it).

The side issue associated with this embedding (whether
exactly this one or, if modifications are proposed, the
modified version) is that IMHO the pure SCL semantics
should, in some sense, match the embedding. In case
the SCL semantics turns out to be principally different
from the embedding, then we should either change
the embedding or SCL semantics.


Mapping SCL formulas to SFOL
--------------------------------------------------

In order to facilitate the use of  standard first order predicate 
calculus (SFOL
in the following)  for proving theorems presented in SCL, we define a 
mapping
M from SCL to SFOL.

This mapping holds both in cases a syntactically correct SCL formula F
 is also a syntactically correct SFOL formula and in cases where F is not
a  syntactically  correct SFOL formula  (for example, if F is a formula
"forall x. x(x)" then F is  a correct SCL formula but not a correct SFOL 
formula).

In other words, the mapping treates SFOL formulas in the same way as
any other SCL formulas: SFOL formulas are simply a subset of SCL formulas.

The result of the mapping is intended to be usable by SFOL theorem
provers. Obviously, the provers may (and do) use their own conversion
mechanisms and special machinery (equality handling is a typical example).
Such further modifications by provers are OK if the crucial properties 
detected
by the provers (for example, satisfiability and (for some provers) also 
the size of models)
are preserved.

Observe that the mapping automatically defines a standard FOL semantics
for SCL formulas. The important points of the semantics defined by the 
mapping
(satisfiability, size of models, etc) coincides with a "standard FOL" 
reading
of SCL formulas. In particular, if an SCL formula F is a syntactically 
correct
SFOL formula, then F is satisfiable iff  the outcome of mapping M(F) is 
satisfiable.
Essentially, the mapping M(F) changes only the signature of F, not the 
important
logical properties of F.

The mapping M defined in the following is normative for SCL: this is THE 
mapping
of any SCL formula to SFOL. Mappings which are different from M are not 
correct
SCL mappings. Using only the correct SCL mapping is crucial for 
compatibility
of various SCL concrete syntaxes, ordinary SFOL formulas and translated
forms of various other logic-based languages to SCL. The correct mapping
guarantees that in a conjunction of formulas translated from different 
languages
the subformula components are interpreted correctly.

We will present the mapping M in two parts: the first part defines a mapping
M' from SCL formulas without equality, while the second part extends the
definition of M' to the mapping M, covering also formulas with equality.

The approach used in the mapping for the equality predicate is axiomatic.
Equality predicates are considered to have no intrinsic meaning: their
meaning is explicitly given by the axioms constructed by the mapping.

M': mapping SCL formulas without equality to SFOL
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

SCL contains two distinguished predicate symbols for equality, "=" and 
"scl=",
(their difference is explained in the following section).

Although the mapping M' in the current section is defined also for the
case where a mapped SCL formula F contains predicates  "=" or "scl=",
the mapping M' is incomplete in such cases. If F contains "=" and "scl=",
then the complete mapping M defined in the next section adds the
necessary axioms to the result of M'(F).

In case a mapped formula F in SCL does not contain "=" or "scl=", then M(F)
is equal to M'(F).

Observe that in SCL formulas the terms p and f in the following atoms
p(t_1,....,t_n) and terms f(t_1,....,t_n) may be arbitrary terms of SCL,
not just symbols as in SFOL.

For any atom p(t_1,....,t_n)  in SCL:

if p is not a symbol "scl=" then:
  M'(p(t_1,....,t_n)) := holds_n+1(M'(p),M'(t_1),....,M'(t_n))
if  p is a symbol "scl=" then:
 M'(p(t_1,....,t_n))  := scl=(M'(t_1),....,M'(t_n))

For any term f(t_1,....,t_n) in SCL:

M'(f(t_1,....,t_n)) := app_n+1(M'(f),M'(t_1),....,M'(t_n)))

For any formula c(a_1,....,a_n) in SCL where c is a logical connective from
the set {implies, and, or, not, equivalent} and a_1,...,a_n are atoms:

M'(c(a_1,....,a_n) ) := c(M'(a_1),....,M'(a_n))

For any q(x,a) in SCL where q is a quantifier from
the set {exists, forall}, x is the variable bound by q and
a is the formula in the scope of q:

M'(q(x,a)) := q(x,M'(a))

For any q(x,p,a) in SCL where q is a quantifier from
the set {exists, forall}, x is the variable bound by q,
p is a restriction predicate symbol on x and
a is the formula in the scope of q:

M'(q(x,p,a)) := q(x,M'(p(x)) implies M'(a)


M: mapping SCL formulas with equality to SFOL
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

SCL contains two distinguished predicate symbols
denoting equality:

(1)  =
(2) scl=

Intuitively, "=" is the equality predicate used in SFOL
formulas, while "scl=" is a special, strong equality predicate of SCL.

Thus, in case an SCL  formula F with equality is also considered to
be an SFOL formula (in other words, if we tract a standard FOL
formula in the SCL context), then F contains only = as an equality 
predicate.
No SCL  formula G containing scl= cannot be considered to
be a correct SFOL formula.

The following defines an extension M of the mapping M' to
the case where a formula F in SCL contains an equality (either
"=" or "scl=")

M(F) := M'(F) & M'(equalityaxioms(=,F)) & equalityaxioms(scl=,M'(F))

where equalityaxioms(e,f) is a set of axioms for a distinguished
equality predicate e in an SFOL formula f, computed for e and f in
a traditional way from the signature of f (signature meaning the set of
all predicate and function symbols in f). equalityaxioms(e,f) consist of
three subsets: equivalence axioms, substitution axioms for function symbols,
substitution axioms for predicate symbols.

Equivalence axioms:

forall x. e(x,x).
forall x,y. e(x,y) implies e(y,x)
forall x,y,z. (e(x,y) and e(y,z)) implies e(x,z).

Substitution axioms for function symbols present in the formula f
contain n axioms for each function symbol fsymb in f, where n is arity 
of fsymb
and the position of the variable x (resp y) in fsymb(z_1,...,x,....z_n) 
(resp fsymb(z_1,...,y,....z_n))
is iterated from 1 to n, so that for each fsymb and each position in the 
set {1,...,n} there is
exactly one substitution axiom of the following form:

forall x,y,z_1,...,z_n. e(x,y) implies e(fsymb(z_1,...,x,....z_n), 
fsymb(z_1,...,y,....z_n))

Substitution axioms for predicate symbols present in the formula f
contain n axioms for each function symbol psymb in f, where n is arity 
of psymb
and the position of the variable x (resp y) in psymb(z_1,...,x,....z_n) 
(resp psymb(z_1,...,y,....z_n))
is iterated from 1 to n, so that for each position in the set {1,...,n} 
there is
exactly one substitution axiom of the following form:

forall x,y,z_1,...,z_n. e(x,y) implies (psymb(z_1,...,x,....z_n) implies 
psymb(z_1,...,y,....z_n))

We note that in the definition of a mapping M

M(F) := M'(F) & M'(equalityaxioms(=,F)) & equalityaxioms(scl=,M'(F))

the translation M(F) in equalityaxioms(scl=,M'(F)) cannot contain any
function symbols except  app_i for several arities i, and it cannot contain
any predicate symbols except scl= and holds_i for several arities i.

---------------

 
Regards,
              Tanel Tammet