FOM: Quantifier question

[Torkel Franzen]

  Thomas Forster says:

  >It seems such an obvious logic to consider.... surely someone
  >must have sorted this out in the 50s or 60s......

  So it would seem! However, you seem to have come upon an idea that
although apparently obvious hasn't occurred to anybody before, or at
least has not been documented. I think the people on this list will be
able to settle the matter of the properties of this logic. I include
below (i) a suggested proof that there can be no completeness theorem
for the logic in question (from a member of the list) and (ii) my
supposed completeness proof, which may well be altogether mistaken. At
this point, I don't feel competent myself to settle the matter either
way!


1) SUGGESTED PROOF THAT THERE CAN BE NO COMPLETENESS PROOF

The language L* has the usual connectives, relation symbols, and the
quantifier "there are infinitely many". Note that we don't have
constant or function symbols, and we don't have the usual quantifiers,
and we don't have equality.  It is convenient to explicitly add the
dual quantifier "for all but finitely many".

We write L for the usual predicate calculus with the usual connectives, 
relation symbols, and the usual quantifiers, but no equality.

Let phi be any formula in L. We write phi* for the formula in L*
obtained by replacing "there exists" by "there exists infinitely
many", and "for all" by "for all but finitely many". If T is a finite
set of formulas in L, we write T* for the set of all phi*, phi in
T. We write "forall x", "therexists x", "for infinitely many x", "for
all but finitely many x", by Ax, Ex, E*x, A*x, respectively.

LEMMA 1. Let T be a finite set of A...AE...E sentences in the language
of L and M be an infinite model of T*. Then some restriction of M to a
subset of dom(M) satisfies T.

Proof: Let T,M be as given, and let D = dom(M). Without loss of
generality, we can assume that T is a single sentence phi =
(Ax1)...(Axk)(Ey1)...(Eyr)(psi), where psi is quantifier free and k,r
>= 1.

We use the new constant symbols c0,c1,... . In this context, by a subsentence 
of phi* we mean any sentence that comes from phi* by chopping off one or more 
quantifiers and replacing the variables in the chopped off quantifiers by 
various constants ci. 

For all n >= 1, we define the n-systems. These are towers A1 containedin ... 
containedin An of finite sets of subsentences of phi*, together with cofinite 
subsets S1 containing S2 containing ... containing Sn, of D, together with 
functions f1 containedin f2 ... containedin fn, where

1. Each fi is a function from the set of constants in Ai into D.
2. Every sentence in every Ai holds in M under the assignment fi.
3. Every constant in every Ai lies in Si.  4. Let 1 <= i <= n. If
(A*xj)...(A*xk)(E*y1)...(E*yr)(psi) lies in Ai, then for all xj in Si,
(A*xj+1)...(A*xk)(E*y1)...(E*yr)(psi) holds in M.  5. Let 1 <= i <
n. If (A*xj)...(A*xk)(E*y1)...(E*yr)(psi) lies in Ai, and c is a
constant in Ai, then (A*xj+1)...(A*xk)(E*y1)...(E*yr)(psi)[xj/c] lies
in M.  6. Let 1 <= i < n. If (E*yj)...(E*yr)(psi) lies in Ai, then for
some constant c in Ai+1, (E*yj+1)...(E*yr)(psi)[xj/c] lies in Ai+1.

