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

[Christopher Menzel]

Frank Loebe wrote:
> 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?
>   

Since there is a simple effective mapping of non-segregated CL dialects 
*without sequence variables* into a traditional first-order language 
(see Section 6.6.1), one can of course carry out the mapping and then 
use any first-order inference engine on the resulting sentences.  (That 
mapping is easily generalized to "partially" segregated languages.)  It 
is possible, however, to formulate a proof theory for CL dialects 
directly; the result looks very similar to standard proof theories, 
modified in pretty straightforward ways to accommodate the type freedom, 
variable polyadicity, the ability to bind multiple variables, etc.  
E.g., the CLIF schema for universal instantiation for an axiomatic proof 
theory would be

(if (forall (N_1 ... N_n) WFF) WFF'), where WFF' is the result of 
replacing all free occurrences of each N_i in WFF with occurrences of a 
name M_i that is free for N_i in WFF.

This will cover sentences where some of the N_i occur in predicate 
position in WFF as much as those where they are all in subject position.

Proof theory for CL with sequence variables is more tricky, and to my 
knowledge no one has worked it out in detail.  It will of course not be 
decidable, as CL with seq vars is expressively equivalent to a 
sublanguage of the infinitary language L_omega1_omega that allows 
infinite conjunctions and disjunctions.  There are some obviously valid 
principles, though, e.g.,

(if (forall (seq) WFF) WFF'), where WFF' is the result of replacing all 
free occurrences of seq in WFF with a sequence of names N_1 ... N_m, all 
of which are free for seq in WFF.

And in the other direction there is the infinitary rule:

(forall (N) WFF_1)
(forall (N_1 N_2) WFF_2)
(forall (N_1 N_2 N_3) WFF_3)
...
-----------------------------------
(forall (seq) WFF)

where each WFF_i is the result of replacing seq in WFF is the sequence 
N_1 ... N_i of names, all of which are free for seq in WFF.

I don't know if this would yield a complete proof theory (similar to 
Peano Arithmetic with an omega rule) but again, of course, it could not 
be decidable because of the infinitary character of the introduction 
rule for quantified sequence variables.  CL with seq vars is also easily 
shown not to be compact (though it is possible that a form of so-called 
"Barwise" compactness for L_omega1_omega holds for it -- another open 
question requiring someone with more time and perhaps more brainpower 
than I've got! :-).

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

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.

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

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

This is of course satisfied in a traditional, segregated dialect in a 
model containing just one object that is in P's extension but not Q's.  
In a non-segregated dialect D, however, both P and Q are names with 
denotations.  The first conjunct of the sentence prevents them from 
referring to the same object in the domain, hence the second conjunct, 
which is true only in models with one element, can't possibly be 
satisfied in a model of D if the first conjunct is and vice versa.

> to us, this was counter-intuitive at first
> glance, because non-segregated dialects allow for more syntactic freedom)
>   

Ah, but with great freedom comes great responsibility!  (I don't know 
what that means, but it sounds good! :-)  Non-segregated CL dialects do 
indeed give you greater syntactic freedom, but part of that freedom is 
gained by having a semantics on which predicates denote, and a 
consequence of that semantics is sentences like the above.  However, I 
don't see this as any sort limitation; if it turns out to be important 
to use exactly the form above to capture something about a given domain, 
then one should use a segregated dialect.  Alternatively, in a 
non-segregated dialect, one can introduce explicit, disjoint predicates 
REL and IND for relations and individuals and express the proposition 
above as, e.g.:

  (forall (x) (and (iff (P x) (not (Q x)))
                   (forall (x y) (if (and (IND x) (IND y)) (= x y))))) .

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

Pat is the conformance expert; I'll let him take those questions.

> 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 
theory might appear to require non-well-founded sets at first sight, 
since a relation can be in its own extension.  However, well-foundedness 
is a problem only if relations were identified with their extensions.  
But in CL, they aren't.  There are just objects, some of which, 
intuitively, are relations, but an inviolable distinction between 
relations and individuals is not part of the semantics of CL.  In CL's 
model theory, everything is an object and every object has a (possibly 
empty) relational extension.

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

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

Yes!

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

Well, not in a segregated dialect in which "X" has been designated a 
non-discourse name.  Such names are not allowed to occur as arguments in 
atomic sentences.  But assuming you are talking about a partially 
segregated dialect in which "X" is a discourse name and "M" is not, yes, 
the sentence above is easily satisfied (consider a model with one 
element that is in the extension of (the denotation of) "M" but which is 
not in its own extension), and, proof theoretically speaking, it is 
clear that no contradiction can be derived because "M", being 
non-discourse, cannot be substituted for "X" in an instance of universal 
instantiation.

> but _as such_
> (i.e., without any transformations) it is contradictory in a non-segregated
> dialect.
>   

Yes, one could derive essentially the same contradiction as in the 
existentially quantified case.  So you wouldn't want it as an axiom!

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

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

> This truely not being meant as an offensive question
>   

Please, we welcome all challenges and objections!  (What doesn't kill us 
makes us stronger! :-)
> but as one of understanding, but how could one argue that CL provides a
> common semantic approach?

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?

> 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 
expressed as a CL dialect.  I fear though that I'm not fully 
appreciating your question.  Hopefully Pat will have a go.

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

It could well be something has been overlooked there.  I'll give this a 
closer read later this evening.

Cheers!

Chris Menzel