The recursion-theoretic study of mathematical structures other than ω is now a field of much activity. Analysis and algebra are two such structures which have been studied for their effective contents. Studies in analysis began with the work of Specker on nonconstructive proofs in analysis [16] and in Lacombe's inspiring notes on relevant notions of recursive analysis [8]. Studies in algebra originated in the work of Frolich and Shepherdson on effective extensions of explicit fields [1] and in Rabin's study of computable fields [15]. Equipped with the richness of modern techniques in recursion theory, Metakides and Nerode [11]–[13] began investigating the effective content of vector spaces and fields; these studies have been extended by Kalantari, Remmel, Retzlaff, Shore and others.

Kalantari and Retzlaff [5] began a foundational inquiry into effectiveness in topological spaces. They consider a topological space X with a countable basis ⊿ for the topology. The space is fully effective, that is, the basis elements are coded into ω and the operation of intersection of basis elements and the relation of inclusion among them are both computable. Similar to , the lattice of recursively enumerable (r.e.) subsets of ω, the collection of r.e. open subsets of X forms a lattice ℒ(X) under the usual operations of union and intersection.

In 1959 M. Dummett [3] introduced the logic LC obtained by adding the axiom ACpqCqp to the formalization of the intuitionistic prepositional calculus having modus ponens and substitution as its rules of inference. Later on R. A. Bull [1] showed, by quite a roundabout way, that the implicational theses of LC were precisely the theses of the implicational calculus obtained by adding the axiom CCCpqrCCCqprr to the system of positive implication. In 1964 Bull [2] gave another proof, this time using results of Birkhoff concerning subdirectly reducible algebras.

The aim of this short note is to emphasize that the use of Gentzen's natural deduction systems (see Prawitz [4]) allows us to give a much more direct proof.

In this note we investigate an extension of Peano arithmetic which arises from adjoining generalized quantifiers to first-order logic. Markwald [2] first studied the definability properties of L1, the language of first-order arithmetic, L, with the additional quantifer Ux which denotes “there are infinitely many x such that…. Note that Ux is the same thing as the Keisler quantifier Qx in the ℵ0 interpretation.

We consider L2, which is L together with the ℵ0 interpretation of the Magidor-Malitz quantifier Q2xy which denotes “there is an infinite set X such that for distinct x, y ∈ X …”. In [1] Magidor and Malitz presented an axiom system for languages which arise from adding Q2 to a first-order language. They proved that the axioms are valid in every regular interpretation, and, assuming ◊ω1, that the axioms are complete in the ℵ1 interpretation.

If we let denote Peano arithmetic in L2 with induction for L2 formulas and the Magidor-Malitz axioms as logical axioms, we show that in we can give a truth definition for first-order Peano arithmetic, . Consequently we can prove in that is Πn sound for every n, thus in we can prove the Paris-Harrington combinatorial principle and the higher-order analogues due to Schlipf.

Let ‘ϕ’, ‘χ’, and ‘ψ’ be variables ranging over functions from the sentence letters P0, P1, … Pn, … of (propositional) modal logic to sentences of P(eano) Arithmetic), and for each sentence A of modal logic, inductively define Aϕ by

[and similarly for other nonmodal propositional connectives]; and

where Bew(x) is the standard provability predicate for PA and ⌈F⌉ is the PA numeral for the Gödel number of the formula F of PA. Then for any ϕ, (−□⊥)ϕ = −Bew(⌈⊥⌉), which is the consistency assertion for PA; a sentence S is undecidable in PA iff both and , where ϕ(p0) = S. If ψ(p0) is the undecidable sentence constructed by Gödel, then ⊬PA (−□⊥→ −□p0 & − □ − p0)ψ and ⊢PA(P0 ↔ −□⊥)ψ. However, if ψ(p0) is the undecidable sentence constructed by Rosser, then the situation is the other way around: ⊬PA(P0 ↔ −□⊥)ψ and ⊢PA (−□⊥→ −□−p0 & −□−p0)ψ. We call a sentence S of PA extremely undecidable if for all modal sentences A containing no sentence letter other than p0, if for some ψ, ⊬PAAψ, then ⊬PAAϕ, where ϕ(p0) = S. (So, roughly speaking, a sentence is extremely undecidable if it can be proved to have only those modal-logically characterizable properties that every sentence can be proved to have.) Thus extremely undecidable sentences are undecidable, but neither the Godel nor the Rosser sentence is extremely undecidable. It will follow at once from the main theorem of this paper that there are infinitely many inequivalent extremely undecidable sentences.