[SCL] SCL basic consensus badly needed

[pat hayes]

>Hi SCL-ers,
>
>We need to build a consensus on some
>basic issues before we can sensibly
>move on.
>
>Please, everybody: let us have a serious
>look on SCL <-> SFOL (standard FOL)
>conversion this week and let us try
>hard to reach a consensus on this
>by the end of the week.

Tamel, sorry Ive been so out of the loop, hope you have not become 
too discouraged.

>
>What is necessary:
>
>A) Have a look at
>    http://philebus.tamu.edu/pipermail/scl/2003-June/000269.html
>
>    I'll give some additional brief notes
>    in the rest of this mail:
>    - what to look for
>    - how to understand the proposal
>    - the issues where people have had different opinions
>
>B) Make up your mind on the mapping
>    "SCL without equality" <-> "SFOL without equality"
>    and please tell your standpoint in an answer
>    to this email.
>
>    This is (almost) trivial, of course.
>
>    We do not have consensus there yet, since:
>
>    Although we need a "holds" predicate and an "app" function
>    (to be more exact, a separate "holds" for each
>    arity, ie an infinite supply of "holds_1","holds_2", etc)
>    to translate SCL formulas like "forall x. x(x)"
>    to SFOL as "forall x. holds_2(x,x)",
>    it would seem that in simpler cases we
>    could avoid inserting "holds".
>
>    For example, one could wish to translate SCL
>    formula "forall x. p(x)" as "forall x. p(x)"
>    in SFOL, and not as "forall x. holds_2(p,x)".
>
>    However, I am convinced that having such a
>    translation schema with "exceptions" is a very
>    bad idea and is not usable in practice, for
>    various reasons. Additionally, it will not
>    buy us anything performance-wise.

? Surely it does in many cases, with engines which use indexing on 
relation names. In fact that is the only case I have seen made for 
not immediately converting the unification algorithm to handle the 
'higher-order' constructs directly.

>
>    I am suggesting using a uniform translation
>    schema, ALWAYS inserting "holds" and "app".
>
>    QUESTION: Would you agree to that or not?

No, unless we are forced to.  I think we can do (have done?) better, 
in the following sense.

You asked the question using a 2-headed arrow <-> but there are 2 
translations involved.

SFOL -> SCL is trivial as SFOL *is already* SCL. I think this is 
important and needs to be preserved in our account: SFOL is a subset 
of SCL.  SCL -> SFOL is therefore an embedding, and requires use of 
the holds/app embedding to cover all of SCL syntax.  The result, if 
we round-trip, is that SFOL->SCL->SFOL  amounts to the SFOL->SFOL 
mapping which you get by rewriting SFOL in SFOL using the holds/app 
embedding (which of course has always been an option, though 
unmotivated.)

Actually we could define the SCL->SFOL mapping in two ways, as you 
point out. One way is to leave any SFOL syntax alone and to embed 
only non-FOL SCL using holds/app. The other is to apply the holds/app 
uniformly, which is what I was assuming above. I can see the merits 
of both ways of defining the translation, but like you, lean towards 
the uniform technique as a 'standard'. However, we could observe that 
if you start in FOL, then the SCL results and standards apply to you 
without change, so there is actually no need to apply any complex 
self-embeddings in order to use a FOL engine on SCL that happens to 
be FOL already.

On re-reading this I see it may be confusing. What I mean is that we 
should indeed define a mapping from full SCL to FOL along the lines 
you suggest, ie simple and applying uniformly to the entire syntax. 
However, I think we can also observe that SFOL is a well-defined 
sublanguage of SCL - I expect we will have several such sublanguages 
- and that it is perfectly OK to work entirely within this 
sublanguage and still be using SCL correctly. So to conform to the 
SCL spec while using FOL is not to necessarily use the full-SCL -> 
FOL embedding mapping. That is an option for someone who has FOL 
tools and wishes to offer a full-SCL service, for example: but then 
they would need to pay attention to matters like the one you raise, 
of how to handle the 'extra' vocabulary introduced by the embedding. 
No doubt a full writeup of the final document suite should refer to 
this and discuss it in some detail, but I don't see it as being a 
show-stopper or requiring us to do anything as drastic as introducing 
two kinds of equality.

>    If not, please give your arguments and ideas
>    for alternative solutions.
>    If yes, please state so.

see above.

>
>
>C) Make up your mind on the mapping
>    "SCL with equality" <-> "SFOL with equality"
>    and please tell your standpoint in an answer
>    to this email.

I think that with the current version of the model theory, the above 
applies to the with-= case just as it does to the without-= case.

>
>    I'll give a brief explanation of the approach
>    taken in the proposal mentioned at the beginning
>    of this email (please look there for the
>    details).
>
>    We assume that initially we have SFOL without equality.
>    We get equality by explicitly axiomatising a
>    predicate symbol "=".

