[FOM] RE: cofinite quantifier

[Dave Marker]

Thomas Forster asks:
>How undecidable is the theory of natural numbers with the cofinite quantifier?

Here's one answer.
Suppose we start with the language {+,*,<} and look at the fragment  F
generated from the atomic formulas by closing under propositional
connectives and the quantifer Q where
Qx\phi asserts that there is an n such that \phi holds for all x>n.
The F-theory of the integers is decidable. Ted Slaman gave a
direct proof of this. I noticed that the integers is an
F-elementary substrucute of the reals so decidability follows from Tarski.
(More generally, any two commutative ordered rings have the same
F-theory). This really says that this fragment has little expresive
power.

If we add a symbol for x^y to the language, then the natural numbers
is still an elementary substructure of the reals. If Shanuel's conjecture
is true then decidability would follow from the Macintyre-Wilkie theorem
on decidability of real exponentiation.

Dave Marker