² For definiteness, let us agree that symbols for negation, implication, and universal quantification are primitive, the others being introduced by definition.

³ These are of course not the only desirable conditions, but their adequacy (in a certain sense) will appear in section 2. The desirability of these conditions may be seen, from one point of view, by observing that the semantical relation of entailment, , satisfies (ii)–(viii). (Γ H- A if and only if every model which satisfies all wffs of Γ also satisfies A.) Conditions (ii)–(iv), (vi)–(viii) resemble those given by Tarski (Über einige fundamentale Begriffe der Metamathetnatik, Comptes rendus des séances de la Société des Sciences et des Lettres de Varsovie, Classe III, vol. 23 (1930), pp. 22–29Google Scholar) for systems which have no generalization rule.

⁴ This is known in the literature as the Deduction Theorem, and was enunciated by Herbrand, (Recherches sur la théorie de la démonstration, Warsaw (1930))Google Scholar and also in effect by Tarski, (Remarques sur les notions fondamentales de la méthodologie des mathématiques, Rocznik Polskiego Towarzystwa Matematycznego, vol. 7 (1929), pp. 270–272)Google Scholar.

⁵ See, for example, Church, Alonzo, Introduction to mathematical logic, Part I, Princeton (1942)Google Scholar.

⁶ Besides failing to satisfy (vi), Definition I violates condition (i), provided that infinite sets Γ are admitted. This can be shown as follows. Let Δ be a recursively enumerable set of variables which is not recursive. (It is well known from the fundamental work of Church and Kleene that such a set exists.) Since Δ is recursively enumerable, there is a recursive function Φ which maps the natural numbers onto Δ. Now let A₀, A₁, … be a recursive enumeration of the set of all wffs in which each wff occurs exactly once. Let B₀ be the first of these wffs which is not a generalization (i.e., not of the form (α)D) and which contains Φ(0) as its only free variable. Let B_n + 1 be the first wff in the list A₀, A₁; … coming after B_n which is not a generalization and which contains Φ(n + 1) as its only free variable. (There clearly must be such a formula.) Now let Γ be the set of all wffs B₀, B₁, …. Γ is decidable. For, given any wff A, we begin to form the sequence B₀, B₁, … until we arrive at a term B_n which comes after A in the enumeration A₀, A₁ …. If A occurs among B₀, …, B_n, then A is in Γ. On the other hand, if A does not occur among B₀, …, B_n, then A is not in Γ, since A cannot appear a second time in the sequence A₀, A₁….D(Γ, E) (in the sense of Definition I) is, however, not decidable if, for instance, E is any formal axiom. For if D(Γ, E) were decidable, then one could decide in particular, given any column of the form 〈E, (α)E, E〉, whether it is in D(Γ, E). Since no formal axiom or member of Γ has the form (α)E, it is seen that 〈E, (α)E, E〉 is in D(Γ, E) if and only if α is not free in any wff of Γ. Thus the set of variables free in some wff of Γ would be decidable, but this set is just Δ, which is undecidable.

⁷ The reader who compares Kleene's work with this paper should be cautioned that in the former the symbol ‘⊢’ is used to denote a relation between a sequence (rather than a set) of formulas and a formula. Furthermore, Kleene does not use ‘⊢’ to denote a relation equivalent to the semantical notion of entailment, since he uses ‘Γ⊢A’ to assert the existence of a primitive deduction of A from Γ (with no restriction on generalization). See pp. 87–88 of Kleene's book.

⁸ Of course we may use (ix) in this proof since we have already shown that (ix) is a direct consequence of (ii)–(viii).