Ah, but that is a different matter. We have been talking about using 
a logic-with-=, not about axiomatizing equality in a logic-without-=. 
Different issues arise.

>
>    The axiomatisation is traditional, consisting
>    of two parts:
>
>    1) Three traditional equivalence axioms for "=".
>
>    2) Axiom schemas for substituting equal terms
>       to equal terms in formulas.
>       Observe that for each particular SFOL formula
>       F the axiom schemas will produce a finite
>       number of substitution axioms.
>
>       Essentially, a number of axioms is constructed
>       for every function and predicate symbol in F.
>
>    What is the confusing issue which arises:
>
>    What happens now is that in case we first convert
>    an SCL formula to SFOL using "holds" and "app",
>    and THEN create the substitution axioms for
>    equality, then obviously we also create the
>    substitution axioms for these inserted "hold"
>    and "app" predicates and functions.

Quite.

>
>    However, if we look at simple SCL formulas
>    (example, "forall x. p(x)") which SEEMINGLY
>    do not need "app" and "holds" in the SFOL
>    translation, then we have a tendency to overlook
>    that the substitution axioms for "holds" and
>    "app" will be created. These axioms are exactly
>    the source of confusion from Horrock formulas!

Well, Im not sure what your point is here. I mean, tendencies to 
overlook are hardly our business here, surely. We can define the 
mapping so that the results come out correctly, seems to me.

You seem to be making several assumptions at once here. First, that 
we are not actually using the logic with-= , but are axiomatizing 
SFOL+= inside SFOL (without =).  If we use an actual logic with =, 
then I don't see any problem.  Second, that this axiomatization is 
being made with respect to the wrong vocabulary. So, do it correctly. 
What is the issue here? Whichever way we define the SCL->SFOL 
embedding, attempting to axiomatize FOL-with-= inside FOL requires 
one to be sensitive to the vocabulary; either way, the vocabulary of 
the FOL resulting from the SCL->SFOL is quite well-defined. So apply 
the equality translation rules to the vocabulary you get, right?

On re-reading I think I may see your point. Suppose we claim that 
users of SFOL who wish to use SCL *must* go through an SFOL->SCL 
conversion and then use our SCL->SFOL mapping to enable their 
FOL-based tools to apply to SCL. I think this would be a serious 
mistake, but lets suppose we do. In that case, 'normal' SFOL syntax 
will be implicitly mapped into the holds/app syntax, and then the 
'normal' way of axiomatizing equality will miss the extra axiom 
instances needed for the holds/app vocabulary; so following the 
'normal' rules on the *original* SFOL syntax to figure out the needed 
equality schema instances will fail. Is that the issue? Because if 
so, I think that we can easily handle this by allowing people to just 
declare that they are using the FOL subset of SCL syntax and that FOL 
reasoners will apply.  And by adding that any use of the holds/app 
embedding would require that appropriate instances of the equality 
substitution schema be added to any target equality axiomatization 
(if that really needs to be said: of COURSE they do, right?)

>
>    Hence, if we want to use equality as it is
>    traditionally used in SFOL (ie no "holds" and
>    "app"), we have to drop the substitution axioms
>    for "holds" and "app". Then we have an SFOL
>    equality.
>
>    On the other hand, keeping the substitution
>    axioms for "holds" and "app" will give us a
>    stronger equality predicate (ie more consequences
>    can be derived).
>
>    Hence the beforementioned proposal suggest using
>    TWO DIFFERENT equality predicates in SCL: one (=)
>    would be a weaker equality (no substitution axioms
>    for "holds" and "app", hence no problems with
>    Horrock formulas), the other (scl=) would be a stronger
>    equality, where substitution axioms for "holds" and
>    "app" are axiomatised.
>
>    QUESTION: Would you agree with the mentioned proposal
>    or not?

Not.

>If not, please give your arguments and ideas
>    for alternative solutions.

1.  I think the idea of two different equalities is semantically incoherent.
2. Chris' most recent tweak to the MT has eliminated the Horrocks 
sentences as a problem
3. This problem, if I follow it, has to do with axiomatizing equality 
in FOL-without-equality, so is peripheral to our concerns for either 
case. (I don't mean to say we should completely ignore it, only that 
it is not central or fundamental. I think we can give a useful 'user 
guide' for how to best handle axiomatizations of equality in various 
subsets of SCL.)

>    If yes, please state so.
>    Please state any suggestions for modification or
>    issues which need stressing or working on.
>
>
>Regards,
>          Tanel Tammet
>

Sorry again for the long delay in responding.

BTW, will you be at the SW meeting in Florida in a couple of weeks?

Pat


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