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

[Frank Loebe]

Hi,

first of all, many thanks for the detailed answers.

Chris Menzel wrote:
> >
> > 1.) Proof Theory
[...]

Ok, thanks, we don't have more issues wrt this topic currently.

> > 2.) Axiomatization & Completeness
[...]
> > 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?).
> >
>
> As noted above -- though I don't think such an axiomatization has been
> published anywhere.  I think I have an axiomatization for CL in an
> unfinished paper; I can try to find it if you'd like.

Indeed, that would be very interesting and we'd be grateful if you could
send us this paper.

> > If so, is a corresponding proof of completeness available?
>
> It seems to me that completeness (for CL without seq vars, again) is
> proved most easily by showing that valid proofs in CL are mapped (via
> the mapping of 6.6.1) one-to-one to valid proofs in the target language,
> and then showing that every CL sentence is mapped to a sentence with
> parallel logical properties, i.e., logical truths are mapped to logical
> truths and non-(logical truths) to non-(logical truths).  I confess I
> have not worked this out in detail, but it does seem to me to be a
> straightforward task.

I'm not sure, but I think we might refer to two slightly different notions
of completeness here. It seems that you refer to the completeness of a proof
theory wrt the semantics. Instead of this, until a "genuine" proof theory
exists, we'd be interested in a (comprehensible) characterization of the set
of tautologies of CL, i.e., a set of CL sentences (or sentence schemes),
which might later serve as axiomatic system in a proof theory for CL, or
possibly larger than necessary for this purpose. Similarly, this would be
interesting for those subclasses of structures given by segregated and
non-segregated dialects. In this case, "axiomatization" refers to a set Ax
of CL sentences whose models form the class of non- or partially segregated
CL structures, respectively. "Completeness" would in this case mean to show
the exact match between the model class of Ax and that one which it shall
characterize.

Thus far, we have found sentences which distinguish CL from FOL and HOL, in
the following sense: we pick some sentence phi and view it as a CL sentence
on the one hand, and try so as a FOL/HOL sentence on the other (so no
holds-app translation (as in sect. 6.6.1 of the draft standard) is/should be
used). Then there are (at least)
(1) CL tautologies, which are not expressable in FOL or HOL
(2) HOL tautologies / contradictions which are satisfiable in CL (but are
not CL-tautologies)
(3) "tautologies" for non-segregated dialects which are not tautologous for
full CL or FOL (as you noted)

Moreover, most FOL tautologies (at least those we checked) seem to be valid
in full CL. (1) above indicates that CL has more tautologies than FOL, the
question is, which more are needed to form an axiomatization (in the above
sense(s)).

(I'll discuss holds-app-translations below)


> > 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.;
>
> Well, usually logics are considered more powerful insofar as *fewer*
> sentences are satisfiable (since they are able to rule out
> interpretations that are allowed in weaker frameworks), but yes, there

Ok, thanks - that wasn't clear to me.

> are sentences there are satisfiable in segregated dialects that are not
> satisfiable in non-segrated dialects.  I'll talk about your example
> below, but the following (noticed some years ago relative to a similar
> framework by Michael Kifer and brought to light for CL by Ian Horrocks)
> is a good illustration of this:
>
>   (forall (x) (and (iff (P x) (not (Q x))) (forall (x y) (= x y)))

[I kept this part above for reference, see further below]

> > 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).
>
> The model theory for CL can be carried out in any standard set theory,
> notably, ZFC or NBG.  It could also be carried out in a non-well-founded
> set theory, though no use is made of non-well-founded sets.  The model
> [...]

This is how we understood it (finally ;-)

> > 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.
> >
>
> I'm not quite sure I'm understanding what you are getting at here, but
> it is important to note that CL itself involves no more commitment to
> sets than does ordinary first-order logic.  The domain of a model of a
> CL dialect is simply a nonempty set.  Like ordinary first-order logic,
> of course, the model theory for CL is expressed in mathematical English
> that assumes some basic set theory.  But that set theory is not itself
> something that must be axiomatized in any CL dialect.

Ok, I agree that it must not be axiomatized *in* CL dialects in order to use
them (and probably, many introductions to FOL do not deal with axiomatic set
theory). However, if one were interested in an axiomatization of full CL (in
the above sense), it should be necessary to know which structures are *all*
structures which may serve as CL model. What I'd expect is that one will
obtain different tautologies if, e.g., hypersets are allowed as universes of
reference. We have not looked at differences in detail yet, and, in
particular, it's not clear to us how much difference ZFC vs. NBG would make.
However, there should be some basic assumptions, such as the existence of
unions and intersections of sets (again, for the class of all possible model
structures, not necessarily within a single model). Based on your answer, it
seems that such assumptions have not yet been made explicit anywhere, right?

> Thanks very much for this example -- it is interestingly different from
> the Kifer/Horrocks example above.

Thanks :-)