We now show that every n-system can be extended to an n+1-system. Let
the A1,...,An,S1,...,Sn,f1,...,fn be an n-system. We first meet
condition 5 by simply throwing the relevant subsentences into An+1,
and leave Sn,fn as yet unchanged. At this point we still satisfy
conditions 1,2,3,5. TO meet condition 6, we have to add new
constants. For the various (E*yj)...(E*yr)(psi) lying in An, introduce
different constants c that have not been used before, and throw
(E*yj+1)...(E*yr)(psi)[yj/c] into An+1. In order to meet conditions
1,2, we need to extend fn to fn+1 so that for each
(E*yj)...(E*yr)(psi) lying in An, (E*yj+1)...(E*yr)(psi) holds in M
with yj = fn+1(c). And in order to meet condition 3, it is vital that
fn+1(c) be chosen from Sn. But since (E*yj)...(E* yr)(psi) holds in M,
there are infinitely many choices for fn+1(c). Since Sn is cofinite,
one of the possible choices lies in Sn. Pick any such choice lying in
Sn. We have now extended An,fn to An+1,fn+1, and have left Sn
unchanged. We have met all conditions except condition 4. We look at
all sentences in An+1 of the form (A*xj)...(A*xk)(E*y1)...(E*yr)(psi),
and consider the set {xj: (A*xj+ 1)...(A*xk)(E*y1)...(E*yr)(psi) holds
in M}. Since these (A*xj)...(A*xk)(E* y1)...(E*yr)(psi) hold in M,
each of these sets are cofinite, and so we set Sn+ 1 to be Sn
intersected with all of these associated sets.

We have now constructed A1,...,S1,...,f1,..., satisfying conditions
1-6 with "< = n", "<n" removed. We claim that the restriction of M to
the elements assigned by the f's to the constants appearing in the A's
satisfies phi. To verify this, let d1,...,dk be among the relevant
constants. We can repeatedly apply condition 6 staring with j = 1, and
obtain constants e1,...,er such that psi(d1,...,dk,e1,...,er) holds in
M. QED

Let M be a model with domain D. The clone expansion of M is defined as
follows.  The new domain D' is D x omega. The k-ary relation R is
reinterpreted as R'((x1,n1),...,(xk,nk)) iff R(x1,...,xk).

LEMMA 2. Let T be any set of sentences in L. If M satisfies T then the
addition of countably infinitely many clones of every element of M
results in an infinite model of T*.

Proof: It is straightforward to prove that a formula of L* holds at a
D'- assignment in M' if and only if the corresponding formula of L
holds at the corresponding D-assignment in M. The idea is that in M',
if (x,n) witnesses, then any (x,m) also witnesses, and therefore there
are infinitely many witnesses. QED

THEOREM 3. Let T be a finite set of A...AE...E sentences. Then T has a
model if and only if T* has an infinite model.

Proof: Suppose T has a model. By Lemma 2, T* has an infinite
model. Suppose T* has an infinite model. By Lemma 1, T has a
model. QED

We remark that since equality is not in L, a set of sentences in L has
a model if and only if it has an infinite model.

We say that T is a set of sentences in L with <= if and only if T
contains the sentences <= is transitive, <= is connected, <= is
reflexive.

On the semantic side, if <= is transitive, connected, and reflexive,
then we obtain a linear ordering when we factor out by the equivalence
relation "x <= y and y <= x". This linear ordering is called the
factored <=. We also write x < y for x <= y and not y < x.

Let T be a set of sentences in L with <=. We define the expanded
theory T'. The language of T' is that of T together with the
distinguished unary relation P.  T' is T together with (forall
x)(therexists y)(x <= y and y <= x and P(y)).

Finally, we define the sentence alpha(P) in L* as 

(for all but finitely many x)(P(x) implies (there are finitely many
y)(P(y) and y <= x)).

LEMMA 4. Let T be a finite set of A...AE...E sentences in the language
of L with <=, and M be an infinite model of T'* + alpha(P). Then some
restriction of M to a some D' containedin dom(M) satisfies T', where
the factored <=|D' is of order type < omega + omega.

Proof: By Lemma 1, let M' be a restriction of M to D' containedin D =
dom(M), that satisfies T'. Since M satisfies alpha(P), let E be a
cofinite subset D, where for all x in E, there are finitely many y
such that P(y) and y <= x. Then with finitely many exceptions, for all
x in D', there are finitely many y in D' such that P(y) and y <=
x. Note that <=|D' is transitive, connected, and reflexive, and P
restricted to D' has at least one element from each of the equivalence
classes in <=|D'. So the x in D' such that there are finitely many y
in D' with P(y) and y <= x must be in finite position in the factored
<=|D'.  The finitely many exceptions must therefore occupy positions <
omega + omega in factored <=|D'. QED

