[SCL] Possible simple scheme for relation-constant overlap

[Tanel Tammet]

Hi,

Here is an example of how we COULD treat the wish
to sometimes overlap relations and constants, and
sometimes not.

I'll explain this (probably nothing new to you) with
all the details on an example I had in the new
standalone MT chapter for the core SCL.

Let us have a formula Ft in TFOL:

-P(c) ? Ax.Q(f(x))

Observe that Ft does have a model with
a one-element domain.

Formula Ft could be converted to SCL abstract syntax
by converting predicates P and Q and function f to constants,
giving SCL formula called Fs1:

Formula_3(And,
Formula_2(Neg,Atom_2(P,c)),
Formula_3(Forall,(x),Atom_2(Q,Term_2(f,x)))

Observe that Fs1 does have a model with
a two-element domain, but NOT with a
one-element domain.

But, if we allow SCL to contain arbitrary tuple constructions
(not currently allowed in core SCL)
then we could transform Ft by converting predicates to
tuple constructors, getting the formula Fs2:

Formula_3(And,
Formula_2(Neg,P_1(c)),
Formula_3(Forall,(x),Q_1(f_1(x)))

Observe that Fs2 is essentialy a "traditional" FOL
formula and, like Ft but unlike Fs1, it does
have a model with one-element domain.

In case we are allowed to have arbitrary tuple
constructors, then (as seen) we have two ways to
convert each term and atom, which is
nice, but also somewhat confusing.
Which way do we choose?

We could follow Chris's advice and do it
by "grammar". IMHO the only practical way
would be to have special syntactic markers in
the transformed-from language, so that, say,
we could have a formula M1:

-P(c) ? Ax.!Q(!f(x))

where ! is not a linear logic operator :-)
but a marker saying that Q and f have to be
converted to tuple symbols, but P is
converted to a constant.

The conversion result of M1 would be:

Formula_3(And,
Formula_2(Neg,Atom_2(P,c)),
Formula_3(Forall,(x),Q_1(f_1(x)))

I do not know what we will gain from
this, but maybe we will.

Let us continue. Next we want to OVERLAP
tuple and constant representation of predicates.

For example, we could want to say that P and Q in the formula

-P(c) ? Ax.!Q(!f(x))

are equal (the same thing) although P is converted
to a constant and Q is converted to a tuple symbol.

What should that mean? It would mean - informally -
that we take the following axiom in SCL core:

Formula_3(Forall, (x),
Formula_3(Equiv,
Atom_2(P,x),
Q_1(x) ))

What problems will we encounter?
The problem that since P is a constant, it is
not related to any arity. Other formulas may
contain P in tuples of different arities, like this:

-P(c) ? P(c,c) ? Ax.!Q(!f(x))

and hence we need also the second axiom, for arity 2:

Formula_3(Forall, (x,y),
Formula_3(Equiv,
Atom_2(P,x,y),
Q_1(x) ))

Overall, it appears that we need an axiom schema (somewhat similarly to
the axiom schema of equality) which can for any concrete finite formula
be instantiated to a finite number of instances, exactly one for each tuple
arity occurring in the formula.

We could take a special module of SCL, defining an axiom
schema called Overlap like this:

Overlap(u,v) := a conjunction for each n in 1...max_arity of tuples in 
formula:
Formula_3(Forall, (x1,...,xn),
Formula_3(Equiv,
Atom_n(u,x1,...,xn),
v(x1,...,arity(v)) ))

where arity(v) is the arity of the tuple constructor.

This axiom schema is definitely NOT expressible in SCL,
but the axiom instances created for each SCL formula
are definitely proper SCL (assuming we allow arbitrary
tuple constructors, of course).

I do not know if all this is any good to have, and rather
suspect that it will make things a bit messy. But, it
certainly gives extra capabilities in principle.

I have simply tried to write the example down in
way that I can understand, led by intuition from
Chris's latest presentation (which I could not
fully understand yet).

Chris, would that schema be similar to what you
had in mind and wrote in your last 1.02 presentation?

Regards,
Tanel Tammet