[CL] Clarifications on CL & 2 possible problems (dialect expressiveness; definition of S-variants)

[Frank Loebe]

Hi,

we have an interest in using CL instead of some specific FOL notation
(only), but we would like to have a rather clear understanding of some of
the less common aspects of the foundations of CL. Having invested some time
on the (draft) standard documents and the lists archives, we have a couple
of open questions and some need for confirmation of our current
understanding.

1.) Proof Theory
We have read that the specification of a proof theory for CL will not be
part of the standard. But does a proof theory exist already, or even
corresponding inference engines? If so, for which dialects apart from
"standard" FOL? Given these general questions, the following, more specific
ones would be most interesting.

2.) Axiomatization & Completeness
We have checked some of the "standard" tautologies of FOL against the CL
semantics. Those we checked seem to be maintained, as indicated in [1]
(sometimes adjusting them, e.g. replacement of a name x by a term t in (all
x (phi(x)) -> phi(x/t) needs to restricted to discourse names in segregated
dialects). Is there an axiomatization of CL (i.e., of the set of its
tautologies; referring to the full language, and to the sublanguage which
only omits sequence variables?). If so, is a corresponding proof of
completeness available?

3.) Segregated vs. Non-segregated Dialects
Is it correct, that segregated dialects can be more powerful than
non-segregated ones, in the sense that sentences may be satisfiable in
segregated dialects, but unsatisfiable in non-segregated ones? (an example
is given  below, in item 4.; to us, this was counter-intuitive at first
glance, because non-segregated dialects allow for more syntactic freedom)

If so, how should "exact semantic conformance" be understood, i.e., how can
non-segregated dialects be exactly conformant if there are such sentences?
Especially, this conflicts with the last sentence of section A.4.2 of the
standard draft [2], claiming exact semantic conformance of CLIF if numerals
and quoted strings are neglected. Moreover, the last sentence of section 7.1
in [2] requires to let every dialect "decide" as to whether it interpretes
names in UD or UR. But how does that make sense, if translations may be
necessary to establish an in-principle equal expressiveness among segregated
and non-segregated dialects?

4.) Underlying set theory and Russell(-like) sentences
The general question in this regard is whether a particular set theory is
assumed for CL semantic structures (and if so, which one). Our current state
of reading suggests that no assumptions about the set theory are made.
However, if one were interested in an axiomatization of CL, we do not see
how to develop one without specifying that set of sets containing those sets
which may serve as a universe of reference for a CL semantic structure.

Before moving to the origin of this question, we'd like to state that we are
aware that repeated questions for Russells paradox, which we had to look at,
as well. As far as we can see, the sentence
   (exists M (all X (M(X) iff (not X(X)))))
just yields a contradiction (is that correct?). However, this brought us to
the sentence which omits the existential quantifier, i.e.,
             (all X (M(X) iff (not X(X))))
It seems that this is satisfiable in a segregated dialect, but _as such_
(i.e., without any transformations) it is contradictory in a non-segregated
dialect.

5.) This leads us to another question, concerning the provision of a common
semantics. Before, we acknowledge that CL offers more syntactic freedom than
standard FOL. However, the necessity of translations using holds and app
constructions among segregated and non-segregated dialects, in order to
achieve equal expressiveness, seems to prevent a full "semantic integration"
among the CL dialects. This truely not being meant as an offensive question
but as one of understanding, but how could one argue that CL provides a
common semantic approach? Put differently, in order to see the differences
between, say, FOL and description logic which forms a fragment, why would it
 be advantageous to consider/express both as CL dialects, rather than
mapping their usual semantics directly?

6.) A smaller, technical question: in the last draft [2], non-repeating
sequences have become required in quantified sentences, whereas before
arbitrary sequences were allowed. First, we thought that quantified sequence
markers could still lead to constructions like (all x x (phi(x)). However,
the definition of S-variants [2, p.13] seems to treat them like names, i.e.,
seq_J(@v) may be different from seq_I(@v), for a sequence marker @v in S. Is
that correct? If so, is there a requirement missing in the definition of
S-variants, namely that seq_J(@v) = seq_I(@v) for all @v not in S?
Otherwise, these may vary and could change the interpretation of unbound
sequence markers.

Thanks in advance for clarification.

Best regards,
Frank Loebe
------------------------------------------------
Research Group Ontologies in Medicine (Onto-Med)
University of Leipzig
http://www.onto-med.de
------------------------------------------------

[1] Menzel, C. & Hayes, P. 2003. SCL: A logic standard for semantic
integration.
    http://ceur-ws.org/Vol-82/SI_paper_12.pdf

[2] ISO/IEC JTC 1/SC 32. 2006. Common Logic Standard (draft nr. 32 N xxxx,
2006-06-01)
    http://cl.tamu.edu/docs/cl/24707-21-June-2006.pdf