LEMMA 5. Let T be as in Lemma 4. Suppose M has a model where factored
<= is of order type < omega + omega. Then the clone expansion of M has
an expansion by P which satisfies T'* + alpha(P).

Proof: By Lemma 2, the clone expansion of M satisfies T'*. The order
type of the factored clone expansion of <= is the same as the order
type of the factored <=. Choose P to pick out exactly one element from
the equivalence classes of <= in the clone expansion of M. QED

THEOREM 6. Let T be a finite set of A...AE...E sentences with <=. Then T has a 
model where <= of order type < omega + omega if and only if T'* + alpha(P) has 
an infinite model. 

Proof: By Lemmas 4 and 5. QED

Let L' be L together with equality. A set of sentences with <= in L' is a set 
of sentences in L' which contains the axioms of linear ordering.

LEMMA 7. There is an effective procedure which converts any finite set T of 
A...AE...E sentences with <= in L' to a finite set T^ of A...AE...E sentences 
with <= in L such that the former has a model with <= of order type omega if 
and only if the latter has a model with factored <= of order type <= omega + 
omega. 

Let L'' be L' together with constant and function symbols. 

LEMMA 8. There is an effective procedure which converts any finite set T of 
A...AE...E sentences with <= in L'' to a finite set T$ of A...AE...E sentences 
with <= in L' such that the former has a model with <= of order type omega if 
and only if the latter has a model with <= of order type omega. 

LEMMA 9. The set of A...AE...E sentences with <= in L'' that has a
model with < = of order type omega is complete Pi-1-1.

THEOREM 10. The set of satisfiable sentences in L* is complete Pi-1-1.



2) SUPPOSED COMPLETENESS PROOF


  The system has as its only quantifier Inf-x, meaning "there are
infinitely many x such that". We have as rules some suitable formulation
of the usual rules for propositional logic and identity, and the
specific rules for Inf



a)          Inf-x A => A  if x is not free in A
b)          Inf-x A(x) => Inf-y A(y)
c)         ~Inf-x(x=s)
d)          Inf-x(A v B) => Inf-x A v Inf-x B
e)          Inf-x A(x) => Inf-x Inf-y (A(x)&A(y)&~x=y)
f)          Having proved A=>B, conclude Inf-x A=>Inf-x B



I write G |- A to mean that the formula A is derivable from the set
G of formulas.


  We need:

  1) If G(c)|- A(c) where c is a constant, G(x) |- A(x)

(The constant elimination property.)

  2) For every m, every G, every A and B:

     If

(i)      G |- A(x1) and ... and A(xm) and all the xi are different =>
                       B(x1) or .. or B(xm)

     and

(ii)     G |- Inf-x A(x)

     then

(iii)    G |- Inf-x B(x).


   3) For every n every A1,..,An and every B:

      If

(i)      G |- A1(x1) and ... and An(xn) => B(x1) or ... or B(xn)

      then

(ii)     G |- Inf-x A1(x) and ... and Inf-x An(x) => Inf-x B(x)



  Claim: 1)-3) follow from the rules given. Note that even if there
is some oversight in my verification of this, this is not an essential
difficulty, since 1)-3) are clearly semantically sound, and so we would
just add whatever is needed to get 1)-3).


  The dubious part is rather the completeness proof itself, which goes
as follows. We use the Henkin-Mates approach, so let G0 contain
a sentence {A}, assumed consistent. I also assume that A contains no
function symbols, though it may contain individual constants.

  We have an infinite supply of special constants, individual constants
that do not occur in A.

  We have an enumeration A0,A1,A2,... of all formulas in the language
obtained by adding all the special constants.

  We define Gn+1 by recursion as usual.

  If An is not of the form Inf-x B(x) or not-Inf-x B(x):

  Gn+1 = Gn + An if An is consistent with Gn, otherwise Gn+1 = Gn + not-An.

  If An is of the form Inf-x B(x) or not-Inf-x B(x):


  case 1: Inf-x B(x) is consistent with Gn. In this case we add
