[SCL] Obvious SCL spec ideas for extensions

[Tanel Tammet]

Hi,

pat hayes wrote:

>> For example, a natural extension idea for core SCL
>> is to allow people to write tuples of OTHER types
>> than Atom_i and Term_i. These tuples could be,
>> like, say, Man_1 and Father_2, ie ordinary
>> TFOL predicates. In order to bring them in
>> we would simply need to extend the abstract
>> syntax and concrete syntaxes (the latter must
>> then contain special markup). There is even
>> no need to modify the current quantifiers. The
>> Man_1 and Father_2 type of tuples would
>> simply be disjoint from predicates as constants.
>
>
> Why? If I follow you here, these seem remarkably close to the 'role' 
> syntax for predicates, suggesting a further unification. BUt maybe I 
> am not following you. Can you give a simple example?

The example actually came in a later message. I have copied
this message and pasted it into the following.

Of course, I am not sure that the schema in the following
is what you have had in mind, but it seems to be
fairly intuitive and relatively simple.

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

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 the examples did) 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,...,x_max(n,arity(v)),
                  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).

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

Regards,
                 Tanel Tammet

-------------- next part --------------
Skipped content of type multipart/related