FOM: Quantifier question

[Torkel Franzen]

  About two and half years ago, Thomas Forster posed a question concerning
the logic with "there are infinitely many x such that" as its only
quantifier. I suggested an axiomatization of this logic:

  1) All instances of ordinary propositional axioms and identity axioms,

  2) the further axioms (for every A and B)

           Inf-x A -> A  if x is not free in A
           Inf-x A(x) -> Inf-y A(y)
           ~Inf-x(x=s)
           Inf-x(A v B) -> Inf-x A v Inf-x B
           Inf-x A(x) -> Inf-x Inf-y (A(x)&A(y)&~x=y)

  3) as rules, Modus Ponens and the proof rule

           if A->B has been proved, conclude Inf-x A -> Inf-x B


  I've recently had occasion to take a closer look at this, and
reconstructed the completeness proof for the above that I more or
less vaguely had in mind. It seems to me to be correct, i.e. if
a sentence A in this logic is valid, it is provable using the
above rules, but only if we do not allow function symbols in the
language. If we do allow function symbols, we get such valid formulas
as

        Inf-x p(f(x)) & ~Inf-x p(x) -> Inf-x Inf-y (~x=y&f(x)=f(y))

which are not provable from the above axioms. We can prove this
formula if we add the schema

        Inf-x Inf-y (A(t(x))&A(t(y))&~t(x)=t(y)) -> Inf-x A(x)

(for any term t(x)), but I've failed completely to prove any completeness
theorem for this or any other extension of the axioms in the case where
we allow function symbols.

  Does anybody have any ideas about this, or about any treatment of it
in the literature? I haven't been able to find any such treatment.