Inf-x B(x), and we also add an infinite number of sentences
B(c1),B(c2),.. where the ci are individual constants that have not
been previously used for this purpose, and do not occur in any
of the formulas A0,..,An, and we also add ci#cj for
different i,j, forcing these constants to be interpreted as
different individuals. We leave infinitely many special constants
still unused.

  case 2: Inf-x B(x) is inconsistent with Gn.

   Subcase 1: not-B(x) is inconsistent with Gn. (Example: G0 may
consistently contain not Inf-x (x=x).) In this case we only add
not-Inf-x B(x) to obtain Gn+1.

   Subcase 2: not-B(x) is consistent with Gn. In this case we add
not-Inf-x B(x), but also (since we want to force the interpretation
to be such that only finitely many x satisfy B(x)) we add
not-B(c) for *every* special constant c which does not occur in
any of the formulas A0,..,An.

  G is of course the union of the Gn.

  Now suppose we manage to prove G consistent. Then we define, as usual,
an interpretation whose individuals are the equivalence classes of
constants, with constants a and b equivalent if a=b belongs to G. This
yields a model, by the usual reasoning. In the crucial case, where
A is Inf-x B(x), we need to verify that A is in G if and only if
B(a) is in G for infinitely many constants a, and indeed for
infinitely many equivalence classes [a]. In one direction, this is
immediate: if Inf-x B(x) is in A, we've added all the B(c) and
inequalities between the c. In the other direction, if Inf-x B(x)
is not in G, we've added at some stage not-Inf-x B(x), and then
also added not-B(c) for all but finitely many constants, so there
can't be infinitely many c, let alone infinitely many equivalence
classes, such that B(c) is in G.

  So the whole trick is now to prove G consistent. Suppose Gn+1 is
inconsistent. We have two cases.

   case 1: We added Inf-x B(x), and we also added B(c1),B(c2),... and
inequalities between the newly added constants. Suppose a proof of
an inconsistency uses c1,..,cn. Now the difference
compared to the Henkin proof for standard logic is that the newly
added c1,c2,.., even though they have not been used before for this
purpose, is the they c1,c2,.. may well occur in formulas that have
been added before, namly in earlier case-2 situations. So there may
be formulas not-A1(c1),...,not-Am(c1),not-A1(c2),...,not-Am(c2),...
..not-A1(cn),..,not-Am(cn) among those earlier added. But these
are the only possible occurrences of the c1 in earlier formulas.
So there is a derivation of an inconsistency from

   not-A1(c1),...,not-Am(c1),not-A1(c2),...,not-Am(c2),...
   ..not-A1(cn),..,not-Am(cn), all the ci different,
   B(c1),B(c2),..,B(cn).

But then, by the constant elimination property, there is a derivation of

   B(x1) and ... and B(xn) and all the xi different =>
       C(x1) or ... or C(xn)

where C(x) is A1(x) or.. or Am(x). So by property 1 above,  and the
fact that Inf-x B(x) is derivable, it follows that Inf-x C(x) is
derivable, and therefore the disjunction of Inf-x Ai(x), contradicting
the consistency of earlier sets in the sequence and the provability
of not-Inf Ai(x) for every x.

  case 2: We added not-Inf B(x), and also added not-B(c) for every
special constant not occurring in any of A0,..,An. An inconsistency means
then that Gn proves the disjunction B(c1) or ... or B(cn) for some
special constants c1,..,cn.

First, if there are no previous Qx-additions to the set, no ci occurs
in Gn, so Gn proves B(x1) or ... or B(xn), so Gn proves B(x), and we
have in fact the subcase in which only not-Inf x B(x) is added. So
there must be some previous Inf-x-additions to the set. The reasoning
is now similar to that in case 1. We find that a subset of Gn must
prove

    A1(x1) and ... and An(xn) => B(x1) or .. or B(xn)

where Gn also proves Inf-x A1(x),..,Inf-x An(x), and the property
2 yields a contradiction.