[SCL] Possible simple scheme for relation-constant overlap

[pat hayes]

>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.

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?

>
>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

?

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

>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,

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))

>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
>
>
>
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes