

warwick.ac.uk/lib-publications 
 

Original citation: 
Dean, Walter. (2017) Bernays and the completeness theorem. Annals of the Japan 
Association for Philosophy of Science, 25. pp. 45-55. 
 
Permanent WRAP URL: 
http://wrap.warwick.ac.uk/84526  
 
Copyright and reuse: 
The Warwick Research Archive Portal (WRAP) makes this work by researchers of the 
University of Warwick available open access under the following conditions. Copyright © 
and all moral rights to the version of the paper presented here belong to the individual 
author(s) and/or other copyright owners. To the extent reasonable and practicable the 
material made available in WRAP has been checked for eligibility before being made 
available. 
 
Copies of full items can be used for personal research or study, educational, or not-for-profit 
purposes without prior permission or charge. Provided that the authors, title and full 
bibliographic details are credited, a hyperlink and/or URL is given for the original metadata 
page and the content is not changed in any way. 
 
Publisher’s statement: 
http://phsc.jp/en/annals.html  
 
A note on versions: 
The version presented here may differ from the published version or, version of record, if 
you wish to cite this item you are advised to consult the publisher’s version. Please see the 
‘permanent WRAP URL’ above for details on accessing the published version and note that 
access may require a subscription. 
 
For more information, please contact the WRAP Team at: wrap@warwick.ac.uk 
 

http://go.warwick.ac.uk/lib-publications
http://go.warwick.ac.uk/lib-publications
http://wrap.warwick.ac.uk/84526
http://phsc.jp/en/annals.html
mailto:wrap@warwick.ac.uk


Annals of the Japan Association for Philosophy of Science Vol.xx, No.x (201x) 1–10 1

Bernays and the Completeness Theorem

Walter Dean

1. Introduction

A well-known result in Reverse Mathematics is the equivalence of the formalized

version of the Gödel Completeness Theorem [8] – i.e. every countable, consistent set

of first-order sentences has a model – and Weak König’s Lemma [WKL] – i.e. every

infinite tree of 0-1 sequences contains an infinite path– over the base theory RCA0.
1

It is less well known how the Completeness Theorem came to be studied in the set-

ting of second-order arithmetic and computability theory. The first goal of this note

will be to recount these developments against the backdrop of the latter phases of

the Hilbert program, culminating in the publication of the second volume of Hilbert

and Bernays’s [13] Grundlagen der Mathematiks in 1939. This work contains a de-

tailed formalization of the Completeness Theorem in a system similar to first-order

Peano arithmetic [PA] – a result which has come to be known as the Arithmetized

Completeness Theorem. Its second goal will be to illustrate how reflection on this

result informed Bernays’s views about the philosophy of mathematics, in particular

in regard to his engagement with the maxim “consistency implies existence”.

2. Origins and arithmetization

Hilbert posed the problem of the completeness of the first-order predicate cal-

culus in his 1928 Bologna address [10] after having investigated (in conjunction with

Bernays) a variety of completeness notions in his 1917/1918 and 1921/1922 Göttingen

lectures [5].2 These lectures also serve as the basis for the axiomatization of first-

and second-order logic in Hilbert and Ackermann’s 1928 textbook Grundzüge der

theoretischen Logik [11]. This was in turn Gödel’s source in his 1929 dissertation [8].

An important technique employed in Hilbert’s lectures and in the Grundzüge is the

method of arithmetical interpretations. In the case of propositional logic, such an in-

terpretation is an assignment of the values 0 (true) and 1 (false) to the propositional

variables X, Y, Z, . . ., together with the interpretation of disjunction as multiplication

and negation as 1�X. A formula is taken to be valid if it evaluates to 0 under all such

interpretations. In his 1917/1918 lectures Hilbert used this definition to prove both

the soundness of the propositional calculus and also its so-called Post Completeness

1 This is one of several results originally announced by Friedman [6] whose proof later
appeared in Simpson’s monograph [19] IV.3.

2 See [21] discussion of this evolution.

— 1 —


2 Walter Dean Vol. xx

– i.e. if an underivable formula were to be added to the calculus as a scheme, the

system would be become inconsistent. In his 1918 Habilitationsschrift, Bernays would

go on to adapt Hilbert’s presentation to prove the completeness of the propositional

calculus in the now familiar form – i.e. “every valid formula is provable”.

In order to address the analogous questions about first-order logic, Hilbert and

Ackermann [11] described a method for transforming first-order formulas into proposi-

tional ones whereby each predicate symbol is associated with a collection of numerical

substitution instances derived by replacing universally quantified formulas with con-

junctions and existentially quantified with disjunctions. This yields a method for

constructing counter-models for formulas falsifiable in a finite domain which Gödel

showed could be extended to arbitrary formulas.

Suppose that F is an irrefutable sentence which we wish to show is satisfied in

a model M. Gödel described how to construct a family of propositional formulas

A0, A1, A2, . . . composed of numerical substitution instances of the primitive pred-

icates appearing in F in a manner similar to that originally described by Hilbert

which mimics the dependencies betweens the bound variables of F . He also showed

that if all of the Ai are irrefutable in the propositional calculus, then F is irrefutable

in the predicate calculus. The completeness theorem for the propositional calculus

can now be invoked to yield propositional valuations vi satisfying each of the Ai.

Relying on the manner in which these formula are constructed, it can be shown that

the vi assign compatible truth values to their propositional variables and that there

are finitely many ways of extending vi to vi+1. König’s Lemma can thus be employed

to obtain a valuation v! satisfying all of the Ai simultaneously.
3 This valuation may

in turn be used to construct a model M satisfying F by taking the extension of a

k-ary predicate P(~j) to be the set {~j 2 Nk : v!(P(~j)) = 0}.
On this basis Gödel observed that his proof yields a model with domain N. In

the second (1938) edition of [11], Hilbert and Ackermann went one step further in

stressing that the construction of the valuations vi also provides arithmetical defini-

tions of the predicates appearing in F . Prior to the treatment of the Completeness

Theorem in the second volume of the Grundlagen Hilbert and Bernays had also elab-

orated on the significance of arithmetical models in the first two chapters of the first

volume. They begin this discussion by distinguishing between what they refer to

as contentual and formal axiomatics. The former is typified by Euclidean geometry

and physical theories whose fundamental notions draw on experience and which may

thus be understood contentually. Formal axiomatic theories are typified by Hilbert’s

axiomatizations of geometry and abstract away from intuitive content. They begin

instead with the assumed existence of “a fixed system of things . . . which is delimited

3 Although Gödel does not mention König’s Lemma by name, its role in the proof of
completeness appears to have first been noted by Kreisel [14] (p. 268).

— 2 —


No. x Bernays and the Completeness Theorem 3

from the outset and constitutes a domain of subjects for all predicates of the propo-

sitions of the theory” and whose existence is “an idealizing assumption that properly

augments the assumptions formulated in the axioms” (p. 2). As such structures

“transcend the realm of experience” (p. 3), Hilbert and Bernays arrive at the conclu-

sion that the corresponding axiomatic theories can only be appropriately grounded

by providing a proof of their consistency.

This provides the context for their introduction of arithmetical models:4

We are therefore forced to investigate the consistency of theoretical systems without consid-

ering actuality, and thus we find ourselves already at the standpoint of formal axiomatics. ¶
Now, one usually treats this problem . . . with the method of arithmetization. The objects of a

theory are represented by numbers or systems of numbers and the basic relations by equations

or inequations, such that, on the basis of this translation, the axioms of the theory turn out

either as arithmetical identities or provable sentences . . . or as a system of conditions whose

joint satisfiability can be demonstrated via arithmetical existence sentences . . . [12], p. 3

Much of the second volume of the Grundlagen is devoted to the exposition of

techniques by which Hilbert and Bernays hoped to provide a finitist consistency proof

for theories such as the systems of second-order arithmetic in which they ultimately

proposed to formalize analysis (Supplement IV of [13]). But they also provide a

treatment of Gödel’s incompleteness theorems (§5.1), before ultimately considering

various ways in which proof theoretic results such as those of Ackermann and Gentzen

may call for a “trangression” of the original finiten Standpunkt (§5.3). Preceding this

is their presentation of the Completeness Theorem (§4.2). As a prelude to this, they

remark (§3.5c) that this result simplifies the decision problem for first-order logic

by showing that derivability may be identified with validity and irrefutability with

satisfiability. But they also observe that since this result is not guaranteed to provide

finite counter-models it must be initially understood as belonging to the set-theoretic

understanding of logic as opposed to the finist one.

In light of this, Hilbert and Bernays go on to introduce the notion of an e↵ec-

tively satisfiable [e↵ektiv Erfüllbar] formula ([13], pp. 189-190) – i.e. one which upon

being put into prenex normal form can be transformed by e↵ectively replacing atomic

formulas with truth values and formulas containing free variables with computable

[berechenbar] number theoretic predicates so that each substitution instance with

numerals is made true in an arithmetical model. For irrefutable formulas which have

no finite models (e.g. of the sort discussed in §1 of [12]) they suggest that such an

interpretation would constitute a “finitist sharpening” ([13], p. 191) of the Complete-

ness Theorem. But upon introducing the definition of e↵ective satisfiability, they go

on to conjecture that completeness would fail if this notion were to be substituted

4 See also [12] pp. 18-19 and pp. 37-42.

— 3 —


4 Walter Dean Vol. xx

for the traditional (non-e↵ective) definition of satisfiability in its statement.5

These considerations set the stage for Hilbert and Bernays’s formalization of the

Completeness Theorem. Unlike modern presentations, this treatment begins with a

careful exposition (§4.1) of Gödel’s method of the arithmetization of syntax. This

machinery is employed (§4.2a) to define a primitive recursive function q(x) such that

the truth of q(n) = 0 for each natural number n (where n is the numeral for n) implies

the irrefutability of a given first-order formula F in the predicate calculus.6

The proof of the Completeness Theorem given in §4.2b proceeds by showing how

these arithmetized definitions can be used to formalize the steps in Hilbert and Ack-

ermann’s rendition of Gödel’s proof as summarized above. This leads to a method

for transforming a formula F of an arbitrary first-order language into an arithmetical

formula F ⇤ by replacing its primitive predicate and function symbols by arithmetical

formulas of appropriate arities extracted from Gödel’s construction such that if q(n)

holds for all n (i.e. F is irrefutable) then F ⇤ is a true arithmetical sentence. This

proof yields one form of what is now called the Arithmetized Completeness Theorem:

if F is a sentence which is consistent relative to the axioms of the the predicate calcu-

lus (and thus q(n) = 0 holds for all n), then F has an arithmetically definable model –

i.e. one whose domain is a set of natural numbers definable by a formula of first-order

arithmetic and whose primitive relation and function symbols are interpreted by the

extension of such formulas in the standard model N = hN, 0, s, +, ⇥i.
Just prior to their presentation of Gödel’s Incompleteness Theorem, Hilbert and

Bernays describe the significance of this form of his Completeness Theorem as follows:

The transition from the formula F to the formula F ⇤ through number-theoretic substitution

has the significance of providing a number-theoretic model for the axiom system, since the

formulas of the axioms by the replacement of the symbols for the basic predicates through

number-theoretic expressions go over into provable number-theoretic expressions . . . There

thereby exists for a consistent axiom system of the kind considered a number-theoretic model

in the deductive sense. ¶ This result has its significance as a completeness theorem, that is
as a kind of deductive closure of the predicate calculus, only under the assumption of the

consistency of the number-theoretic formalism . . . ¶ This consideration indicates that the task
of a proof of the consistency of the full number-theoretic formalism endures as an unfinished

problem in our investigation. [13], p. 253

3. After the Grundlagen

As Hilbert acknowledged in his introduction to [12], both volumes of the Grund-

5 “It is rather to be assumed that in general it is not possible for a irrefutable prenex
formula to be satisfiable by computable logical functions.” [13], p. 191.

6 As Hilbert and Bernays only introduce the (now) standard formalization of consis-
tency as ¬Bew(p?q) in §5.2, the definition of q(x) given in §4.1 more closely resembles
the contemporary notion of Herbrand consistency (cf., e.g. [9], p. 179 ↵).

— 4 —


No. x Bernays and the Completeness Theorem 5

lagen were composed by Bernays. And in fact one of the earliest applications of

the Arithmetized Completeness Theorem grew out of Bernays’s contemporaneous

work on the system which is now known as Gödel-Bernays set theory [GB]. Bernays

originally presented this system as a two-sorted theory of sets (x, y, z, . . .) and classes

(X, Y, Z, . . .) with separate set and class membership relations.7 It is a consequence of

Bernays’s Class Theorem ([1], p. 72) that GB proves the existence of all predicatively

definable classes – i.e. those definable without the use of bound class variables. From

this it can be seen to follow that this system conservatively extends ZF. Nonetheless,

Bernays originally provided a finite axiomatization which can be conjoined to yield a

single sentence containing 2 as its sole non-logical symbol. This in turn suggests GB

as a natural theory to consider in regard to Hilbert and Bernays’s conjecture that

there exist irrefutable first-order formulas which are not e↵ectively satisfiable.

In the course of attempting to demonstrate this, Kreisel [14] isolated a fact which

is implicit in Hilbert and Bernays’s proof of the Arithmetized Completeness Theo-

rem – i.e. that if q(x) and F ⇤ are defined as above, then not only does the truth

of 8x(q(x) = 0) in the standard model entail that of F ⇤, but also the conditional

8x(q(x) = 0) ! F ⇤ is in fact provable in a first-order arithmetical system such as PA.

He then used this fact in conjunction with the availability of an additional interpre-

tation of PA into the language of GB to construct a sentence similar to that arising in

Russell’s paradox. But rather than leading to a contradiction, Kreisel showed that the

relevant sentence is undecidable in GB, modulo the assumption of its !-consistency.8

Kreisel thus showed how, upon formalization in a system like PA, the Arithme-

tized Completeness Theorem can be used to obtain a form of Gödel’s First Incom-

pleteness Theorem for a system S consisting of GB without the axiom of infinity.9 But

in addition to this, he also initiated the study of arithmetical models of set theory –

i.e. structures of the form A = hN, Ei satisfying the axioms of theories like S where
E ✓ N ⇥ N is an arithmetically definable set interpreting membership. In particular,
Kreisel explicitly stated that no such model can be such that E is a recursive rela-

tion.10 Since S admits a finite axiomatization, this confirmed Hilbert and Bernays’s

7 As Bernays observes in [1], his axiomatization is based on an earlier formulation of
von Neumann which was first presented in his 1929-1930 Göttingen lectures.

8 The independent statement is explicitly constructed on p. 274 of [14] and roughly
expresses that the arithmetical interpretation R⇤ of the Russell class does not bear
the relation 2⇤ – i.e. the arithmetical interpretation of 2 – to itself.

9 Kreisel’s axiomatization of S is given on p. 48 of [15].
10 As Wang observed in his review of [14], the proof Kreisel sketched doesn’t actually

yield this result but (in e↵ect) only the weaker statement that the definition of 2⇤

produced by applying the Arithmetized Completeness Theorem to GB can never be
�01. This anticipates the later work (summarized in the introductory remarks to [8])
which collectively showed that any consistent statement has an arithmetical model in
which all of its relations are �02-definable and also that this statement fails for ⌃

0
1 [⇧

0
1.

— 5 —


6 Walter Dean Vol. xx

conjecture.

These results would be of isolated interest were they not also related to the

early study of non-standard models of arithmetic and set theory. For as Rabin [17]

observed, if A |= S and M is a model of arithmetic obtained by interpreting arith-

metical notions in the conventional manner in A, then M cannot be isomorphic to the

standard model N . Thus although the Arithmetized Completeness Theorem can be

employed to yield an arithmetical definition of a model of an apparently stronger the-

ory of sets (modulo the assumption of its formal consistency statement), the models

so obtained are non-standard with respect to how they interpret arithmetical notions

themselves. In light of this, Wang [20] (p. 32) describes such models as ‘not very

“natural”’ and Rabin [17] (p. 408) described them as ‘highly pathological’.

4. Bernays’s reappraisal

Although Bernays was not directly involved with obtaining any of the foregoing

results, he made similar use of the Arithmetized Completeness Theorem in the last of

his series of papers on GB [3] (pp. 87-93). After first describing how the Ackermann

interpretation of Zermelo-Fraenkel set theory without the axiom of infinity can be

extended to provide an interpretation of S, he then observes that the methods of the

Grundlagen can also be employed to reduce the consistency of this system to that

of number theory. In particular, he states that arithmetizing the Henkin complete-

ness construction for S yields a “constructive” proof of the consistency of this system

relative to the consistency of the “number theoretic frame” ([2], p. 93).

In order to appreciate the significance which Bernays appears to have invested

in such a reduction, it is important to keep in mind that from the 1940s onwards, he

expressed increasing confidence that the proof theoretic work of Ackermann, Gentzen,

Schütte and others had provided constructive consistency proofs for arithmetic and

subsystems of analysis (e.g., [2], p. 87). This in turn appears to have informed his

appraisal of the foundational significance of the Completeness Theorem itself.

A useful waypoint here is provided by the controversy between Hilbert and Frege

concerning whether the consistency of various sets of geometric axioms entails the

existence of a model in which they are satisfied (the view conventionally attributed

to Hilbert) or whether consistency should be defined in terms of existence of a model

(the view conventionally attributed to Frege).11 Gödel acknowledged his awareness

of this controversy in the introduction to his dissertation as did Bernays in an unpub-

lished note from the mid-1920s.12 Therein he observes that while consistency proofs

11 This was, of course, the subject of the 1899 exchange of letters between Frege and
Hilbert (reprinted in [7]) which arose in light of Frege’s reaction to the publication of
the first edition of Hilbert’s Grundlagen der Geometrie.

12 The note in question is reprinted in [18], pp. 389-390. It dates from between 1925 and

— 6 —


No. x Bernays and the Completeness Theorem 7

have thus far proceeded by exhibiting models, the development of proof theory pro-

vides an alternative to Frege’s position in the form of a deductive understanding of

consistency.

This point is taken up in greater detail in Bernays’s 1930 paper “The philoso-

phy of mathematics and Hilbert’s proof theory” [4]. This paper begins by reviewing

the rationale for using formal logic and proof theory as tools for investigating the

foundational questions which had arisen in mathematics in light of the paradoxes.

But it is also notable in that it provides a summary of the status of Hilbert’s finitist

consistency program on the eve of the Incompleteness Theorems. After expressing

optimism that the systems of formal arithmetic which were currently under investi-

gation would be shown to be not only consistent but also deductively complete, he

concedes that “a considerable field of problems remains open” (p. 59) in this area.

But Bernays also asserts that the unavailability of such results does not pose

a problem for the use of proof theoretic methods to investigate formal axiomatics,

inclusive of systems which posit infinite totalities. For as he writes

[T]he formalism of statements and proofs, which represent our idea-formation does not coin-

cide with the formalism of that structure we intend in the concept-formation. The formalism

is su�cient to formulate our ideas about infinite manifolds and to draw from these the log-

ical consequences, but it is, in general, not capable of producing the manifold, as it were,

combinatorially from within. [4], p. 59

Bernays’s view at this point thus appears to have been that while the systems em-

ployed in formal axiomatics are su�cient for formalizing the practice of subjects like

analysis, they do not themselves provide models of their axioms and also presumably

that this would continue to be the case even if consistency proofs in the style then

under consideration (e.g. as based on the ✏-substitution method) became available.

Although Bernays does not mention the Completeness Theorem by name in his

1930 paper, its role comes to the surface in his 1950 essay “Mathematical existence

and consistency” [4]. He begins with the observation that the equation of existence

with consistency is salutary as it serves to dispel the impression that mathematics is

concerned with a form of “ideal” existence which is unlike that of theoretical entities

in the physical sciences. But he also remarks that there is still the problem of finding

a general way of understanding consistency so that its equation with satisfiability in

a model is more than a matter of definition. He goes on to reiterate the claim that

development of proof theory has made it possible to delimit such a conception within

number theory and analysis – i.e. “that of the impossibility of arriving deductively

at an inconsistency”.

1928 and is found in the Hilbert Nachlass, Cod. 685: 9,2. Thanks to an anonymous
referee for drawing my attention to this.

— 7 —


8 Walter Dean Vol. xx

In this case Bernays states that the Completeness Theorem does indeed show

that “each requirement that does not lead deductively to an inconsistency can . . . be

satisfied” and thus that the “identification of existence with consistency appears to

receive exact confirmation”. But he also stresses that this coincidence is “far from

obvious”. For as he notes, even if we define the inconsistency of a formula A as the

non-existence of a model in which A is satisfied, the passage from the consistency

of ¬A to the existence of a satisfying model still requires that the validity of the

principle that the failure of the negation of a universal proposition (i.e. not all M,

M 6|= A) entails an existential one (i.e. there exists M |= A). Noting that this form of

inference is in general non-constructive, Bernays issues the following admonishment:

The common acceptance of the explanation of mathematical existence in terms of consistency

is no doubt due in considerable part to the circumstance that on the basis of the simple cases

one has in mind, one forms an unduly simplistic idea of what consistency (compatibility) of

conditions is. One thinks of the compatibility of conditions as something which the complex

speaks of directly such that one only needs to make clear the content of the conditions in order

to see whether they are in agreement or not. In fact, however, the role of the conditions is that

they a↵ect each other in functional use and by combination. That which results in such a way

is not contained as a constituent part of what is given through the conditions. [4], p. 98

These remarks were written at a time when the metamathematical ramifications

of the Completeness Theorem were just beginning to be understood. Nonetheless,

they are indicative that Bernays already realized that the methods of Gödel or of

Henkin do not always yield a model which can reasonably be described as being

“produced from within” or being a “constituent part” of a consistent set of axioms.

The non-constructive aspects of the Completeness Theorem are, of course, now well

known in virtue of its equivalence to WKL.13 However Bernays also appears to have

appreciated this aspect in virtue of the relationship of the Completeness Theorem to

results such as the Löwenheim-Skolem theorem which are now often thought of as

means of demonstrating the non-categoricity of theories such as PA or GB.

He returned to comment on such connections in his last (1970) philosophical

paper “Schematic Correspondence and Idealized Structures”. Here Bernays first ob-

served that once we have adopted the axiomatic method, the Completeness Theorem

provides a form of “harmony” between the semantic and deductive consequences of a

set of first-order statements. But he then goes on to observe that the formalization of

analysis and set theory naturally leads to the use of second-order axiomatizations – an

approach which is already explored in Hilbert’s Göttingen lectures and is developed

in detail in Supplement IV of the second volume of the Grundlagen.

13 See [19] XIII.2 for discussion of this in the context of Reverse Mathematics and com-
putability theory and (e.g.) [16] in the constructive setting.

— 8 —


No. x Bernays and the Completeness Theorem 9

But as Bernays was also in a good position to appreciate by this time, it is also

possible to e↵ect a kind of reduction of second- to first-order logic by treating the

membership (or predication) relation of a second-order theory as a “basic axiomatic

relation, analogously to the incidence relation in geometry” ([4], p. 184). Once

such a step is undertaken, he remarks that it becomes possible to construct not only

non-standard models of arithmetic but also models of set theoretic systems like S or

GB which are non-standard in virtue of possessing either a countable domain or a

restricted range of second-order quantification.14

The question thus arises how we should regard such models – e.g. in comparison

to their “intended” counterparts. Bernays appears to have remained agnostic on the

significance of second-order logic for securing categorical descriptions of mathematical

structure which have occupied many latter-day theorists. For as he had already made

clear in [1], he viewed his own axiomatization of set theory in as a two-sorted first-

order system. And he also stops short of endorsing a “non-axiomatic” understanding

of second-order theories. For as he stressed earlier neither concept-formation nor

proof in classical mathematics require us to “transgress” an axiomatic understand-

ing of such theories ([4], p. 117) – e.g. by adopting a semantic understanding of

second-order consequence.

Bernays did, however, use this opportunity to underscore a point which appears

to apply specifically to the Arithmetized Completeness Theorem and which elaborates

his remarks in [2]:

By following the idea of Hilbert to make the deductive structure the object of study, the the-

ory is in a sense projected into number theory. The resulting number-theoretic structure is,

in general, essentially di↵erent from the structure intended by the theory. But it can serve to

recognize the consistency of the theory from a standpoint that is more elementary than the

assumption of the intended structure. [4], p. 186

The context of this passage makes clear that Bernays was well aware that a model

of set theory or analysis constructed in this manner must be non-standard with re-

spect not only to its interpretation of membership and domain of quantification, but

also its interpretation of “natural number” as well. This in turn raises the question of

how his invocation of a ‘more elementary’ number theoretic standpoint can be recon-

ciled at this stage with both his appreciation of the role of the Completeness Theorem

in securing assertions of mathematical existence and also his recognition that this re-

sult can itself be formalized in first-order arithmetic. Although subsequent work in

Reverse Mathematics has shed considerable light on related matters (see, e.g., [19],

IX.2-3), a more thorough examination of this question must await another occasion.

14 Kreisel additionally applied the arithmetized completeness theorem to S in precisely
this way in the course of his incompleteness proof in [14].

— 9 —


10 Walter Dean Vol. xx

References

[1] P. Bernays. A system of axiomatic set theory : Part I. Journal of Symbolic Logic,

2(1):65–77, 1937.

[2] P. Bernays. A system of axiomatic set theory: Part VII. Journal of Symbolic Logic,

19(2):81–96, 1954.

[3] P. Bernays. Betrachtungen zum Paradoxen von Thoralf Skolem. In Avandlinger utgitt av

Det Norske Videnskaps-Akademi i Oslo, pages 3–9, Oslo, 1957. Aschehoug. Reprinted

in [4], pp. 113-118.

[4] P. Bernays. Abhandlungen zur Philosophie der Mathematik. Wiss. Buchgesellschaft,

Darmstadt, 1976.

[5] W. Ewald and W. Sieg, editors. David Hilbert’s Lectures on the Foundations of Logic

and Arithmetic 1917 – 1933. Springer, 2013.

[6] H. Friedman. Some systems of second-order arithmetic and their use. In Proceedings

of the International Congress of Mathematicians, Vancouver 1974, volume 1, pages

235–242. Canadian Mathematical Congress, 1975.

[7] G. Gabriel and B. MacGuinness, editors. Gotlob Frege: Philosophical and mathematical

correspondence. Blackwell, 1980.

[8] K. Gödel. On the completeness of the calculus of logic. In Solomon Feferman et al.,

editors, Collected Works Volume 1, pages 44–123. Oxford Univeristy Press, 1929.

[9] P. Hájek and P. Pudlák. Metamathematics of First-Order Arithmetic. Springer, 1998.

[10] D. Hilbert. Problems of the grounding of mathematics. Mathematische Annalen, 102:1–

9, 1929.

[11] D. Hilbert and W. Ackermann. Grundzüge der theoretischen Logik. Springer, first

edition, 1928. Reprinted in [5].

[12] D. Hilbert and P. Bernays. Grundlagen der Mathematik, volume I. Springer, 1934.

[13] D. Hilbert and P. Bernays. Grundlagen der Mathematik, volume II. Springer, 1939.

[14] G. Kreisel. Note on arithmetic models for consistent formulae of the predicate calculus.

Fundamenta mathematicae, 37:265–285, 1950.

[15] G. Kreisel. Note on arithmetic models for consistent formulae of the predicate calculus.

II. In Actes du XIeme Congres International de Philosophie, volume XIV, pages 39–49.

North-Holland, 1953.

[16] G. Kreisel. Church’s Thesis: A kind of reducibility axiom for constructive mathematics.

In Intuitionism and Proof Theory, pages 121–150. North-Holland, Amsterdam, 1970.

[17] M. Rabin. On recursively enumerable and arithmetic models of set theory. Journal of

Symbolic logic, 23(4):408–416, 1958.

[18] W. Sieg. Beyond Hilbert’s Reach? In David Malament, editor, Reading natural philos-

ophy: essays in the history and philosophy of science and mathematics, pages 363–405.

Open Court, 2002.

[19] S. Simpson. Subsystems of second order arithmetic. Cambridge University Press, Cam-

bridge, second edition, 2009.

[20] H. Wang. Undecidable sentences generated by semantic paradoxes. The Journal of

Symbolic Logic, 20(1):31–43, 1955.

[21] R. Zach Completeness before Post: Bernays, Hilbert, and the development of proposi-

tional logic. Bulletin of Symbolic Logic, 5(03):331–366, 1999.

— 10 —