> > 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.
>
> I'm not sure I see why.  It is true that the "holds/app" translation
> scheme in 6.6.1 is only given for non-segretated languages, but it is
> easily generalized to partially segregated languages as well.  Can you
> spell out your objection here in more detail?
[...]
> Hm, well, the semantics we provide applies to all CL dialects, and the
> dialects pretty well seem to cover the entire spectrum of first-order
> languages, from most to least restrictive.  Again, can you provide any
> more reasons for saying that it does not provide a common
> semantic approach?

Ok, let me try to explain (what might be more a feeling than a clear
objection, even for me). By definition, all CL dialects have a common
semantics. However, if I write a sentence similar to the Horrocks sentence
from above

(if (and (P a) (not (Q a))) (not (forall (x y) (= x y))))

One cannot tell whether this sentence (in its abstract syntax form; not as a
CLIF sentence) is a tautology or merely satisfiable, unless one fixes a
specific CL dialect (or at least, whether it is a non-segregated or
segregated one). This is the first "problem" (equal syntax, different
semantics according to different dialects). Hence, one needs translations
between dialects.

Similarly, if I translate a sentence from a non-segregated dialect to a
segregated one, section 6.6.1 advocates the holds-app-translation and claims
that *no* other axioms about holds and app are required. It is not clear to
us, why no further axioms are required. We have not had a deep look into
that yet, but two observations cause our reserve wrt this (so far).

Firstly, looking at models in the holds-app-language, there are no
constraints on the interpretation of holds and app, apart from the
translated sentences. E.g., assume the translation of P(x) from a segregated
dialect to holds(P,x). Nothing prevents holds from being interpreted with a
symmetric relation in the holds-app-language, obtaining holds(x,P) in one
specific model (though not in every model, that's clear). In general, it is
still open for us whether this unconstraintness could cause problems, e.g.,
why is it guaranteed that *all* and *only* entailments in the source
language (SL) correspond to entailments in the target language (TL) (i.e., T
\models(SL) phi iff tr(T) \models(TL) tr(phi))?

Secondly, could the status of sentences wrt being tautologies change due to
the translation? Maybe, this is not true for (full-)CL tautologies, but it
may be true for "tautologies" in non-segregated dialects. What we considered
so far is e.g. the above sentence (call it phi) and its translation. That
translation would not be tautology, since it is none in full CL. In order to
"create" a tautology (which it is for every non-segregated dialect), one
could add axioms to the holds predicate, say psi, such that (and phi psi)
becomes tautologous in the holds-app-language. Otherwise, one would need a
different translation.
(Sorry in case we overlooked some simple solution to these "observations"
...)

Given this, let me go back to the FOL-DL case before restating the question
for advantages of CL wrt semantic integration.

> > 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?
> >
>
> Well, if you are already considering a DL as a fragment of FOL --
> presumably through its representation as a modal logic and thence as a
> fragment of FOL (??) -- then you presumably already *have* the DL

Well, here, I referred to a truth-preserving translation of DL expressions
(of those DLs where applicable) to FOL expressions (basically, mapping
concepts to unary predicates, and roles/properties to binary predicates). I
don't know whether this involves an intermediate step through a modal logic,
but I thought the connection could be shown directly. (Sorry for having no
reference readily available.)

> expressed as a CL dialect.  I fear though that I'm not fully
> appreciating your question.  Hopefully Pat will have a go.

Frankly speaking, the question is the following. Let L1 and L2 be two logics
with different syntax and semantic structures. What one can always try to do
is to establish a connection manually (if possible, show equal
expressiveness (or an embedding) and find translations of syntax and
semantics such that the order of translating and reasoning becomes
irrelevant). Where is the difference for such an integration, if L1 and L2
are CL dialects? At present, it seems to us that the manual connection task
is transformed into finding the right holds-app-translation between
dialects, or providing a corresponding axiomatization of holds and app for a
general translation. Unfortunately, we have no presentable support for this
impression.

> [open: sequence variables in S-variant definition]
>
> Cheers!
>
> Chris Menzel

Best regards,
Frank Loebe