[SCL] SCL basic consensus badly needed

[Tanel Tammet]

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.

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.

    I am suggesting using a uniform translation
    schema, ALWAYS inserting "holds" and "app".

    QUESTION: Would you agree to that or not?
    If not, please give your arguments and ideas
    for alternative solutions.
    If yes, please state so.


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'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 "=".

    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.

    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!

    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? If not, please give your arguments and ideas
    for alternative solutions.
    If yes, please state so.
    Please state any suggestions for modification or
    issues which need stressing or working on.


Regards,
          Tanel Tammet