We prove the statement in the title.

The main purpose of this paper is to show how partial recursive functions and isols can be used to generalize the following three well-known theorems of combinatorial theory.

(I) For every finite projective plane Π there is a unique number n such that Π has exactly n 2 + n + 1 points and exactly n 2 + n + 1 lines.

(II) Every finite projective plane of order n can be coordinatized by a finite planar ternary ring of order n. Conversely, every finite planar ternary ring of order n coordinatizes a finite projective plane of order n.

(III) There exists a finite projective plane of order n if and only if there exist n − 1 mutually orthogonal Latin squares of order n.

We show that two abelian-by-finite groups are elementarily equivalent if and only if they satisfy the same sentences with two alternations of quantifiers. We also prove that abelian-by-finite groups satisfy a quantifier elimination property. On the other hand, for each integer n, we give some examples of nilpotent groups which satisfy the same sentences with n alternations of quantifiers and do not satisfy the same sentences with n + 1 alternations of quantifiers.

The recursion theorem in abstract partially ordered algebras, such as operative spaces and others, is the most fundamental result of algebraic recursion theory. The primary aim of the present paper is to prove this theorem for iterative operative spaces in full generality. As an intermediate result, a new and rather large class of models of the combinatory logic is obtained.

We develop the theory of partial satisfaction relations for structures that may be proper classes and define a satisfaction predicate (⊨*) appropriate to such structures. We indicate the utility of this theory as a framework for the development of the metatheory of first-order predicate logic and set theory, and we use it to prove that for any recursively enumerable extension Θ of ZF there is a finitely axiomatizable extension *Θ′ of GB that is a conservative extension of Θ. We also prove a conservative extension result that justifies the use of ⊨* to characterize ground models for forcing constructions.

We establish a surprising connection between Menger's classical covering property and Blass-Laflamme's modern combinatorial notion of groupwise density. This connection implies a short proof of the groupwise density bound on the additivity number for Menger's property.

We improve on and generalize a 1960 result of Maltsev. For a field F, we denote by $H(F)$ the Heisenberg group with entries in F. Maltsev showed that there is a copy of F defined in $H(F)$ , using existential formulas with an arbitrary non-commuting pair of elements as parameters. We show that F is interpreted in $H(F)$ using computable $\Sigma _1$ formulas with no parameters. We give two proofs. The first is an existence proof, relying on a result of Harrison-Trainor, Melnikov, R. Miller, and Montalbán. This proof allows the possibility that the elements of F are represented by tuples in $H(F)$ of no fixed arity. The second proof is direct, giving explicit finitary existential formulas that define the interpretation, with elements of F represented by triples in $H(F)$ . Looking at what was used to arrive at this parameter-free interpretation of F in $H(F)$ , we give general conditions sufficient to eliminate parameters from interpretations.

Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Earlier work showed all of these implications to be strict. Here we reprove one of the strictness results, using very different arguments. The technique used is a mixture of realizability, forcing in the guise of Heyting-valued models, and Kripke models.

We work under the assumption of the Axiom of Determinacy and associate a measure to each cardinal κ < ℵ ε0 in a recursive definition of a canonical measure assignment. We give algorithmic applications of the existence of such a canonical measure assignment (computation of cofinalities, computation of the Kleinberg sequences associated to the normal ultrafilters on all projective ordinals).

In [1], page 85, Quine states: “… ponentials of logically true statements are logically true.” It is perhaps of some interest that this assertion is not completely precise as can be seen from counterexamples. One simple example is the following:

Let L be some language in which ‘c’ and ‘b’ are atomic sentential constants. Let ‘c’ be false and ‘b’ true. Suppose that L includes parentheses and the material conditional ‘⊃’ as logical notation, but that ‘b’, at least, counts as extra-logical.

An effective method for testing arguments consisting of singly quantified expressions has recourse to Parry's trapezoid symbolism.1 The procedure entails representing in that symbolism each premise of the argument and the negation of the conclusion. Variables are disregarded. After clearing away any negated quantifiers, the universal statements, including a denied existential conclusion, are first set down and their conjunction (KU) derived. Existential statements, including a denied universal conclusion, are then listed. The argument is valid if and only if some contradiction appears, whether as some premise empty of lines, as a KU empty of lines, or as some existential statement having no lines in common with the KU.