FOM: Quantifier question

[Matthew Frank]

Model-Theoretic Logics, ed. Jon Barwise and Solomon Feferman, Springer,
1985, is the place to look, in the early chapters.  The logic of "there
are uncountably many x such that" is better behaved.  --Matt

On Fri, 12 Jul 2002, Torkel Franzen wrote:

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