[FOM] The quantifier "For infinitely many x"

[Torkel Franzen]

  In July last year, there were some exchanges on the list about the
quantifier "For infinitely many x". Thomas Forster had (on another
mailing list) raised the question of the axiomatizability of the logic
having only this quantifier, and he commented

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

In the posting

  http://www.cs.nyu.edu/pipermail/fom/2002-July/005743.html

I included a suggested completeness proof for a Hilbert-style axiomatization
of this logic with equality but without function symbols, adding
to the propositional logic part

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

(Completeness here means only that if A is valid, A is provable.) I
also included a suggested proof (from another FOM contributor) that
the set of satisfiable sentences in this logic is complete Pi-1-1,
which would mean that there could be no such completeness proof.

  I have since learned that Thomas was indeed right in assuming that
this topic must have been dealt with in the sixties. The paper by
Mitsuru Yasuhara, "Syntactical and semantical properties of
generalized quantifiers", JSL Volume 31 Number 4, Dec. 1966, deals
with just this logic, and more generally with the interpretation "for
at least k x".  The paper contains a model-theoretic proof (said to
have been produced under the guidance of Craig) that the sentences
valid under the reading of Qx as "for infinitely many x" coincide with
the sentences valid under the reading of Qx as "for at least k x", for
any infinite cardinal x. By Vaught's result (and later, Keisler's
explicit axiomatization) regarding "for uncountably many x", this
means that the sentences valid under the reading of Qx as "for
infinitely many x" are r.e. Yasuhara also gives an explicit sequent
calculus axiomatization of this logic, proving its completeness (in a
somewhat stronger form than that given above) without using the
model-theoretic result, leaving out = on the basis of a semantical
observation that = can always be eliminated from sentences in this
logic.

  As far as I can see, Yasuhara's paper settles the matter at issue.
His sequent calculus covers the =-free part of the above axiomatization,
so without having studied his proof in detail, I accept it on the basis
of the argument given in the cited posting. Also, the contrary argument
for the Pi-1-1 completeness of satisfiability in this logic is on
inspection seen to be incorrect, since Lemma 1 and Lemma 2 of that
argument are false.

  However, Yasuhara's paper excludes function symbols, so I don't know
if there is anything in the literature that settles the question of
the axiomatizability of the Inf-x logic with function symbols.

---

Torkel Franzen