[SCL] Possible simple scheme for relation-constant overlap

[Tanel Tammet]

Hi,

>> 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.
>
>
> You are losing me. Do you mean that these markers are part of the SCL 
> syntax? If so, forget that idea. If not, what are you saying?

No, these markers are NOT part of SCL syntax. They could be part of  
some concrete
SCL syntax, but not SCL abstract syntax itself. The sentence
with markers

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

is assumed to be in a concrete SCL infix syntax.

The markers are simply a way to say (in some concrete syntax) whether
a predicate in the concrete syntax is meant to be a constant in the
SCL abstract syntax or a tuple constructor in the SCL abstract
syntax (the latter correspond to traditional FOL predicates).

In any concrete syntax there should be a way to indicate which
exactly we mean.

Now, I am ASSUMING here that we want to have two
kinds of predicates in SCL abstract syntax (varyadic/matchable with vars,
and non-varyadic/traditional predicate). This assumption is not my 
preference,
in fact, but I understood from your and Chris's
recent writings that you think this would be desirable.

>>
>> 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?
>
>
> Yes, what does it mean? Clearly 'P' and 'Q' are not the same piece of 
> syntax. So you must (?) be saying that they co-denote, ie that P=Q 
> (note, no quote marks) ?  But then why did you not write that, ie:
>
> -P(c) ? Ax!Q(!f(x)) & P=Q

No, I cannot write this, since equality predicate normally
assumes that both arguments of the equality are of the same
type (typically, terms, of course). !Q in the example is not
a term in the SCL abstract syntax (it is a tuple constructor, ie
ordinary TFOL predicate) while P is a term (a constant).

So we cannot write they are equal, at least not by
using any traditional equality predicates.

>
> ?
>
> Overall, I guess I don't follow what it is that you are saying here.


Well, it was my way of  trying to understand what you
and Chris were saying we need. Tried to write a concrete
example using SCL abstract syntax, which can be read
as TFOL. Maybe I did it all wrong, and then I'd appreciate
if you could write an example of how you see the
two kinds of predicates should (a) be used and (b) mapped
to TFOL.

>> 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,
>
>
> If you put that arity argument first, it would be:
>
> Overlap(u,v) iff ( forall (@x) (Atom(u, @x) iff v(arity(v), at x))

I guess so. Seqvars do help for these kinds of axiom schemas,
as you indicated here (did not think about using seqvars when
I wrote the example).

The whole point of my attempt was creating an example
so that I could understand how these two kinds of predicates, sometimes
overlapping, sometimes not, could be presented with
SCL abstract syntax (readable as TFOL) and axiom schemas.

This kind of presentation does not necessitate any unconventional
tricks with MT: Essentially, traditional FOL MT should suffice.

Regards,
               Tanel Tammet