Contributions to the Metamathematics of Arithmetic

acta philosophica gothoburgensia 30
Contributions to the
Metamathematics of Arithmetic
Fixed Points, Independence, and Flexibility
Rasmus Blanck
Thesis submitted for the Degree of Doctor of Philosophy in Logic
Department of Philosophy, Linguistics and Theory of Science
University of Gothenburg
© olof rasmus blanck, 2017
isbn 978-91-7346-917-3 (print)
isbn 978-91-7346-918-0 (pdf )
issn 0283-2380
The publication is also available in full text at:
http://hdl.handle.net/2077/52271
Distribution:
acta universitatis gothoburgensis
Box 222, 405 30 Göteborg, Sweden
acta@ub.gu.se
Typeset in Adobe Garamond Pro using XƎLATEX
Cover design by Peter Johnsen
Printed by Ineko, Kållered 2017
Abstract
Title: Contributions to the Metamathematics of Arithmetic:
Fixed Points, Independence, and Flexibility
Author: Rasmus Blanck
Language: English (with a summary in Swedish)
Department: Philosophy, Linguistics and Theory of Science
Series: Acta Philosophica Gothoburgensia 30
ISBN: 978-91-7346-917-3 (print)
ISBN: 978-91-7346-918-0 (pdf )
ISSN: 0283-2380
Keywords: arithmetic, incompleteness, flexibility, independence,
non-standard models, partial conservativity, interpretability
This thesis concerns the incompleteness phenomenon of first-order arith-
metic: no consistent, r.e. theory T can prove every true arithmetical sen-
tence. The first incompleteness result is due to Gödel; classic generalisations
are due to Rosser, Feferman, Mostowski, and Kripke. All these results can
be proved using self-referential statements in the form of provable fixed
points. Chapter 3 studies sets of fixed points; the main result is that dis-
joint such sets are creative. Hierarchical generalisations are considered, as
well as the algebraic properties of a certain collection of bounded sets of
fixed points. Chapter 4 is a systematic study of independent and flexible
formulae, and variations thereof, with a focus on gauging the amount of
induction needed to prove their existence. Hierarchical generalisations of
classic results are given by adapting a method of Kripke’s. Chapter 5 deals
with end-extensions of models of fragments of arithmetic, and their relation
to flexible formulae. Chapter 6 gives Orey-Hájek-like characterisations of
partial conservativity over different kinds of theories. Of particular note is
a characterisation of partial conservativity over IΣ1. Chapter 7 investigates
the possibility to generalise the notion of flexibility in the spirit of Fefer-
man’s theorem on the ‘interpretability of inconsistency’. Partial results are
given by using Solovay functions to extend a recent theorem of Woodin.

Acknowledgements
Writing a thesis throws you from joy to despair, and hopefully back again.
This is to express my gratitude to all of you who have contributed to the
joyous side of the process: colleagues, friends, family, and students.
I have benefited from having many thesis advisors over the years: Ali
Enayat, Christian Bennet, Dag Westerståhl, and Fredrik Engström. This
would never have been possible without you. Thank you for the effort,
time, and belief you put in me.
Ali, when you first came to the department, I was suffering from a motiv-
ational dip and had almost given up on logic. You remedied this by inviting
me to work with you, even before you formally became my advisor. Thank
you for being such an inspiration to me, and for your overwhelming gen-
erosity and patience. Christian, thank you for starting all this when I first
set foot in the old Philosophy department years ago; the path has not been
straight, but I hope the apple hasn’t fallen too far from the tree. Dag, thank
you for making it possible to start my graduate studies in Göteborg. Fre-
drik, thank you for steady guidance, and for your ability to ask exactly the
right questions at the right time.
A more collective thank-you goes to the members of the logic group, and
to the participants of the logic seminar at the department of Philosophy,
Linguistics and Theory of Science. I’d also like to mention the reading
group on models of arithmetic that Saeideh Bahrami and Zach McKenzie
organised during their visit to the department.
Martin Kaså, your friendship is invaluable to me; I have no idea how
I could ever have endured these years without your regular knocks on my
door. Peter Johnsen, thank you for the beautiful cover design of this book.
It’s been a pleasure sharing an office with a number of other graduate
students, in rough order of appearance: Martin Filin Karlsson, Stellan
Petersson, Pia Nordgren, Erik Joelsson, and Alla Choifer. Thank you for
making office hours (and evenings, and weekends) much more enjoyable.
Costas Dimitracopoulos, thank you for agreeing to be the external re-
viewer of this thesis, and for your help with spotting a number of misprints
in an earlier version of the manuscript.
Among international colleagues, I am grateful to Albert Visser, Taishi
Kurahashi, Volker Halbach, and Volodya Shavrukov for expressing interest
in and commenting on my work. Volodya has also gracefully allowed me
to include one of his unpublished results in Chapter 7.
I have been dependent on scholarships to fund my graduate studies, and
therefore I wish to acknowledge generous financial support from the fol-
lowing foundations:
Stiftelsen Anna Ahrenbergs fond för vetenskapliga m.fl. ändamål, Kungliga
och Hvitfeldtska stiftelsen, Adlerbertska stipendiestiftelsen, Stiftelsen Paul och
Marie Berghaus donationsfond, Stiftelsen Henrik Ahrenbergs studiefond, and
Bertil Settergrens fond.
There is a life outside the department too. Without my friends in the
band Räfven I might have finished this thesis on time, or perhaps not at all.
You’ve brought me to far more places around the world that I could ever
expect and given me much energy and inspiration.
I would also very much like to thank Niklas Rudbäck and Per Malm,
for our writing retreats at Näs and Grönskhult, and for your continuous
reminder of the elm/beech distinction; Erik Börjeson, for our hiking trips
and for many other distractions; my parents Eva and Hans, for supporting
me in oh so many ways.
Jonna, my dear. I believe that you have suffered most during my periods
of hard work, head in the clouds. Your support and understanding seem
endless. Therefore, my most heartfelt thanks go to you.
Göteborg, April 2017
Rasmus Blanck
Contents
1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1 Scope, theme, and topics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 About this thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.1 Notation and conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2 Arithmetised meta-arithmetic . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Model theory of arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.4 Recursion theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3 Sets of fixed points . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.1 Recursion theoretic complexity . . . . . . . . . . . . . . . . . . . . . . . 32
3.2 Counting the number of fixed points . . . . . . . . . . . . . . . . . . 34
3.3 Hierarchical generalisations . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.4 Algebraic properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4 Flexibility in fragments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.1 Definitions and motivation . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.2 Mostowski’s and Kripke’s theorems . . . . . . . . . . . . . . . . . . . . 44
4.3 Flexibility and independence in Robinson’s arithmetic . . . . 47
4.4 Refinements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.5 Scott’s lemma and Lindström’s proof . . . . . . . . . . . . . . . . . . 52
4.6 Chaitin’s incompleteness theorem . . . . . . . . . . . . . . . . . . . . . 55
5 Formalisation and end-extensions . . . . . . . . . . . . . . . . . . . 57
5.1 Formalisation of Kripke’s theorem . . . . . . . . . . . . . . . . . . . . 57
5.2 Formalisation of the GRMMKV theorem . . . . . . . . . . . . . . 60
5.3 Hierarchical generalisations . . . . . . . . . . . . . . . . . . . . . . . . . . 63
6 Characterisations of partial conservativity . . . . . . . . . . 65
6.1 The Orey-Hájek characterisation and its extensions . . . . . . . 66
6.2 A characterisation of partial conservativity over IΣ1 . . . . . . 68
6.3 Language extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
6.4 Theories that are not recursively enumerable . . . . . . . . . . . . 72
7 Uniformly flexible formulae and Solovay functions . . 75
7.1 Woodin’s theorem and its extensions . . . . . . . . . . . . . . . . . . . 76
7.2 Digression: On coding schemes . . . . . . . . . . . . . . . . . . . . . . 81
7.3 Uniformly flexible formulae . . . . . . . . . . . . . . . . . . . . . . . . . 84
7.4 Partial results on uniformly flexible Σ1 formulae . . . . . . . . . 87
7.5 Hierarchical generalisations: Asking the right question . . . . 92
8 Concluding remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
Sammanfattning på svenska . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
1 Introduction
A major insight of mathematical logic is that truth and provability are com-
plicated concepts. This thesis aims to contribute to the study of the intricate
relationship between truth and provability in formal theories suitable for
describing the natural numbers 0, 1, 2, 3, …
The single most influential technical result describing this relationship is
Gödel’s first incompleteness theorem. Pick any formal system that is free
of contradiction, and for which there is an effective procedure to decide
whether a given sentence is an axiom of the system or not. If it is possible
to carry out a certain amount of elementary arithmetic within this system,
then it is also possible to construct a sentence pertaining to natural numbers
that is true but impossible to prove in the system.¹ The proof of the first
incompleteness theorem can be paraphrased by appealing to the classic liar
paradox. Consider the sentence
This sentence isn’t true.
If that sentence were true, it would truthfully claim its own falsehood –
but then the sentence would be false. If the sentence is false, then it falsely
asserts its own falsehood, and must therefore be true. Hence, no truth value
can be ascribed to the sentence without giving rise to a contradiction.
In formal theories of arithmetic, this observation amounts to a proof
that the concept of arithmetical truth is not definable in arithmetic. On
the other hand the concept of provability within a fixed system T is defin-
able in arithmetic, which allows for the construction of an arithmetical
counterpart of
This sentence isn’t provable within T.
¹(Gödel, 1931). The reader familiar with Gödel’s incompleteness theorem is already un-
easy with the way that this famous result is paraphrased here. Fear not: technical details
abound in Chapter 2.
1
contributions to the metamathematics of arithmetic
To actually construct such a sentence in elementary arithmetic is an im-
pressive technical feat, also due to Gödel. If the sentence above is false,
then it falsely claims its own unprovability in T. Therefore the sentence
must be provable in T. If T only proves true sentences, then the sentence
must be true. But then the sentence truthfully claims its own unprovability
in T, and is therefore true and unprovable in T.
The argument leading up to the true-but-unprovable sentence is differ-
ent from that of the liar paradox, in the respect that it does not lead to a
contradictory statement. It simply exhibits one aspect of the complicated
relationship between truth and provability in formal theories of arithmetic.
In effect: no arithmetically definable formal theory of arithmetic can be
complete in the sense that it proves all and precisely all true arithmetical
sentences.
The study of incompleteness phenomena is no longer in the mainstream
of mathematical logic. (And logic is still not in the mainstream of neither
mathematics nor philosophy.) This does not, however, mean that all the
important problems of the field have been settled. The central parts of this
thesis study incompleteness phenomena for their own sake, in an attempt
to further the knowledge in the field. The question guiding the research
reported in this thesis has been:
[W]hat more can we say about systems of arithmetic than that
they are all incomplete? (Hájek and Pudlák, 1993, p. 3)
A more philosophically inclined researcher may perhaps want to investig-
ate why formal arithmetical theories must fail in describing what we expect
them to describe. Yet another researcher, with concrete applications in
mind, may instead want to ask when incompleteness phenomena matter.
While these are interesting questions (and perhaps even more so than the
guiding question stated above), they do not fall within the scope of this
thesis.
1.1 Scope, theme, and topics
This thesis concerns the incompleteness phenomena of formal, first-order
theories of arithmetic, and the following paragraphs delineate the scope,
2
introduction
theme, and topics treated. The point of departure for this thesis is Gödel
(1931), where the incompleteness theorems are presented for the first time.
The first incompleteness theorem states that for any ω-consistent, r.e. exten-
sion T of formal number theory, there is a proposition undecidable in that
theory, in the sense that this proposition is neither provable nor refutable
in T, while the second incompleteness theorem states that the formalised
consistency statement of T, ConT, is an example of such a proposition.
Rosser’s (1936) generalisation of the first incompleteness theorem weakens
the assumption of ω-consistency to that of mere consistency.
An important method used in the proofs of the aforementioned incom-
pleteness results, and in many proofs in this thesis, is that of constructing
self-referential sentences. The existence of such sentences is guaranteed by
the diagonal lemma, stating that for every arithmetical formula φ(x), and
every theory T satisfying some reasonable assumptions, there is a sentence
δ which is provably equivalent with φ(pδq) in T. Hence every formula is
guaranteed to have at least one provable fixed point in this sense. Here, this
method is studied from slightly different perspective than usual, by consid-
ering the collection of fixed points of a given formula. It is an easy corollary
to the proof of the diagonal lemma that every formula has infinitely many
syntactically distinct fixed points, inspiring the question:
What more can be said about the collection of syntactically
distinct fixed points of a formula than that it is infinite?
This question is recently treated by Halbach and Visser (2014). The main
result presented in this thesis is that every such collection of provable fixed
points is creative, in the recursion theoretic sense. Hierarchical generalisa-
tions are also considered.
In his 1961 paper, Mostowski introduced the class of independent for-
mulae: such a formula has exactly one free variable, and the property that
the only propositional combinations of its instances that are provable in T
are the tautologies.² The existence of such a formula is a generalisation of
the first incompleteness theorem. Almost simultaneously, Kripke, in his
²Mostowski calls these formulae free, but this terminology seems to have fallen out of style
almost immediately.
3
contributions to the metamathematics of arithmetic
1962 paper (which was submitted some weeks before Mostowski’s paper)
defined the concept of flexible formulae: in Kripke’s words, formulae such
that ‘their extensions as sets are left undetermined by the formal system’.
He showed that a flexible formula exists, and that every flexible formula
is also independent. Hence, the existence of a flexible formula is in turn
a generalisation of Mostowski’s generalisation of the first incompleteness
theorem.
Feferman (1960) obtained a generalisation of the second incompleteness
theorem, showing that not only is ConT undecidable in T under reasonable
assumptions on T, T + ¬ConT is even interpretable in T under the same
assumptions. Here, an interpretation is taken as a means of redefining the
notions of the former theory in such a way that every theorem of the former
theory becomes provable in the latter.
The research reported in this thesis attempts to generalise these general-
isations of the incompleteness theorems in a number of ways. One kind
of generalisation is to scrutinise what the ‘reasonable assumptions’ on the
formal theories are, and one way of obtaining such generalisations is to con-
sider how much mathematical induction is needed to prove the existence of
independent and flexible formulae. Many results in the literature on flex-
ible formulae are stated only for extensions of PA, while it is evident that
the assumption that T extends PA is unnecessarily strong. Fine-tuning the
amount of induction needed for the existence proofs forms a part of the
study of fragments of arithmetic, and this line of generalisation is initiated
in Chapter 4, and continued in part in Chapter 5.
Another way to generalise the incompleteness theorems is to consider
not only r.e. extensions of formal arithmetic, but theories defined by for-
mulae of higher complexity. The first published result of this kind is due to
Jeroslow (1975), who showed that every consistent extension of arithmetic
whose set of theorems is ∆2-definable is still Π1-incomplete, even though
there are such extensions that prove their own consistency. For an inves-
tigation of such self-supporting theories, see Kaså (2012). In two recent
papers (Kikuchi and Kurahashi, 20xx; Salehi and Serahi, 2016) the first in-
completeness theorem is generalised to show that for every Σn+1-definable,
Σn-sound extension of arithmetic T, there is a true Πn+1 sentence that is
4
introduction
undecidable in T. A further generalisation is obtained here, by showing
that similar results hold for independent and flexible formulae as well.
A grand generalisation along the lines of Feferman’s result would be to
show that not only are there independent and flexible formulae, but also
that the independence and flexibility is somehow interpretable in arith-
metic. Put formally, a formula γ(x) is Σn-flexible over T iff, for every
Σn formula σ(x), the theory T + ∀x(γ(x) ↔ σ(x)) is consistent. This
means that the extension of a flexible formula can consistently be claimed
to coincide with the extension of any Σn formula. The goal would then be
to show the ‘interpretability of flexibility’ in the sense that, with γ(x) and
σ(x) as above, T+∀x(γ(x) ↔ σ(x)) is interpretable in T. Partial results
of this kind are given.
To fully appreciate the nature of the partial results alluded to above, it is
necessary to take non-standard models of arithmetic into consideration. Re-
call that a formula is flexible if its extension as a set is left undetermined by
the formal system at hand. This means that the theory obtained by adding
to T the sentence ∀x(γ(x) ↔ σ(x)) is consistent. By the completeness
theorem for first-order logic, there is then a model of this augmented the-
ory. By the nature of models of first-order arithmetic, every such model
is an end-extension of the standard model of arithmetic N. The syntactical
notion of interpretability can be characterised by the semantical notion of
end-extendability: for any two consistent r.e. theories T, S extending PA,
S is interpretable in T iff every model of T can be end-extended to a model
of S. This characterisation is discussed in some detail in Chapter 6, where
also a number of extensions of the Orey-Hájek-Guaspari-Lindström char-
acterisation are established. Of particular note is a version of the OHGL
characterisation for extensions of IΣ1.
In light of the characterisation of interpretability, it makes sense to ask:
even if not every model of T can be end-extended to a model of S, can
there be some models of T having such end-extensions? In Chapter 5 it is
shown that this is indeed the case, in particular, there is a Σn+1 formula
γ(x) such that for every σ(x) ∈ Σn+1, every model of T + ConT can be
end-extended to a model of T + ∀x(γ(x) ↔ σ(x)). This result is in turn
extended to encompass many of the refinements given in Chapter 4.
5
contributions to the metamathematics of arithmetic
Woodin (2011) establishes the existence of an r.e. setWe with the follow-
ing properties: We is empty in the standard model, and ifM is a countable
model of PA, and if s is an M-finite set that extends We, then there is an
end-extension of M in which We = s. This result has a flavour of inde-
pendence in Mostowski’s sense, flexibility in Kripke’s sense, as well as of
interpretability as discussed in the preceding paragraphs. In Chapter 7, it
is shown that the countability assumption on M can be removed, hence
establishing an interpretability result in the spirit of Feferman, but only for
these ‘finitely flexible’ formulae. Moreover, it is shown that if the restriction
to countable models is kept, then Woodin’s result holds true for extensions
of IΣ1, by using the extended version of the OHGL characterisation.
Partial results on ‘the interpretability of flexibility’ are given. In particu-
lar, it is shown that Σ2-flexibility is indeed interpretable, in the sense that
there is a Σ2 formula γ(x) such that for every σ(x) ∈ Σ2, every model of
T can be end-extended to a model of T + ∀x(γ(x) ↔ σ(x)). This result
can in turn be generalised to show that for every n, there is a Σn+2 formula
as above, such that the extension can be taken to be Σn-elementary. The
problem of obtaining Σn-elementary extensions for Σn+1 formulae seems
to be much more difficult.
1.2 About this thesis
This thesis reports on work done within two different projects under two
different sets of thesis advisors. Chapter 3 reports on work done under
supervision of Christian Bennet, Fredrik Engström, and Dag Westerståhl
(main advisor), and concerns properties of sets of provable fixed points in
arithmetical theories. Chapters 4 through 7 results from work done under
supervision of Christian Bennet, Ali Enayat (main advisor), and Fredrik
Engström. These chapters share the common theme of studying independ-
ent and flexible formulae of arithmetic, their relationship, and generalisa-
tions of those notions.
One ambition in writing this thesis is to give an as complete as possible
description of the studied areas. In doing so, given that earlier results in this
specific field date between 1930 and 2016, it is often necessary to include a
number of theorems that are not original. When this is the case, the origin
6
introduction
of these theorems is clearly stated. Results with no explicit attribution are
due to the author.
After this introductory chapter, the second chapter introduces the neces-
sary background and notations that are used in the substantial chapters 3
through 7. Since the technical results in those chapters draws from many
different sources, such as the metamathematics of first- and second-order
arithmetic, recursion theory and model theory, the background chapter is
rather extensive.
Chapter 3 is based on Blanck (2011). The objects of study in this chapter
are sets of provable fixed points in arithmetical theories. The main result
is that each such set is creative. Hierarchical generalisations are considered,
as well as some preliminary results on the algebraic structure of certain
collections of sets of fixed points.
Chapter 4 introduces the central notions of independent and flexible for-
mulae, and investigates their relationship. It also acts as a literature review
by going through a number of previously published results, but also adding
a handful of new generalisations. This chapter is an expanded version of
Blanck (2016).
Chapter 5 shifts attention from the syntactic study in Chapter 4, to
instead focus on models of arithmetical theories. It is shown that most of
the results of Chapter 4 can be formalised, giving rise to particular end-
extensions of models of arithmetic. The contents of Chapter 5 is again
based on Blanck (2016) but the hierarchical generalisations in Section 5.3
appear here for the first time.
Chapter 6 gives an overview of the famed Orey-Hájek characterisation of
interpretability and some of its extensions. For use in some applications in
Chapter 7, some other essentially well-known results are included. A new
characterisation of partial conservativity over IΣ1 is given. The original
results appearing in this chapter have been previously published in Blanck
and Enayat (2017).
Chapter 7 focuses on stronger generalisations of theorems from chapters
4 and 5. Partial results on the interpretability aspect of flexible and in-
dependent formulae are given. The original results of Section 7.1 and the
coding schemes of Section 7.2 have appeared in Blanck and Enayat (2017).
7

2 Background
The purpose of this chapter is to provide the necessary background material
for the rest of this thesis. The results presented in this chapter are all listed
as Facts; some of these are rather obvious, while other are substantial, more
or less well known, theorems. No proofs of the Facts are given, except
in the rare cases where it is difficult to find a proof in the literature. The
terminology is chosen to emphasise that these results are the foundation
upon which this thesis rests.
The reader is assumed to be acquainted with first-order logic, the first-
order theories Q (Robinson’s arithmetic) and PA (Peano arithmetic), naive
set theory, and the basic theory of recursive functions. More details on
the material presented below can be found in the more or less standard
textbooks Hájek and Pudlák (1993); Kaye (1991); Lindström (2003); Ro-
gers (1967); Smoryński (1985). Another source, relevant for many of the
hierarchical generalisations, is Beklemishev (2005).
2.1 Notation and conventions
The objects of study in this thesis are formal, first-order theories, formu-
lated in (finite extensions of ) the language of arithmetic LA, which con-
tains the non-logical symbols 0, S, +, ×, <. Theories are regarded as sets
of sentences: the set of non-logical axioms of the theory. Each theory de-
noted T, S, . . . , possibly with subscripts or other decorations, is assumed
to be a consistent extension of Robinson’s arithmetic Q. If T is a theory,
Th(T) is the set of theorems of T, i.e., the sentences provable from T.
The terms, formulae and sentences of LA are defined as usual. The
numerals are written 0, 1, 2, . . . , without bars or other devices otherwise
used to indicate numerals. Generally, the symbols used for formal variables
are x, y, z, u, and v, while the symbols used for numerals are e, i, j, k,m,
n. Both kinds of symbols may appear with subscripts or other decorations.
9
contributions to the metamathematics of arithmetic
Sentences and formulae of LA are denoted by lower case Greek letters,
while upper case Greek letters are used for sets of sentences or formulae. The
variables displayed are almost always exactly the free variables of a formula,
and x¯ is sometimes used to denote any finite sequence of free variables.
Fix a Gödel numbering of terms and formulae. pφq denotes the numeral
representing the Gödel number of φ. pφ(x˙)q denotes the numeral repres-
enting the Gödel number of the sentence obtained by replacing x with the
value of x. Hence x is free in pφ(x˙)q but not in pφ(x)q. The symbol
:= is used to denote equality between formulae. Let > := 0 = 0, and
⊥ := ¬>.
Models are structures for a first-order language; this language is always
(a finite extension of ) the language of arithmetic LA. A model consists
of a non-empty set (called the domain), together with interpretations of
the non-logical symbols for functions, relations and constants. Models are
denoted M, N , K, M′, M0, and similarly. The domain of a model M is
denoted byM , while elements of the domain are generally denoted a, b, c.
There is one privileged model, the standard model of arithmetic (denoted
N), consisting of the set ω of natural numbers, together with the symbols
of LA under their intuitive interpretations. A sentence is true, if it is true
in N. Any model that is not isomorphic to the standard model is called
non-standard.
If φ(x) is an LA-formula and M an LA-structure with a ∈ M , the
notation M |= φ(a) is shorthand for ‘φ(x) is true in M when x is inter-
preted as a’. It is also possible to treat φ(a) as shorthand for a formula φ(c)
in an expanded languageL = LA + {c}. If M is anLA-structure, and
a ∈M , then (M, a) denotes theL -structure where c is interpreted as a.
The set of finite binary strings is denoted by <ω2, and when s and t are
finite binary strings, s_t denotes their concatenation. The set of functions
from a set X to {0, 1} is denoted by X2, and ω<ω denotes the set of non-
empty finite subsets of ω.
The notation ∃x ≤ tφ(x) is used as shorthand for ∃x(x ≤ t ∧ φ(x)),
and similarly ∀x ≤ tφ(x) denotes ∀x(x ≤ t → φ(x)), where t is some
LA-term. The initial quantifiers of these formulae are bounded, and a for-
mula containing only bounded quantifiers is a bounded formula.
10
background
Definition 2.1 (The arithmetical hierarchy).
1. ∆0 = Σ0 = Π0 is the class of bounded formulae ofLA.
2. A formula is Σn+1 iff it is of the form ∃x1 . . . ∃xkpi(x1, . . . , xk, y¯),
where pi(x1, . . . , xk, y¯) is Πn.
3. A formula is Πn+1 iff it is of the form ∀x1 . . . ∀xkσ(x1, . . . , xk, y¯),
where σ(x1, . . . , xk, y¯) is Σn.
The notation introduced above, along with the definition of the arithmet-
ical hierarchy is standard in many textbooks on models of arithmetic such
as Kaye (1991), Hájek and Pudlák (1993), and Kossak and Schmerl (2006).
It is, however, not as standard in the literature on arithmetised metamath-
ematics, e.g. Feferman (1960), Bennet (1986), Lindström (2003). As this
thesis lies in the intersection of these two fields, an intermediate class PR
of primitive recursive formulae is therefore introduced, with the following
properties:
Fact 2.2 (Cf. Lindström, 2003, Chapter 1).
1. The class PR contains ∆0, and is primitive recursive.
2. PR is closed under propositional connectives and bounded quanti-
fication.
3. If φ(x1, . . . , xn) is PR, then Q ` φ(k1, . . . , kn) iff φ(k1, . . . , kn)
is true.
4. If φ(x1, . . . , xn, y¯) is PR, then ∃x1 . . . ∃xnφ(x1, . . . , xn, y¯) is Σ1,
and ∀x1 . . . ∀xnφ(x1, . . . , xn, y¯) is Π1.
In what follows, Γ is either Σn+1 or Πn+1 and Γ+ is either Σn or Πn
or PR. Γd is Σn if Γ is Πn, and vice versa. A Σn formula is ∆Tn (or ∆Mn )
if it is equivalent in T (or M) to a Πn formula, and ∆n = ∆Nn . Note that
PR ⊂ ∆1. Bn is the class of Boolean combinations of Σn formulae.
For some applications below, it is necessary to consider finite extensions
L of LA. It is possible to relativise the definition of the arithmetical
hierarchy to the extended language, and the resulting classes are denoted
11
contributions to the metamathematics of arithmetic
Σn(L ), Πn(L ), Γ(L ), and so on. In those cases that L = LA ∪ {c},
where c is a single constant, the notation Σn(c) etc. is used for brevity.
WheneverL = LA, the reference toL is omitted.
Definition 2.3. For every n, IΣn(L ) is the theory obtained by augment-
ing Robinson’s Q with an induction axiom for every formula in Σn(L ).
Since Σ0 = ∆0, I∆0(L ) is identical to IΣ0(L ).
Definition 2.4. The theory I∆0(L ) + exp is obtained from I∆0(L ) by
adding an axiom asserting that the exponentiation function is total.
The induction axioms referred to above are assumed to be formulated
with parameters. This has the convenient consequence that if L is an ex-
pansion ofLA obtained by adding finitely many constants, then for all n,
IΣn ` IΣn(L ).
The strength of the theories Q, I∆0, I∆0 + exp, IΣ1, IΣ2, . . . , PA is
strictly increasing; each theory in the list proves all the consequences of the
previous ones, and no theory proves all the consequences of a later theory.
The theories IΣn+1 and I∆0 + exp are the strong fragments of PA, while
the weak fragments of arithmetic are the ones occurring strictly between
I∆0 + exp and Q. Q, I∆0 + exp and IΣn are finitely axiomatisable, but
PA is not. It is not known if I∆0 is finitely axiomatisable.
In these theories, it is possible to prove some useful closure properties
of the classes in the arithmetical hierarchy. The first two items below are
presumably folklore, while the last is explicitly stated in Hájek and Pudlák
(1993, p. 63–64).
Fact 2.5.
1. Every finite conjunction (or disjunction) of Γ(L ) formulae is, prov-
ably in first-order logic, equivalent to a Γ(L ) formula.
2. Every Γ(L ) formula is, provably in I∆0(L ), equivalent to a Γ(L )
formula with only one quantifier in each block.
3. In IΣn+1(L ) the classes Σn+1(L ) and Πn(L ) are closed under
bounded quantification.
12
background
2.2 Arithmetised meta-arithmetic
This section is devoted to introducing the necessary concepts and results
from the field here called arithmetised meta-arithmetic. Most, if not all,
definitions and facts stated here can be found in Hájek and Pudlák (1993)
or Lindström (2003).
The formula ρ(x0, . . . , xn) numerates the relation R(k0, . . . , kn) in T
if, for every k0, . . . , kn,
R(k0, . . . , kn) iff T ` ρ(k0, . . . , kn).
Hence, ξ(x) numerates the set X in T if, for every k,
k ∈ X iff T ` ξ(k).
Moreover, ρ(x0, . . . , xn) binumerates the relation R(k0, . . . , kn) in T if,
for every k0, . . . , kn,
R(k0, . . . , kn) iff T ` ρ(k0, . . . , kn), and
not R(k0, . . . , kn) iff T ` ¬ρ(k0, . . . , kn).
Hence, ξ(x) binumerates the set X in T if, for every k,
k ∈ X iff T ` ξ(k), and
k /∈ X iff T ` ¬ξ(k).
The existence of well-behaved (bi)numerations is guaranteed by the follow-
ing four results.
Fact 2.6 (Feferman, 1960). A set X is primitive recursive iff there is a PR
formula that binumerates X in Q.
Fact 2.7 (Ehrenfeucht and Feferman, 1960). Let T be a consistent, r.e.
extension of Q, and let X be any r.e. set. There is then a Σ1 formula (and
also a Π1 formula) that numerates X in T.
Fact 2.8 (Putnam and Smullyan, 1960). Let T be a consistent, r.e. exten-
sion of Q, and let X0 and X1 be disjoint r.e. sets. There is then a Σ1
formula ξ(x) such that ξ(x) numeratesX0 in T and ¬ξ(x) numeratesX1
in T.
13
contributions to the metamathematics of arithmetic
In particular, if X is a recursive set, then there is a Σ1 formula (and
therefore also a Π1 formula) that binumerates X in T.
Definition 2.9. A set X of sentences is monoconsistent with a theory T
iff T + φ is consistent for all φ ∈ X .
Fact 2.10 (Lindström, 1979, Lemma 4). Let T be a consistent, r.e. exten-
sion of Q, and let X and Y be r.e. sets, Y monoconsistent with T. There
is then a Σ1 formula (and also a Π1 formula) ξ(x) such that for every k, if
k ∈ X , then T ` ξ(k), and if k /∈ X , then ξ(k) /∈ Y .
Given a formula τ(z), let Prfτ (x, y) be a formula expressing the relation
‘y is a proof of the sentence x from the set of sentences satisfying τ(z)’.
Then Prfτ (x, y) is Γ+ whenever τ(z) is. Let Prτ (x) := ∃yPrfτ (x, y) and
Conτ := ¬Prτ (⊥). Whenever τ(z) is Σn+1, Prτ (x) is Σn+1 and Conτ
is Πn+1. For any formula τ(z), let (τ |y)(z) := τ(z) ∧ z ≤ y, and
(τ + y)(z) := τ(z) ∨ z = y.
If T is an r.e. theory, PrfT(x, y), PrT(x), PrT+y(x), ConT, etc. denotes
ambiguously Prfτ (x, y), Prτ (x), Prτ+y(x), Conτ , etc., where τ(z) is any
PR binumeration of T. A theory T is Γ-definable if there is a τ(z) ∈ Γ
such that T = {k ∈ ω : N |= τ(k)}. If T is Γ-definable but not r.e., τ(z)
is instead assumed to be any Γ formula defining T in N.
The first part of the following useful fact is due to Craig (1953), and
the latter part to Grzegorczyk et al. (1958). The generalisation to extended
languages is immediate.
Fact 2.11 (Craig’s trick).
1. For every Σ1(L )-definable theory there is a deductively equivalent
PR-definable theory.
2. For every Σn+2(L )-definable theory there is a deductively equival-
ent Πn+1(L )-definable theory.
Hence, by Fact 2.6, every r.e. (that is, Σ1-definable) theory has a de-
ductively equivalent axiomatisation that is binumerated by a PR formula
in Q.
Many properties of the proof and provability predicates are provable in
I∆0 + exp. The following observations are sometimes useful:
14
background
1. I∆0 + exp ` ∀x(τ(x) → τ ′(x)) → ∀y(Prτ (y) → Prτ ′(y))
2. I∆0 + exp ` ∀x(τ(x) → τ ′(x)) → (Conτ ′ → Conτ )
3. I∆0 + exp ` ∀x∀y(Prτ+x(y) ↔ Prτ (x→ y))
4. I∆0 + exp ` ∀x(Prτ (x) ∧ Prτ (¬x) → ¬Conτ )
5. I∆0 + exp ` ∀x(Prτ (¬x) ↔ ¬Conτ+x)
6. I∆0 + exp ` ∀x(Prτ (x) ↔ ¬Conτ+¬x).
A number of constructions of this thesis make use of some kind of self-
referential statements. The existence of such statements follows from the
following facts. The first is essentially due to Gödel (1931); it is stated in
full generality in Carnap (1937).
Fact 2.12 (Diagonal lemma). For every Γ+ formula γ(x), a Γ+ sentence
ξ can be effectively found, such that
Q ` ξ ↔ γ(pξq).
The next two generalisations of the diagonal lemma are due to Ehren-
feucht and Feferman (1960) and Montague (1962), respectively.
Fact 2.13 (Parametric diagonal lemma). For every Γ+ formula γ(x, y), a
Γ+ formula ξ(x) can be effectively found, such that for every k ∈ ω,
Q ` ξ(k) ↔ γ(k, pξ(k)q).
Fact 2.14 (Uniform diagonal lemma). For every Γ+ formula γ(x, y), a Γ+
formula ξ(x) can be effectively found, such that
I∆0 + exp ` ∀x(ξ(x) ↔ γ(x, pξ(x˙)q)).
The following three results show the incompleteness of sufficiently strong
axiomatisable formal theories of arithmetic. The first two are due to Gödel
(1931), and the third is due to Rosser (1936). The original results were
stated for much stronger theories; see, e.g., Tarski et al. (1953) and Hájek
and Pudlák (1993) for the subsequent refinements.
15
contributions to the metamathematics of arithmetic
Fact 2.15 (The first incompleteness theorem). Let T be any consistent, r.e.
theory extending Q. Then there is a true Π1 sentence γ such that T 0 γ.
Fact 2.16 (The second incompleteness theorem). Let T be any consistent,
r.e. theory extending I∆0 + exp. Then T + ¬ConT is consistent.
Fact 2.17 (Rosser’s incompleteness theorem). Let T be any consistent, r.e.
theory extending Q. Then there is a Π1 sentence ρ such that T 0 ρ and
T 0 ¬ρ.
A related limitative result is Tarski’s theorem on the undefinability of
truth. A truth-definition for T is a formula Tr(x) such that for every sen-
tence φ, T ` φ↔ Tr(pφq).
Fact 2.18 (Tarski, 1933). Let T be any consistent extension of Q. There
is no truth-definition for T.
On the other hand, there are partial truth-definitions, and partial satis-
faction predicates, for extensions of I∆0 + exp; these go back to Hilbert
and Bernays (1939).
Fact 2.19. LetL be a finite extension ofLA. For every k and everyΓ(L ),
there is a k + 1-ary Γ(L )-formula SatΓ(L )(x, x1, . . . , xk), such that for
every Γ(L )-formula φ(x1, . . . , xk) with exactly the variables x1, . . . , xk
free, I∆0(L ) + exp proves
∀x1 . . . ∀xk(φ(x1, . . . , xk) ↔ SatΓ(L )(pφq, x1, . . . , xk)).
Such a formula is called a partial satisfaction predicate for Γ(L ).
It follows from the above that for every Γ(L ), there is a Γ(L )-formula
TrΓ(L )(x), such that for every Γ(L )-formula φ(x),
I∆0(L ) + exp ` ∀x(φ(x) ↔ TrΓ(L )(pφ(x˙)q)),
and consequently for every Γ(L )-sentence φ,
I∆0(L ) + exp ` φ↔ TrΓ(L )(pφq).
16
background
Such a formula is called a partial truth predicate for Γ(L ). These formulae
can be used to construct hierarchical provability predicates. Let, for each
Γ(L ),
PrT,Γ(L )(x) := ∃z(z ∈ Γ(L ) ∧ TrΓ(L )(z) ∧ PrT(pz˙ → x˙q)).
Hence PrT,Γ(L )(x) is the provability predicate corresponding to the theory
defined by τ(x) ∨ TrΓ(L )(x), where τ(x) is any PR binumeration of T.
Let ConT,Γ(L ) be the sentence ¬PrT,Γ(L )(⊥).
The next fact, provable Γ-completeness, has its roots with Hilbert and
Bernays (1939). A detailed proof of the Σ1 case is found in Feferman
(1960), see also Beklemishev (2005).
Fact 2.20. Let σ(x1, . . . , xn) be any Γ formula. Then
I∆0 + exp ` ∀x1, . . . , xn(σ(x1, . . . , xn) → PrT,Γ(pσ(x˙1, . . . , x˙n)q)).
In particular, if σ(x1, . . . , xn) is a Σ1 formula,
I∆0 + exp ` ∀x1, . . . , xn(σ(x1, . . . , xn) → PrT(pσ(x˙1, . . . , x˙n)q)),
and this can be verified in IΣ1 (Hájek and Pudlák, 1993, Theorem i.4.32).
The provability predicates are subject to the following very useful condi-
tions; they originate with Hilbert and Bernays (1939), subsequently refined
by Löb (1955). For the hierarchical versions presented here, see Smoryński
(1985); Beklemishev (2005).
Fact 2.21 (The Hilbert-Bernays-Löb derivability conditions). Let X be
any set of Γ sentences such that T+X is consistent. Then for all sentences
φ, ψ,
1. if T +X ` φ, then I∆0 + exp +X ` PrT,Γ(pφq)
2. I∆0 + exp ` PrT,Γ(pφq) ∧ PrT,Γ(pφ→ ψq) → PrT,Γ(pψq)
3. I∆0 + exp ` PrT,Γ(pφq) → PrT,Γ(pPrT,Γ(φ)q).
Similar statements also hold for formulae with free variables.
17
contributions to the metamathematics of arithmetic
T is Γ-sound if every Γ sentence provable in T is true, and T is sound iff
T is Γ-sound for all Γ. A theory is Γ-complete iff all true Γ-sentences are
provable in T. The theories Q, I∆0+exp, PA, IΣ1 etc. are all Σ1-complete,
and are assumed to be sound. An extension of such a theory need not be
sound; for example, if T is r.e. and consistent, and even if T is sound,
the consistent theory T + ¬ConT is not Σ1-sound. The following fact
exhibits some essentially well-known properties of these notions, cf., e.g.,
Lindström (2003), Beklemishev (2005), Kikuchi and Kurahashi (20xx),
and Salehi and Seraji (2016). A model-theoretic characterisation of Σn-
soundness appears in Section 2.3 below.
Fact 2.22.
1. If T is Σn-sound, then T is Πn+1-sound.
2. If T is Πn-complete, then T is Σn+1-complete.
If X is any set, then X|k = {n ∈ X : n ≤ k}. A theory T is reflexive
if T ` ConT|k for every k. T is essentially reflexive if every extension of T
in the same language is reflexive.
Fact 2.23 (Mostowski, 1952). PA is essentially reflexive.
If T is essentially reflexive, then T ` φ → Conφ for all φ ∈ LA.
Reflexivity does not imply essential reflexivity: the theory PRA of primitive
recursive arithmetic is reflexive but not essentially reflexive.
It follows from the first incompleteness theorem that no finitely axiomat-
isable theory can be reflexive. There is, however, a notion of small reflection
that holds even for finitely axiomatisable theories. This notion is based on
that of ‘restricted provability from true Γ sentences’ and has indispensable
use in this thesis.
Let PrnT(x) be a formula expressing that there is a proof of x, whose
Gödel number is less than n. For most reasonable Gödel numberings, this
also restricts the length of all formulae occurring in the proof, as well as
the number of quantifier alternations in those formulae, to be less than
n. A proof of φ from T with these properties is called an n-proof of φ.
Similarly, ConnT means that there is no proof of contradiction from T, if
only considering proofs whose Gödel numbers are less than n.
18
background
Let PrnT,Γ(L )(pφ(x˙)q) denote the formula
∃ψ ≤ n(ψ ∈ Γ(L ) ∧ TrΓ(L )(ψ) ∧ PrnT(pψ → φ(x˙)q)),
i.e., ‘there is an n-proof of φ(x) from a true Γ(L ) sentence whose Gödel
number is less than n’. If T is r.e. and Γ(L ) = Σk+1(L ), then PrnT,Γ(L )
is Σk+1(L ). Let ConnT,Γ(L ) denote ¬PrnT,Γ(L )(⊥). The desired reflection
principle for this provability notion follows from the next fact, which is due
to Feferman (1962, Lemma 2.18).³
Fact 2.24. Let T be an r.e. theory formulated in a finite languageL ⊇ LA
and let φ(x) ∈ L . Then for all n ∈ ω,
I∆0(L ) + exp ` ∀x(PrnT(pφ(x˙)q) → φ(x)).
Fact 2.25 (Small reflection). Let T be an r.e. theory formulated in a finite
languageL ⊇ LA, and let φ(x) ∈ L . For each n ∈ ω,
I∆0(L ) + exp ` ∀x(PrnT,Γ(L )(pφ(x˙)q) → φ(x)).
Proof. Pick φ(x) ∈ L , fix n ∈ ω and reason in I∆0(L ) + exp:
Pick x. If ¬PrnT,Γ(L )(pφ(x˙)q), then the implication is vacu-
ously true. Hence suppose that PrnT,Γ(L )(pφ(x˙)q). Then
∃ψ ≤ n(ψ ∈ Γ(L ) ∧ TrΓ(L )(ψ) ∧ PrnT(pψ → φ(x˙)q).
Now recall Fact 2.24, and continue reasoning in I∆0(L ) + exp:
It follows that ψ → φ(x), and ψ follows from TrΓ(L )(ψ).
Hence φ(x), so ∀x(PrnT,Γ(L )(pφ(x˙)q) → φ(x)).
This principle can also be formalised (Verbrugge and Visser, 1994), which
yields I∆0(L ) + exp ` ∀zPrT(p∀x(PrzT,Γ(L )(φ(x)) → φ(x))q).
An important concept is that of partial conservativity, which in its general
form appears in Guaspari (1979). Earlier examples of partial conservative
sentences can be found in, e.g., Kreisel (1962).
³Feferman’s result is stated for extensions of PA, but is well known to hold for extensions of
I∆0+exp (Hájek and Pudlák, 1993, Lemma iii.4.40; Beklemishev, 2005, Lemma 2.2).
19
contributions to the metamathematics of arithmetic
Definition 2.26. A sentence θ is Γ(L )-conservative over a theory T iff
for all γ ∈ Γ(L ), whenever T + θ ` γ, then T ` γ. In other words,
T + θ and T have the same Γ(L )-consequences.
The notion of partial conservativity is occasionally used in an extended
sense, saying that (for theories S ` T) S is Γ(L )-conservative over T iff
for all γ ∈ Γ(L ), whenever S ` γ, then T ` γ.
A related notion is that of an interpretation of one theory in another.
Roughly speaking, S is interpretable in T if the primitive concepts and
variables of S are definable in T in a way that turns every theorem of S into
a theorem of T. It is easy to see that if T ` S, then S is interpretable in T.
Further properties of interpretations are discussed in Chapter 6.
Fact 2.27 (Feferman, 1960). Let T be any consistent, r.e. extension of
I∆0 + exp. Then T + ¬ConT is interpretable in T.
2.3 Model theory of arithmetic
A model of arithmetic is a first-order structure that is adequate for the lan-
guage LA. A detailed introduction to models of arithmetic, containing
most of the material covered here, is Kaye (1991). The first three facts are
standard tools from the general theory of first-order models. The first is due
to Gödel (1930), as is the countable case of the second; the uncountable
case is due to Maltsev (1936).
Fact 2.28 (The completeness theorem). LetX be a set of sentences. Then
X has a model iff X is consistent.
Fact 2.29 (The compactness theorem). Let X be a set of sentences. Then
X has a model iff every finite subset of X has a model.
Fact 2.30 (The Löwenheim-Skolem theorem (1915), (1920)). Let T be a
theory formulated in a countable languageL . If T has an infinite model,
then T has a countable model.
Non-standard models of arithmetic contain infinitely many ‘infinitely
large’ non-standard elements. A useful feature of these elements is that
20
background
some properties holding of arbitrarily large standard numbers spill over to
the non-standard elements. The notion of overspill is originally due to
Robinson (1963), while the hierarchical version stated here is from Hájek
and Pudlák (1993).
Fact 2.31 (Overspill). LetM |= IΣn(L ). Suppose that a ∈M , and that
φ(x, y) is a Σn(L ) (or Πn(L )) formula such that
M |= φ(n, a) for all n ∈ ω.
Then there is a b ∈M \ ω such that M |= ∀x ≤ bφ(x, a).
If M is a submodel of N , and for all a ∈M and all γ(x) ∈ Γ,
M |= γ(a) ⇔ N |= γ(a),
then M is a Γ-elementary submodel of N , in symbols M ≺Γ N . Equi-
valently, N is said to be a Γ-elementary extension of M.
Let M and N be models of arithmetic, and suppose that M is a sub-
model of N . Then M is an initial segment of N , or equivalently, N is an
end-extension of M, in symbols M⊆e N , iff
for each a ∈ N \M , N |= b < a for all b ∈M .
If M ⊆e N , then N is a ∆0-elementary extension of M: hence ∆0
formulae are absolute between end-extensions. An important consequence
of this is that Σ1-sentences are preserved when passing to an end-extension:
if σ is a Σ1-sentence, M |= σ and M ⊆e N , then N |= σ. Conversely,
Π1-sentences are preserved when passing to an initial submodel.
Recall that Th(T) denotes the set of theorems of T. Analogously, the
notation Th(M), where M is an L -structure, is used for the set of sen-
tences that hold in M, i.e. {φ ∈ L : M |= φ}. Furthermore, for each Γ,
the set ThΓ(M) is defined as {φ ∈ Γ : M |= φ}. The model-theoretic
characterisation of soundness can now be given:
Fact 2.32. T is Σn-sound iff T + ThΣn+1(N) is consistent.
21
contributions to the metamathematics of arithmetic
Let M be any model of arithmetic, and let R be a relation in Mn.
Then R is M-definable if there is a formula φ(x1, . . . , xn) such that R =
{〈a1, . . . , a1〉 : M |= φ(a1, . . . , an)}. If this φ can be chosen as a Γ
formula, then R is Γ-definable in M.
Due to the existence of partial truth definitions TrΓ(x) of complexity Γ,
the set
TrueΓ(M) = {m ∈M : M |= TrΓ(m)}
of ‘true Γ-sentences’ as calculated within M is Γ-definable in M. Hence
TrueΓ(M)∩ω = ThΓ(M). Using the hierarchical consistency statement
ConT,Σn introduced in the previous section, the assertion that ‘M thinks
that T + TrueΣn(M) is consistent’, which would otherwise require triple
subscripts, can now be conveniently expressed as M |= ConT,Σn .
Letnεa be Ackermann’s epsilon notation, meaning that then’th position
of the binary expansion of a is 1. Then a can be understood as a code for
the set consisting of all the n’s such that nεa. Let M be a non-standard
model of PA. Then SSy(M), the standard system of M, is the collection
of sets X ⊆ ω such that for some a ∈ M , X = {n ∈ ω : M |= nεa}.
Then a is said to be a code for X , and X is coded in M. Moreover, every
coded set has arbitrarily small non-standard codes.
Fact 2.33. Let M be a non-standard model of IΣn, and let φ(x) be any
Σn formula. Then {k ∈ ω : M |= φ(k)} is coded in M.
Let T be a complete, consistent theory. Rep(T) is the collection of sets
X ⊆ ω representable in T, i.e. the sets for which there exists a ξ(x) that
binumerates X in T.
Fact 2.34 (Wilkie, 1977). If M |= PA, and T is a complete, consistent
extension of PA, then there is an N |= T end-extending M iff
1. Rep(T) ⊆ SSy(M);
2. T ∩Π1 ⊆ Th(M).
The next result is a refinement of Friedman’s embedding theorem, due
to Ressayre (1987), and Dimitracopoulos and Paris (1988), independently.
22
background
Fact 2.35. If M and N are two countable models of IΣ1 with a ∈ M
and b ∈ N , then the following are equivalent:
1. M is embeddable as an initial segment of N via an embedding f
with f(a) = b;
2. SSy(M) = SSy(N ), and ThΣ1(M, a) ⊆ ThΣ1(N , b).
The arithmetised completeness theorem (ACT) states that the canonical
proof of the completeness theorem can be carried out within a suitable
arithmetic theory, such as PA, and this theorem a useful tool for producing
end-extensions of models of arithmetic. The version that is sufficient for
all applications in this thesis (Fact 2.38) is an easy corollary to the next two
facts. First, it is necessary to introduce some new notation: the closure
of a set X under propositional connectives and bounded quantification
is denoted Σ0(X). By Lemma i.2.14 of Hájek and Pudlák (1993), IΣn
proves induction for all Σ0(Σn) formulae.
The following ‘mild refinement’ of the arithmetised completeness the-
orem is essentially due to Paris (1981); the version stated here is from Cor-
naros and Dimitracopoulos (2000).
Fact 2.36 (The arithmetised completeness theorem). Let M |= IΣn+1.
LetL be a language inM, extendingLA, which is ∆M1 , and let S denote
the set of sentences ofL in the sense ofM. LetA1 ⊆ S be Σn inM and
let A2 ⊆ S be Πn in M such that M |= ConA1∪A2 . Then there is a set
B with A1 ∪A2 ⊆ B ⊆ S such that:
1. for every φ ∈ S, φ ∈ B or ¬φ ∈ B;
2. B is Σ0(Σn+1) in M;
3. M |= ConB .
For the intended applications where n = 0 it is not always possible to
guarantee thatA1 andA2 areΣ0 andΠ0, respectively, only that their union
is PR. In these cases the following version of the ACT comes in handy. It
appears in Hájek and Pudlák (1993, Theorem i.4.27), the present wording
is taken from Wong (2016).
23
contributions to the metamathematics of arithmetic
Fact 2.37. IΣ1 proves: If T is a ∆1-definable consistent theory, thenT has
a definable model all of whose Σ1 properties are Σ0(Σ1)-definable.
Together, these results have the following useful consequence, which is
exactly what is used in the applications in thesis.
Fact 2.38. LetL = LA∪{c}. Suppose that M |= IΣn+1, and that T is
a theory formulated in L , such that T is Σn+1-definable in M, and that
M |= ConT. Then there is anL -structure (N , c) such that:
1. N end-extends M;
2. (N , c) satisfies the standard sentences of T.
Proof. Suppose first that n > 0, and suppose that T is Σn+1-definable, and
that M |= ConT. Then by Craig’s trick (Fact 2.11), T has a deductively
equivalent Πn definition A2, and M |= ConA2 . By Fact 2.36, there is a
complete, consistent extension B of A2 which is Σ0(Σn+1)-definable in
M, soB is the elementary diagram of some modelN ofA2 (and therefore,
of T). SinceM |= IΣ0(Σn+1), it is possible to define an embedding from
M onto an initial submodel of N .
Now, suppose that n = 0, and that T is Σ1-definable. Then T has
a deductively equivalent PR definition, whence this definition is ∆1. By
Fact 2.37, there is a definable model N of T, all of whose Σ1 properties
are Σ0(Σ1)-definable. Since M |= IΣ0(Σ1), it is again possible to embed
M onto an initial submodel of N .
The next result concerns the existence of non-standard initial segments
satisfying stronger theories. It is due to McAloon (1982); cf. D’Aquino
(1993).
Fact 2.39. If M is a countable non-standard model of I∆0, and T is a
Σ1-sound LA-theory, then there is some non-standard initial segment of
M that is a model of T. In particular, for every non-standard a ∈M , M
has a non-standard initial segment below a that is a model of PA.
Although this thesis deals mainly with first-order arithmetic, models of
second-order arithmetic appear occasionally; hence the need to introduce
24
background
some terminology. More details, and proofs of the results below, can be
found in Simpson (1999). The language of second-order arithmetic, L2,
is two-sorted; it has a number sort, and a set sort. There is also a symbol
for set membership, ∈. WKL0 is the subsystem of second-order arithmetic
consisting of Q plus induction for Σ1-formulae in L2, plus weak König’s
lemma, i.e. the statement that every infinite subtree of the full binary tree
has an infinite path.
A model of second-order arithmetic is a tuple (M,A), where M is a
first-order structure and A is a collection of subsets of M . If (M,A) is a
model of second-order arithmetic, M is referred to as its first-order part.
The following result is due to Harrington for countableM (unpublished,
see Simpson, 1999, Lemma ix.1.8 and Theorem ix.2.1); the uncountable
case is due to Hájek (1993).
Fact 2.40. Every model M of IΣ1 can be expanded to a model (M,A)
of WKL0.
Fact 2.41 (Simpson, 1999, Theorem iv.3.3). WKL0 proves the compact-
ness theorem and the completeness theorem.
The final result of this section follows immediately from Fact 2.40 and
the completeness theorem.
Fact 2.42. WKL0 proves the same first-order sentences as IΣ1.
2.4 Recursion theory
The reader is assumed to be familiar with the concepts of (partial) recursive
functions and Turing machines. The material presented here can be found
in any of the two detailed introductions to recursion theory Kleene (1952)
and Rogers (1967). For a careful development of formalised recursion
theory of the kind introduced below, the reader is directed to Smoryński
(1985, Chapter 0).⁴
⁴Some of the results below could equally well be thought to belong to Section 2.2, in
that they concern the formalisation of some parts of recursion theory within arithmetic.
In that case, Section 2.2 would have to appear after the present section, with a similar
comment added to the introduction of that section.
25
contributions to the metamathematics of arithmetic
Definition 2.43. A set Y ⊂ ω is recursive in X (or X-recursive) if Y is
solvable under the assumption that X is solvable; in symbols Y ≤T X .
The notation X ≡T Y is shorthand for Y ≤T X and X ≤T Y .
Fact 2.44 (The enumeration theorem, Kleene, 1952, Theorem XXII). Let
X be any set. For each k, there is a function that is universal for k-ary
X-recursive functions: that is, a function ΦXk (x, y1, . . . , yk) that is par-
tial recursive in X , and is such that ΦXk (n, y1, . . . , yk) for n ∈ ω is an
enumeration, with repetitions, of all the partialX-recursive functions of k
variables.
This enumeration is acceptable in the sense of Rogers (1967): there is
an effective correspondence between the partialX-recursive functions and
Turing machines with an oracle for X . For each partial X-recursive func-
tion ϕXe , let the e’th X-r.e. set, WXe , be the domain of ϕXe . If f is a
function such that f ' ϕXe for some e, then e is an X-index for f . The
reference to X is omitted whenever X is a recursive set.
Say that a relation (set, function) is Σn iff it is definable in N by a Σn
formula, and similarly for Πn. A relation is ∆n(N) iff it is definable in N
by both a Σn and a Πn formula. Formulae in these classes are subject to a
strong normal form theorem, as shown by Kleene (1952, Theorem IV).
Fact 2.45 (The normal form theorem). Let n > 0. Every k-ary Σn relation
can be defined in N by a formula of the form
∃y1∀y2 . . .QynT (e, x1, . . . , xk, y1, . . . , yn)
for a suitable choice of e. In the above formula, T is Kleene’s primitive
recursive T -predicate, Q is ∃ or ∀ depending on whether n is odd or even,
and in this latter case, T is prefixed with a negation symbol.
Similarly, every k-ary Πn relation can be defined in N by a formula of
the form
∀y1∃y2 . . .QynT (e, x1, . . . , xk, y1, . . . , yn)
for a suitable choice of e. In the above formula, T is Kleene’s primitive
recursive T -predicate, Q is ∀ or ∃ depending on whether n is odd or even,
and in the former case, T is prefixed with a negation symbol.
26
background
The next few definitions single out particularly interesting classes of sets:
the productive, creative, complete Σn, and recursively inseparable sets.
Definition 2.46. A setX is productive if there is a total recursive function
f(x) such that for all n ∈ ω, ifWn ⊆ X , then f(n) ∈ X \Wn. A setX
is creative if it is r.e. and its complement is productive.
A set Y ⊂ ω is 1-reducible to X (Y ≤1 X) if there is a recursive 1:1
function f such that k ∈ Y iff f(k) ∈ X .
Definition 2.47. A set X is complete Σn if X is Σn, and Y ≤1 X for
each Σn set Y .
Definition 2.48. Two sets X , Y are effectively inseparable if, for every
disjoint, r.e. sets X ′ ⊇ X , Y ′ ⊇ Y , it is possible to effectively find an
element of (X ′ ∪ Y ′)c.
Fact 2.49 (Myhill, 1955). X is creative iff X is complete Σ1.
If X is any r.e. set other than ω, then X is creative iff for every r.e. set
Y that is disjoint from X , X ≡T X ∪ Y . If X and Y are disjoint, r.e.,
effectively inseparable sets, then both X and Y are creative.
Let X be any set, and let {ϕXi : i ∈ ω} be an enumeration of the
X-recursive functions. Let the Turing jump of X , denoted X ′, be the set
{x : ϕXx (x) is defined}. The nth Turing jump ofX is inductively defined
by
X(0) = X
X(n+1) = (X(n))′
Of particular interest are the jumps of the empty set ∅, as they are closely
connected to the arithmetical hierarchy. This relationship is clarified in the
following fact, which is due to Post (1948).
Fact 2.50 (Post’s theorem).
1. A set X is Σn+1 iff X is r.e. in ∅(n).
2. The set ∅(n) is complete Σn.
27
contributions to the metamathematics of arithmetic
WheneverX = ∅(n) for some n ∈ ω, the notation Φnk(x, y1, . . . , yk) is
used in place of ΦXk (x, y1, . . . , yk). The superscript is completely dropped
when n = 0. By Kleene’s normal form theorem and Post’s theorem, the
relation Φnk(x, y1, . . . , yk) = z can be defined in N by a Σn+1 formula
Rnk (x, y1, . . . , yk, z). Since the arity of these formulae is always obvious
from the context, the subscript k is henceforth dropped.
A k-ary function f is strongly defined by a formula φ(x1, . . . , xk, y) in
T iff
1. if f(n1, . . . , nk) = m, then T ` φ(n1, . . . , nk,m) and
T ` ∀y(φ(n1, . . . , nk, y) → y = m);
2. if f(n1, . . . , nk) 6= m, then T ` ¬φ(n1, . . . , nk,m).
The function Φ(x, y1, . . . , yk) is recursive, and since Q is Σ1-complete,
the relation Φ(x, y1, . . . , yk) = z can be strongly represented in Q by a
Σ1 formula R(x, y1, . . . , yk, z). As pointed out by Ali Enayat, this is a
special case of a more general phenomenon.
Fact 2.51. For each n, a function f is recursive in ∅(n) (or, equivalently, f
is ∆n+1) iff f is strongly representable in Q + ThBn(N).
Proof sketch. Let f be a function recursive in ∅(n). By Post’s theorem, the
graph and the co-graph of f can both be defined in N by a Σn+1-formula.
Since the theory Q + ThBn(N) is Σn+1-complete and Πn+1-sound, f is
strongly representable in Q + ThBn(N). For the other direction, note that
ThBn(N) is recursive in ∅(n).
The following result is taken from Smoryński (1985, Theorem 0.6.9) for
the case n = 0; the hierarchical generalisation given here is supposedly
folklore. A slogan for this fact is: there is a Σn+1 function hidden within
every Σn+1 relation, and this can be verified in IΣn.
Fact 2.52 (The selection theorem). For each Σn+1-formula φ with exactly
the variables x1, . . . , xk free, there is a Σn+1-formula Sel{φ} with exactly
the same free variables, such that:
1. IΣn ` ∀x1, . . . , xk(Sel{φ}(x1, . . . , xk) → φ(x1, . . . , xk));
28
background
2. IΣn ` ∀x1, . . . , xk, y(Sel{φ}(x1, . . . , xk)∧
Sel{φ}(x1, . . . , xk−1, y) → xk = y);
3. IΣn ` ∀x1, . . . , xk−1(∃xkφ(x1, . . . , xk) →
∃xkSel{φ}(x1, . . . , xk)).
These formulae are useful in that they can be used in combination with
partial satisfaction predicates to strongly represent ∅(n)-recursive functions
in extensions of IΣn + ThBn(N), by letting ϕe be the ∅(n)-recursive func-
tion whose graph is defined by Sel{SatΣn+1}(e, y1, . . . , yk, z) in N. The
resulting enumeration is acceptable in Rogers’s sense, so whenever conveni-
ent, it can without loss of generality be assumed that
Rn(x, y1, . . . , yk, z) := Sel{SatΣn+1}(x, y1, . . . , yk, z).
Fact 2.53 (The recursion theorem). Let f(z, x1, . . . , xn) be any partial
X-recursive function. There is an X-index e such that
ϕXe (x1, . . . , xn) ' f(e, x1, . . . , xn).
This theorem is due to Kleene (1952, Theorem XXVII), and is usually
employed in the following manner. Define a recursive function f(z, x) in
stages, using z as a parameter. The resulting function may differ depending
on the choice of z. By the recursion theorem, there is an index e such that
ϕe ' f(e, x). Hence the function ϕe(x) computes the same function as
f(z, x) does when fed its own index as the first parameter. This legitimates
self-referential constructions where an index of f is being used in the actual
construction of f . The recursion theorem can be formalised in I∆0 + exp
using the diagonal lemma (Smoryński, 1985, Theorem 0.6.12; Lindström
and Shavrukov, 2008, Section 1.2). To show that, e.g., a Σn+1 function
acquired in this way is provably total, IΣn+1 is required.
29

3 Sets of fixed points
The diagonal lemma (and its variations) is frequently used to construct ‘self-
referential’ sentences in the form of provable fixed points: φ is a provable
fixed point of θ(x) in T iff T ` φ ↔ θ(pφq). Some classic results es-
tablished by this means are Gödel’s first incompleteness theorem, Tarski’s
theorem on the undefinability of truth, and Löb’s theorem. Lindström
(2003) gives many examples of how versatile the technique can be. In this
chapter, provable fixed points, or merely fixed points, are studied from an-
other perspective: given a formula θ(x) inLA, what can be said about the
set of fixed points of θ(x)?
It is a well known fact that the set of all provable fixed points of PrPA,
{φ : PA ` φ↔ PrPA(pφq)}
is creative. This is an easy corollary of Löb’s theorem (1955), together with
Smullyan’s theorem (1961) showing that the set of theorems of PA and the
set of refutable sentences of PA are effectively inseparable.
Say that a formula θ(x) is extensional (or preserves the provable equival-
ence) if, for each φ and ψ, T ` φ ↔ ψ implies T ` θ(pφq) ↔ θ(pψq).
An important subclass of the extensional formulae is the formulae that are
T-substitutable in the sense that for all φ and ψ,
T ` PrT(pφ↔ ψq) → θ(pφq) ↔ θ(pψq).
Smoryński (1987) shows that the class of T-substitutable formulae have, up
to provable equivalence in T, a unique provable fixed point, and Bernardi
(1981) generalises Smullyan’s result to show that every two different PA-
equivalence classes are effectively inseparable. It is then easy to see that the
set of provable fixed points of a substitutable formula is creative.
Bennet shows, in unpublished notes, that the set of Rosser sentences
is complete Σ1, which seems to be the first result of this kind for non-
extensional formulae. Halbach and Visser (2014) show, using a method
31
contributions to the metamathematics of arithmetic
due to McGee, that each set of fixed points is complete r.e. Their result is
mildly strengthened in this chapter to show that each set of fixed points is
creative.
3.1 Recursion theoretic complexity
Let, for each LA-formula θ(x), FixT(θ) = {φ : T ` φ ↔ θ(pφq)}. It
is evident that if T is r.e., then each FixT(θ) is r.e. The equivalence class
of ψ over T is the set [ψ]T = {φ : T ` φ ↔ ψ}. Where no confusion
will arise, the reference to T is omitted. Note that, for each sentence ψ,
[ψ] = Fix(ψ ∧ x = x), which means that the next result is a more general
form of Theorem 1 of Bernardi (1981).
Theorem 3.1. Every two disjoint sets of fixed points are effectively insep-
arable.
Proof. Let θ(x) and χ(x) be any formulae, and let X,Y be disjoint r.e.
sets containing Fix(θ) and Fix(χ), respectively. Let, by Fact 2.8, ξ(x) be
a Σ1 formula such that ξ(x) numerates X and ¬ξ(x) numerates Y in T.
Let, by the diagonal lemma (Fact 2.12), φ be such that
T ` φ↔ (θ(pφq) ∧ ¬ξ(pφq)) ∨ (χ(pφq) ∧ ξ(pφq)).
Suppose φ ∈ X . Then T ` ξ(pφq), so T ` φ ↔ χ(pφq), contradicting
the assumption that X and Y are disjoint. Suppose instead that φ ∈ Y .
Then T ` ¬ξ(pφq), and T ` φ ↔ θ(pφq), again contradicting the
assumption that X is disjoint from Y . Hence φ /∈ X ∪ Y .
By Myhill’s theorem, the concepts of creativeness and Σ1-completeness
coincide. Furthermore, every two disjoint, effectively inseparable sets are
both creative. This allows for the following conclusion, using two different
proofs, of which the latter constructs the reducing function directly.
Corollary 3.2. Every set of fixed points is creative.
Proof. Let θ(x) be any formula. It suffices to show that Fix(θ) is disjoint
from some other set of fixed points. But Fix(θ) ∩ Fix(¬θ) = ∅ on pain
32
sets of fixed points
of inconsistency of T, and Tarski’s theorem rules out the possibility that
Fix(θ) = ω. Hence Fix(θ) and Fix(¬θ) are disjoint and effectively insep-
arable, and thus both creative.
Alternative proof. Let θ(x) be any formula, let X be an arbitrary r.e. set,
and let ξ(x) be a numeration ofX . Let, by the parametric diagonal lemma
(Fact 2.13), φ(x) be such that, for all k,
T ` φ(k) ↔ (θ(pφ(k)q) ∧ ξ(k)) ∨ (¬θ(pφ(k)q) ∧ ¬ξ(k)).
It follows that k ∈ X iff φ(k) ∈ Fix(θ), so Fix(θ) is complete Σ1. By
Myhill’s result, Fix(θ) is creative.
There are plenty of complete Σ1 sets that are not sets of fixed points over
a given theory: if S is an r.e. extension of Q such that Th(S) 6= Th(T),
then Th(S) is not a set of fixed points over T. This observation follows
from the following two results, which are due to Christian Bennet.
Theorem 3.3. If X is an r.e., deductively closed, proper subset of Th(T),
there is no θ(x) such that X = FixT(θ).
Proof. Let X be an r.e., deductively closed, proper subset of Th(T), and
suppose towards a contradiction that X = FixT(θ) for some θ(x). Then
there is a sentence ψ that is provable in T but not an element ofX . By the
diagonal lemma, let φ be such that
T ` φ↔ θ(pψ ∧ φq).
Since ψ is provable, ψ ∧ φ ∈ FixT(θ) = X . But since X is deductively
closed, ψ ∈ X , which is a contradiction.
Definition 3.4. A setX is sufficiently closed if ψ ∈ X implies ψ∨γ ∈ X ,
for each sentence γ.
Theorem 3.5. IfX is an r.e., sufficiently closed, proper superset of Th(T),
there is no θ(x) such that X = FixT(θ).
33
contributions to the metamathematics of arithmetic
Proof. Let X be an r.e., sufficiently closed, proper superset of Th(T), and
suppose towards a contradiction that X = FixT(θ) for some θ(x). Then
there is a sentenceψ ∈ X that is not provable in T. By the diagonal lemma,
let φ be such that T ` φ↔ ¬θ(pψ ∨ φq).
Since ψ ∈ X and X is sufficiently closed, ψ ∨ φ ∈ X = FixT(θ).
Equivalently, T ` (ψ ∨ φ) ↔ θ(pψ ∨ φq), whence by construction of φ,
T ` (ψ ∨ φ) ↔ ¬φ. By propositional logic, T ` ψ, which is impossible.
Question 3.6. Can the collection of sets of fixed points over T be charac-
terised among the creative sets?
3.2 Counting the number of fixed points
There are at least two ways to count the number of provable fixed points of
a formula: the first is to count syntactically different sentences as different
fixed points; the other is to count only the number of equivalence classes of
fixed points. As all sets of provable fixed points are creative and therefore
non-recursive, the number of syntactically distinct fixed points must be
infinite, and the more interesting question is to consider the number of
equivalence classes involved. The results in this section are easily obtained
by applying the results of Bernardi (1981).
Theorem 3.7. If θ(x) is extensional and has finite range, then θ(x) is sub-
stitutable, whence it has a unique fixed point.
Proof. Let θ(x) be an extensional formula with finite range. By Corollary
5 of Bernardi (1981), θ(x) is constant. Hence T ` θ(pφq) ↔ θ(pψq) for
all φ, ψ, so θ(x) is substitutable, and has a unique fixed point.
For extensional formulae in general, it is possible to show a more vague
statement, namely that for each such set of fixed points, there is a recursive
enumeration of the equivalence classes contained in it.
Theorem 3.8. If θ(x) is extensional, then there is a recursive set X such
that for every φ, φ ∈ Fix(θ) iff there is a ξ ∈ X such that T ` ξ ↔ φ.
34
sets of fixed points
Proof. This follows directly from Lemma 1 in Bernardi (1981), the proof
of which is a version of Craig’s trick.
The following corollary is a parallel to Bernardi’s Theorem 6. However,
the class of fixed points does not constitute a partition of ω.
Corollary 3.9. If I ⊆ ω is such that F = {Fix(θi) : i ∈ I} constitutes
a partition of ω, thenF is not r.e. without repetition.
Proof. SupposeF is r.e. without repetition. Then ϕ ∈ Fix(θi) iff ϕ /∈ ω \
Fix(θi), whence Fix(θi) has an r.e. complement, which is not the case.
3.3 Hierarchical generalisations
Let, for each θ(x), FixΓ(θ) = Γ∩Fix(θ), and for each ψ, [ψ]Γ = Γ∩ [ψ].
Here the precise definition of the class Γ is of interest. If Γ is defined
to be closed under provable equivalence in T, then for each θ(x) and Γ,
FixΓ(θ) = Fix(θ). This situation does not arise when using the strictly
syntactical definition of the classes Γ, as given in the background chapter.
With this restriction in mind, it is possible to prove the following charac-
terisation.
Theorem 3.10 (Lindström, 2003, Exercise 2.28c). IfX is an r.e. subset of
Γ, then there is a Bn formula θ(x) such that FixΓ(θ) = X .
Hence, the interesting cases are the sets FixΓ(θ), where θ(x) is itself a Γ
formula. From this point on, assume that θ(x) is of the same complexity as
the fixed points asked for. The main result of this section is that Theorem
3.1 can be extended to hold for these bounded sets of fixed points as well
– the only additional care needed lies in choosing the correct numerations
to keep the complexity down.
Theorem 3.11. Any two disjoint sets of Γ-fixed points of Γ formulae are
effectively inseparable.
Proof. Let θ(x) and χ(x) be any Γ formulae. Suppose that FixΓ(θ) and
FixΓ(χ) are disjoint, and let X and Y be disjoint r.e. subsets of Γ con-
taining FixΓ(θ) and FixΓ(χ), respectively. If Γ 6= Π1, let, by Fact 2.8,
35
contributions to the metamathematics of arithmetic
ξ0(x) be a Π1 formula and ξ1(x) a Σ1 formula such that for i = 0, 1,
ξi(x) numerates X and ¬ξi(x) numerates Y in Q. If Γ = Π1, switch
the complexity of ξ0(x) and ξ1(x). Let, by the diagonal lemma, φ be such
that T ` φ↔ ((θ(pφq) ∧ ¬ξ0(pφq) ∨ (χ(pφq) ∧ ξ1(pφq)).
The rest of the proof is almost identical to the proof of Theorem 3.1.
It is easy to see that for an extensional formula θ(x), FixΓ(θ) is a union of
equivalence classes. Hence, if θ(x) is extensional and FixΓ(θ) 6= Γ, there
must be at least one Γ-equivalence class outside FixΓ(θ). By Theorem 3.11
it follows that whenever θ(x) is extensional, FixΓ(θ) is creative.
The next result gives a sufficient condition for a bounded r.e. set to be a
set of fixed points. Note that the condition is not necessary: any equival-
ence class 6= > satisfies the consequent, but not the antecedent of theorem.
For the statement of the theorem, the following definition is convenient.
Definition 3.12. A setX has a lower bound in T iff there is a non-refutable
sentence φ such that T ` φ→ ψ for all ψ ∈ X .
Theorem 3.13. Suppose that T is a consistent, r.e. extension of I∆0 + exp.
Let X ⊂ Γ be an r.e. set such that Xc has a lower bound. There is then a
Γ formula θ(x) such that FixTΓ(θ) = X .
Proof. LetX be any r.e. subset of Γ such thatXc has a lower boundφ; then
T+φ is consistent. If Γ 6= Π1, let by Fact 2.10, ξ(x) be a Σ1 formula such
that if k ∈ X , then T ` ξ(k), and if k /∈ X , then ξ(k) /∈ Th(T + φ). If
Γ = Π1, choose ξ(x) as a Π1 formula instead. Let θ(x) := TrΓ(x)∧ξ(x).
Suppose ψ ∈ X . Then T ` ξ(pψq) and T + ψ ` TrΓ(pψq) ∧ ξ(pψq).
Hence T ` ψ → θ(pψq). Moreover, T + θ(pψq) ` TrΓ(pψq), so it
follows that every element of X is a fixed point of θ(x).
Suppose that ψ is any Γ sentence such that ψ /∈ X . Then by the choice
of ξ(x), T + φ 0 ξ(pψq), so T + φ + ¬ξ(pψq) is consistent and proves
¬θ(pψq). Suppose now, for a contradiction, that ψ ∈ FixΓ(θ). Then
T + φ+ ¬ξ(pψq) ` ¬ψ, so by propositional logic T + φ+ ψ ` ξ(pψq).
But φ is a lower bound on Xc, whence T ` φ → ψ. It follows that
T + φ ` ξ(pψq), contradicting the choice of ξ(x).
36
sets of fixed points
The next result shows that it is possible to successively remove recurs-
ive sets from Γ, obtaining infinitely many recursive sets of Γ-fixed points.
By inseparability of disjoint sets of fixed points, each recursive set of fixed
points intersects every set of Γ-fixed points (and therefore also every Γ-
equivalence class) non-recursively. It also follows that any formula with a
recursive set of fixed points ( 6= Γ) must be non-extensional.
Theorem 3.14. Let θ(x) be any Γ formula, and let A ⊂ Γ be a recursive
set such that FixΓ(τ)∩A = ∅ for some τ(x) ∈ Γ. Then there is a formula
χ(x) ∈ Γ such that FixΓ(χ) = FixΓ(θ) \A.
Proof. Let θ(x) and A be as above. If Γ 6= Π1, let by Fact 2.8 α0(x)
be a Π1 formula and α1(x) a Σ1 formula such that αi(x) binumerates
A in Q. If Γ = Π1, switch the complexities of α0(x) and α1(x). Let
χ(x) := (θ(x) ∧ ¬α0(x)) ∨ (τ(x) ∧ α1(x)), which is then a Γ formula.
Suppose that φ ∈ A. Then it follows that T ` α0(pφq) ∧ α1(pφq),
so T ` χ(pφq) ↔ τ(pφq). Suppose further that φ ∈ FixΓ(χ). Then
T ` φ↔ τ(pφq), but A is assumed to be disjoint from FixΓ(τ), a contra-
diction.
Now suppose φ /∈ A. Then it follows that T ` ¬α0(pφq)∧¬α1(pφq),
so T ` χ(pφq) ↔ θ(pφq). Hence φ ∈ FixΓ(χ) iff φ ∈ FixΓ(θ), so
FixΓ(χ) = FixΓ(θ) \A.
3.4 Algebraic properties
This section makes essential use of partial truth predicates, so it is assumed
that T ` I∆0 + exp. For each Γ, there is then, up to provable equivalence
in T, precisely one Γ formula whose set of provable Γ-fixed points is equal
to Γ, namely TrΓ(x). LetRΓ be the set of recursive subsets of Γ. It is easy
to see thatRΓ forms a Boolean algebra when ordered under set inclusion.
Theorem 3.15. The set
FΓ = {X ⊆ Γ : X is recursive and ∃θ(x) ∈ Γ s.t. X = FixΓ(θ)},
that is, the set of recursive sets of Γ-fixed points of Γ formulae, forms a
non-principal filter onRΓ.
37
contributions to the metamathematics of arithmetic
The theorem gives a negative answer to a question left open in Blanck
(2011), and it follows from the following sequence of lemmas.
Lemma 3.16. Let F be any finite subset of Γ. Then Γ \ F is a recursive
set of Γ-fixed points, and F is not a set of Γ-fixed points.
Proof. Let F be any finite subset of Γ. Then by Theorem 3.14, Γ \ F is a
recursive set of Γ-fixed points. If F were a set of Γ-fixed points, then F
would be both recursive and creative at the same time.
Lemma 3.17. If A ∈ FΓ and A ⊆ B ∈ RΓ, then B ∈ FΓ.
Proof. Suppose A ∈ FΓ, then there is a θ(x) ∈ Γ such that A = FixΓ(θ).
Let B ⊇ A be a recursive subset of Γ. If Γ 6= Π1, let β0(x) be a Π1
formula and β1(x) be a Σ1 formula such that βi(x) binumerates B in Q.
If Γ = Π1, switch the complexities of β0(x) and β1(x). Let
ψ(x) := (TrΓ(x) ∧ β0(x)) ∨ (θ(x) ∧ ¬β1(x)),
which is then a Γ formula.
Suppose φ ∈ B. Then T ` β0(pφq) ∧ β1(pφq), so T ` φ↔ ψ(pφq),
and φ ∈ FixΓ(ψ).
Suppose φ /∈ B. Then it follows that T ` ¬β0(pφq) ∧ ¬β1(pφq), so
T ` ψ(pφq) ↔ θ(pφq). So if φ is a fixed point of ψ(x), it is also a fixed
point of θ(x), which contradicts the fact that B was chosen to contain
FixΓ(θ). Hence φ /∈ FixΓ(ψ).
Lemma 3.18. If A,B ∈ FΓ, then A ∩B ∈ FΓ.
Proof. Let A,B ∈ FΓ be such that A = FixΓ(θ) and B = FixΓ(ψ).
If Γ 6= Π1, let βi(x), for i = 0, 1 be binumerations of B as above. If
Γ = Π1, switch the complexities of β0(x) and β1(x). Let
χ(x) := (β1(x) ∧ θ(x)) ∨ (¬β0(x) ∧ ψ(x)).
Suppose φ ∈ B. Then T ` θ(pφq) ↔ χ(pφq), so φ ∈ FixΓ(χ) iff
φ ∈ FixΓ(θ) = A. Hence: the only elements of B that are fixed points of
χ(x) are the elements of A.
Suppose φ /∈ B. Then T ` χ(pφq) ↔ ψ(pφq). Since B = FixΓ(ψ),
φ can not be a fixed point of χ(x).
38
sets of fixed points
Question 3.19. IsFΓ an ultrafilter onRΓ?
It is easy to see that if A is a recursive subset of Γ, then at most one of
A and Γ \ A is in FΓ. If at least one of those is in FΓ, then FΓ is an
ultrafilter onRΓ.
39

4 Flexibility in fragments
This chapter serves multiple purposes. First, it introduces the central no-
tions of independent and flexible formulae, and surveys the literature on the
topic, from its inception in the early 1960s until 2016. A second purpose
is to introduce a general method, due to Kripke (1962), for constructing
independent and flexible formulae, which has a number of applications in
coming chapters.
Apart from these purposes, the opportunity is also taken to relate the
classic results on flexibility and independence to the modern research in
fragments of arithmetic, gauging the amount of induction needed to prove
the various results. As is pointed out by Beklemishev (1998), the question
of which of these results hold in theories weaker than PA has been largely
ignored. Hence, this chapter attempts to partly rectify this situation.
4.1 Definitions and motivation
The central notions of this chapter and the next are those of independence
and flexibility, which are due to Mostowski (1961) and Kripke (1962), re-
spectively. These terms are not used univocally in the literature, as is ex-
plained below, but for the purpose of this thesis the following definitions
are adopted. Let, for any formula φ, φ0 := φ and φ1 := ¬φ.
Definition 4.1. A formula φ(x) is independent over a theory T, iff for
every function f ∈ ω2, the theory T + {φ(n)f(n) : n ∈ ω} is consistent.
Definition 4.2. A formula γ(x) is flexible for class of formulae X over a
theory T iff for every ξ(x) ∈ X , the theory T + ∀x(γ(x) ↔ ξ(x)) is
consistent.
The definition of independence used here is equivalent to the one used
by Mostowski, although he calls such formulae free. It seems, however,
41
contributions to the metamathematics of arithmetic
that the habit of using ‘independent’, or variations thereof, for these for-
mulae emerged quickly: both Feferman et al. (1962) and Scott (1962) use
this terminology. Later sources conforming to this usage are, e.g., Lind-
ström (1984), Smoryński (1984), Sommaruga-Rosolemos (1991), Lind-
ström (2003), and Kikuchi and Kurahashi (2016). A notion of an ‘inde-
pendent set’, which is related to that of independent formulae, also appears
in Harary (1961), Kripke (1962), and Myhill (1972). Proofs essentially es-
tablishing the existence of independent formulae abound in the literature
(Mostowski, 1961, Theorem 2; Kripke, 1962, Corollary 1.1; Myhill, 1972,
Remark 2). A similar result also appears in Jeroslow (1971, Lemma 3.1),
and most recently in Hamkins (2016).
The term ‘flexible’ has a more complicated history. It is introduced
by Kripke (1962), although the meaning is somewhat different (see Sec-
tion 4.3 below). Formulae of the type described above appear in, e.g., Vis-
ser (1980), Montagna (1982), Lindström (1984), and Lindström (2003)
without a definite name, while Sommaruga-Rosolemos (1991) uses the
term ‘flexible’ without an explicit definition. The standard work Hájek and
Pudlák (1993), uses ‘flexible’ for what here is called ‘independent’, which
is at odds with the other sources listed above, and a possible source of con-
fusion.
Recall that Gödel’s first incompleteness theorem exhibits a true but T-
unprovableΠ1 sentence γ, thus instantiating the incompleteness of T at the
lowest possible level: since T isΣ1-complete, truth and provability coincide
for Σ1 sentences, and no incompleteness is possible at that level. It is trivial
to construct a Π1 formula with similar properties, e.g., a formula γ(x) such
that for each n ∈ ω, γ(n) is true but unprovable in T, and similarly a Π1
formula ρ(x) such that for every n ∈ ω, T 0 ρ(n) and T 0 ¬ρ(n).
The condition on φ(n) in Definition 4.1 is strictly stronger than the
trivial generalisations discussed in the preceding paragraph: it is equivalent
to the condition that the only propositional combinations of sentences of
the form φ(n) provable in T are the tautologies. For a simple example,
whenever φ(x) is independent over T, and m 6= n, then it follows that
T 0 φ(m) ∨ φ(n) and T 0 ¬φ(m) ∨ ¬φ(n). Elaborating on this ex-
ample, if φ(n) is Π1, then φ(n) must be true, since otherwise ¬φ(n) is
42
flexibility in fragments
a true Σ1 sentence, and therefore provable in T. With this in mind, it
is straightforward to see that the existence of an independent Π1 formula
(or equivalently, an independent Σ1 formula) is a generalisation of both
Gödel’s and Rosser’s incompleteness theorems, a perspective which is also
adopted by Mostowski (1961). Hence it is clear that the study of inde-
pendent and flexible formulae can be regarded as a study of the important
incompleteness phenomenon of formal arithmetical theories.
Although the notions of independent and flexible formulae are similar,
to the point that every flexible formula also is independent (Kripke, 1962,
Corollary 1.1; see also Theorem 4.5 below), there are still important differ-
ences between them. A key distinguishing feature can be articulated as fol-
lows. Given an independent formula ξ(x), and any prescribed set A ⊂ ω,
the completeness theorem gives rise to a model M of arithmetic such that
{n ∈ ω : M |= ξ(n)} = A. No information is, however, gotten about
the truth values of any specific non-standard instances of ξ(x). Moreover,
supposing that ξ(x) ∈ Σn and M |= IΣn, if A is cofinal in ω, then ξ(x)
holds on a downwards cofinal subset of the non-standard part of M. This
follows from the overspill principle, together with the fact that in a model
of IΣn, every bounded, Σn-definable subset of the model has a maximum.
For a flexible formula γ(x), on the other hand, the completeness the-
orem ensures the existence of a model M in which the extension of γ(x)
agrees with that of any desired formula σ(x) (of a suitable complexity class).
This does not give any absolute control of the actual content of the exten-
sion of γ(x) in M; the crucial point being that the extension of γ(x) as
calculated within M agrees with the extension of σ(x), also as calculated
within M. If any instance of σ(x) is undecidable in T, this instance may
very well have different truth values in N and M. For a concrete example,
the extension of the Σ1 formula ¬ConT ∧ x = x is empty as calculated
within N, while it can have two radically different extensions in M: either
the empty set, or the whole domain, depending on whether or not M
satisfies ConT.
43
contributions to the metamathematics of arithmetic
4.2 Mostowski’s and Kripke’s theorems
Having discussed in some detail the properties and merits of independent
and flexible formulae, it is time to prove that both kinds of formulae actu-
ally exist. Below, a detailed proof of Kripke’s theorem on the existence of
flexible formulae is given.⁵ The proof method used by Kripke, and detailed
below, is very versatile, and is applied on numerous occasions throughout
this thesis.
Theorem 4.3 (Essentially Kripke, 1962, Theorem 1). Suppose that T is a
consistent, r.e. extension of I∆0 + exp. For each n > 0, there is a Σn
formula γ(x) such that for each σ(x) ∈ Σn, the theory
T + ∀x(γ(x) ↔ σ(x))
is consistent.
Note that, in one sense, this theorem is the best possible, since it imme-
diately leads to a contradiction to assume the existence of a formula flexible
for a higher complexity than its own. Suppose, e.g., that there is a Σ1 for-
mula γ(x) that is flexible for Σ2 over T. It is then possible to choose a
formula σ(x) ∈ Σ2 such that σ(x) is provably equivalent to ¬γ(x). By
assumption, T + ∀x(γ(x) ↔ σ(x)) is consistent, which is impossible by
the particular choice of σ(x).
As in Kripke’s original proof, the theorem above is derived from an
innocent-looking lemma, establishing the existence of a partial recursive
function f with index e that is such that Q does not refute any sentences
of the form f(e) = k. Strictly speaking, the expression f(e) = k is
not a sentence in LA, but may instead be regarded as shorthand for the
LA-sentence R(e, e, k) ∧ ∃!zR(e, e, z). Here R(x, y, z) is a Σ1 formula
strongly representing the relation Φ(x, y) = z, where Φ(x, y) is a function
that is universal for partial recursive functions.
⁵Kripke states the theorem for extensions of what is essentially Robinson’s arithmetic
Q, but with a different notion of flexibility. More on this in Section 4.3. In Visser
(1980) and Lindström (2003), the theorem is proved for extensions of PA. Sommaruga-
Rosolemos (1991) states the theorem for what he calls primitive recursive arithmetic,
PRA, but his theory is augmented with induction for Σ1 formulae, thus making it
equivalent to (a conservative extension of ) IΣ1.
44
flexibility in fragments
Lemma 4.4 (Kripke, 1962, Lemma 1). Suppose that T is a consistent, r.e.
extension of Q. There is a partial recursive function f with index e (which
depends on T), such that for every k, the theory T+f(e) = k is consistent.
Proof. Define f(x) by the stipulation that f(n) = k iff
T ` ¬(R(n, n, k) ∧ ∃!zR(n, n, z)).
If more than one sentence of this form is provable in T, pick the one whose
proof has the least Gödel number. This assures that f(x) is well-defined,
and since T (and therefore also provability in T) is r.e., f(x) is a partial
recursive function. Let e be an index for f .
Pick k, and suppose, for a contradiction, that T + f(e) = k is in-
consistent. Then it follows that T ` f(e) 6= k, or equivalently, that
T ` ¬(R(e, e, k) ∧ ∃!zR(e, e, z)). But then f(e) = k by definition, so
T ` R(e, e, k) ∧ ∃!zR(e, e, z), contradicting the consistency of T.
Proof of Theorem 4.3. Let T be a consistent, r.e. extension of I∆0+exp. Let
e be as in the proof of Lemma 4.4, and recall that e depends on the actual
choice of T. Pick n > 0, and let γ(x) := ∃z(R(e, e, z) ∧ SatΣn(z, x)).
Let σ(x) be any Σn formula.
By Lemma 4.4, the theory T + f(e) = pσq is consistent, so reason in
that theory:
If γ(x), then for some z,R(e, e, z)∧SatΣn(z, x). But this z
is unique, and R(e, e, pσq) holds, so SatΣn(pσq, x). Hence
σ(x).
If σ(x), then SatΣn(pσq, x). Since R(e, e, pσq), γ(x) fol-
lows by one application of ∃-introduction.
This proves that T + f(e) = pσq ` ∀x(γ(x) ↔ σ(x)), and since the
theory T + f(e) = pσq is consistent, T + ∀x(γ(x) ↔ σ(x)) is also
consistent.
This proof of Kripke’s theorem and lemma depends essentially on the
recursion theorem for defining f(x), the representability of partial recurs-
ive functions in Q, and the existence of partial satisfaction predicates. The
45
contributions to the metamathematics of arithmetic
ingenious part of Kripke’s proof is to define the flexible Σn formula γ(x)
as expressing ‘x satisfies the Σn formula whose Gödel number is output
by f(e)’, which is possible to express formally by using the partial satis-
faction predicate for Σn. Since f(e) can consistently assume any value, it
must also be consistent that γ(x) coincides with any desired formula of a
suitable complexity.
This trick of Kripke’s, feeding the output of a function to a partial sat-
isfaction predicate or other normal form theorem, is used on a number of
occasions later on. For an immediate example, the existence of a Πn for-
mula that is flexible for Πn over T follows by letting e be an index for f as
above, and by letting γ(x) := ∀z(R(e, e, z) → SatΠn(z, x)).
In Kripke (1962), a result is proved (Corollary 1.1) which is, as pointed
out by the referee of Kripke’s paper, essentially equivalent to Mostowski’s
theorem on the existence of an independent Σ1 formula. Mostowski’s ori-
ginal proof of this result goes via a quite sophisticated witness comparison
argument (Mostowski, 1961, Theorem 2; Lindström, 2003, Theorem 2.9).
Kripke instead establishes that the instances of a Σ1-flexible formula form
an independent set over T: a set A such that, for every subset B of A, the
theory T + B + {¬α : α ∈ A \ B} is consistent. In fact, a formula
ξ(x) is independent iff {ξ(n) : n ∈ ω} is an independent set. Since the
method of showing independence by using a flexible formula has a number
of applications in this thesis, the opportunity is taken to give a perspicuous
proof.
Theorem 4.5 (Mostowski, 1961). Suppose that T is a consistent, r.e. ex-
tension of I∆0+ exp. Then there is a Σ1 formula ξ(x) that is independent
over T.
Proof. Let T be a consistent r.e. extension of I∆0 + exp, let f be any func-
tion in ω2, let ξ(x) be a Σ1-flexible Σ1 formula as in Theorem 4.3, and let
X = {ξ(n)f(n) : n ∈ ω}.
By compactness, it suffices to show that for each finite subset A of X ,
the theory T + A is consistent. Let A be any finite subset of X , let B be
the set {n : ξ(n) ∈ A}, and let β(x) be a Σ1 binumeration ofB in Q. By
Theorem 4.3, the theory T + ∀x(ξ(x) ↔ β(x)) is consistent.
46
flexibility in fragments
For each n ∈ ω:
1. If ξ(n) ∈ A, then n ∈ B, and since β(x) binumerates B in Q,
T ` β(n). But then T + ∀x(ξ(x) ↔ β(x)) ` ξ(n).
2. If ¬ξ(n) ∈ A, then n /∈ B, so T ` ¬β(n). It then follows that
T + ∀x(ξ(x) ↔ β(x)) ` ¬ξ(n).
Since the consistent theory T+∀x(ξ(x) ↔ β(x)) proves all the sentences
in A, T +A is consistent. Hence T +X is consistent.
The upcoming section elaborates on the modifications required to con-
struct the analogue of flexible formulae in theories not allowing for partial
satisfaction predicates.
4.3 Flexibility and independence in Robinson’s
arithmetic
The attentive reader reacts to the fact that the proof of Mostowski’s the-
orem, as presented above, is not stated for extensions of Q, while on the
other hand, it is well known that his theorem does apply to such extensions.
Mostowski’s original proof uses a sophisticated witness comparison argu-
ment rather than partial satisfaction predicates, and the use of the former
generates no additional difficulties in Q. It it still, however, possible to
prove Mostowski’s theorem for Q using Kripke’s method, by reverting to
Kripke’s own, nowadays somewhat peculiar-looking, notion of flexibility.
The modifications needed to obtain this rederivation in Q is the topic of
this subsection. Kripke’s original definition of flexibility can be expressed
as follows.
Definition 4.6. A formula γ(x) is flexible in Kripke’s sense for Σn over T
if every Σn relation can be defined by a Σn formula σ(x) that is such that
T + ∀x(γ(x) ↔ σ(x)) is consistent.
By Kleene’s normal form theorem, every Σn-definable relation has a
definition on Kleene normal form. Although these formulae are similar
to partial satisfaction predicates, their satisfaction-like properties can not
47
contributions to the metamathematics of arithmetic
be proved in Q, which is what motivates Kripke’s formulation above. By
replacing the partial satisfaction predicate in the definition of γ(x) with
a formula on a suitable Kleene normal form, Kripke’s original theorem
on flexible formulae is obtained. E.g., if n = 1, γ(x) can be defined as
∃z(R(e, e, z) ∧ ∃yT (z, x, y)).
Theorem 4.7 (Kripke, 1962, Theorem 1). Suppose that T is a consistent,
r.e. extension of Q. For each n > 0, there is a Σn formula γ(x) that is
flexible in Kripke’s sense for Σn over T.
Mostowski’s theorem now follows from the theorem above, by a proof
similar to the proof of Theorem 4.5. The crucial point is that the Σ1 bi-
numeration β(x) used in that proof can here be replaced by a formula
∃yT (k, x, y) for a suitable choice of k.
Another method for constructing a set independent over a given exten-
sion of Q is exhibited in Remark 2 of Kripke (1962), and similar construc-
tions appear in Jensen and Ehrenfeucht (1976), Lindström (1979), Kikuchi
and Kurahashi (2016), and Hamkins (2016). Let, by Rosser’s theorem, ρ
be a Π1 sentence that is undecidable in T. Continue by letting ρ0 be a
Π1 sentence undecidable in T + ρ and ρ1 a Π1 sentence undecidable in
T+¬ρ. Let ρ00, ρ01, ρ10, ρ11 be Π1 sentences undecidable in T+ρ∧ρ0,
T + ρ ∧ ¬ρ0, T + ¬ρ ∧ ρ1, and T + ¬ρ ∧ ¬ρ1, respectively. In gen-
eral, if s is a binary string, the Π1 sentence ρs is undecidable in T plus the
appropriate Rosser sentences or their negations, picked out by the pattern
prescribed by s, where, as usual, φ0 = φ and φ1 = ¬φ. Continue adding
Rosser sentences in this fashion, to obtain the binary branching Rosser tree,
in which every branch can be picked out by a binary sequence, and the
nodes along each such branch together with T constitute a consistent the-
ory. Then the set R, defined as
{ρ,
(ρ ∧ ρ0) ∨ (¬ρ ∧ ρ1),
(ρ ∧ ρ0 ∧ ρ00) ∨ (ρ ∧ ¬ρ0 ∧ ρ01)∨
(¬ρ ∧ ρ1 ∧ ρ10) ∨ (¬ρ ∧ ¬ρ1 ∧ ρ11), . . . }
is independent in Kripke’s sense.
48
flexibility in fragments
It is straightforward but tedious to prove this, due to the mere length
of the sentences in R. The idea is that for any combination of positive
and negative instances of the elements of R, there is a corresponding path
through the Rosser tree that proves all of these sentences. As an illustration,
let r0, r1 be the first two sentences ofR; then T+ρ+ρ0 ` r0∧r1, while
T + ρ + ¬ρ0 ` r0 ∧ ¬r1. Similarly, T + ¬ρ + ρ1 ` ¬r0 ∧ r1 and
T + ¬ρ + ρ0 ` ¬r0 ∧ ¬r1. Since all of these extended theories are
consistent by construction, {r0, r1} is independent over T. This argument
is easily extended to show that any finite subset of R is consistent, which
by compactness is sufficient to show that R is independent over T.
Let r0, r1, r2, . . . be an enumeration of all the sentences in R. Since all
of these sentences are B1, let φ(x) be a ∆2 formula such that
I∆0 + exp ` φ(k) ↔ TrB1(rk)
for all k. Then φ(x) is independent over T; see also Theorem 4.11 below
for an improvement of this result.
4.4 Refinements
The proof of Theorem 4.3 can be modified in a number of ways to yield
similar, and stronger, conclusions. For example, it is possible to construct
a recursive function f0 such that for any choice of k ∈ ω, the theory T +
f0(0) = k is consistent. More generally, for each n ∈ ω, there is a recursive
function fn such that for any choice of k ∈ ω, the theory T + fn(n) = k
is consistent. One such function comes to use in Section 4.6.
Another generalisation, suggested by Ali Enayat, is of the hierarchical
kind. Salehi and Seraji (2016) and Kikuchi and Kurahashi (20xx) discuss
generalisations of the incompleteness theorems to Σn+1-definable theories.
In particular, both papers show that for every Σn+1-definable, Σn-sound
theory there is a true Πn+1 sentence undecidable in the theory (Kikuchi
and Kurahashi, 20xx, Theorem 4.21; Salehi and Seraji, 2016, Theorem
2.5). Theorems 4.8 and 4.9 below are in turn generalisations of these results,
in that they provide Σn+1 formulae that are flexible or independent over
the Σn+1-definable theory T, rather than just exhibiting a true undecidable
Πn+1 sentence. Cf. the discussion of independent formulae in Section 4.1.
49
contributions to the metamathematics of arithmetic
Theorem 4.8. Suppose that T is a Σn+1-definable, Σn-sound extension of
I∆0+exp. There is a Σn+1 formula γ(x) such that for each σ(x) ∈ Σn+1,
the theory T + ∀x(γ(x) ↔ σ(x)) is consistent.
Proof. Let T be a Σn+1-definable, Σn-sound extension of I∆0 + exp. By
Craig’s trick (Fact 2.11), T can without loss of generality be assumed to be
Πn-definable.⁶
By Kleene’s enumeration theorem, there is a functionΦn(x, y), recursive
in ∅(n), that is universal for functions recursive in ∅(n). By Fact 2.51, let
Rn(x, y, z) be a Σn+1 formula strongly representing Φn(x, y) = z in
Q + ThΣn+1(N).
Let f(m) = k iff T ` ¬(Rn(m,m, k) ∧ ∃!zRn(m,m, z)). If more
than one sentence of this form is provable in T, pick the one whose proof
has the least Gödel number. Since T can be assumed to be Πn-definable,
provability in T, and therefore also the relation f(x) = y, is ∆n+1 and
recursive in ∅(n) by Post’s theorem.
Let e be an index for f , and suppose, for a contradiction, that for some
k ∈ ω, the theory T +Rn(e, e, k) ∧ ∃!zRn(e, e, z) is inconsistent. Then
T ` ¬(Rn(e, e, k) ∧ ∃!zRn(e, e, z)), so by definition of f , f(e) = k.
It then follows that T + ThΣn+1(N) ` Rn(e, e, k) ∧ ∃!zRn(e, e, z), so
T+ThΣn+1(N) must be inconsistent. But T is Σn-sound, so by Fact 2.32,
T + ThΣn+1(N) is consistent. This is the desired contradiction, whence
T +Rn(e, e, k) ∧ ∃!zRn(e, e, z) is consistent for each k ∈ ω.
Let σ(x) be any Σn+1 formula. By letting γ(x) be the Σn+1 formula
∃z(Rn(e, e, z)∧ SatΣn+1(z, x)), it follows that T+∀x(γ(x) ↔ σ(x)) is
consistent.
A hierarchical generalisation of Theorem 4.5 follows by an easy modific-
ation of the proof of that theorem.
Theorem 4.9. Suppose that T is a Σn+1-definable, Σn-sound extension of
I∆0 + exp. There is then a Σn+1 formula ξ(x) such that for any f ∈ ω2,
the theory
T + {ξ(k)f(k) : k ∈ ω}
is consistent.
⁶If n = 0, the proof of Theorem 4.3 goes through as it stands.
50
flexibility in fragments
Remark 4.10. By a further modification of the proof of this theorem, in
the spirit of the discussion in Section 4.3, the assumption can be weakened
to T ` Q.
Another kind of generalisation is due to Montagna (1982, Corollary 1).
Theorem 4.11. Let T be a consistent, r.e. extension of I∆0 + exp. There
is a ∆n+1 formula δ(x) such that for every Bn formula β(x), the theory
T + ∀x(δ(x) ↔ β(x)) is consistent.
This can be proved by a proof almost identical to that of Theorem 4.3,
using the fact that there is a ∆n+1 satisfaction predicate for Bn formulae.
Montagna’s original proof is stated for extensions of PA, and imitates the
quite different method used by Visser (1980) to prove the following general
theorem.⁷
Theorem 4.12 (The Gödel-Rosser-Mostowski-Myhill-Kripke-Visser The-
orem). Suppose that {Ti : i ∈ ω} is an r.e. family of consistent, r.e.
extensions of I∆0 + exp, and that {Xi : i ∈ ω} is an r.e. family of r.e. sets
of sentences such that Ti 0 ξ for all ξ ∈ Xi.
For each n > 0, there is then a Σn formula γ(x), such that for every
σ(x) ∈ Σn, every i ∈ ω, and every ξ ∈ Xi,
Ti + ∀x(γ(x) ↔ σ(x)) 0 ξ.
Proof. The goal is to use Kripke’s trick to prove the theorem, hence the
proof is similar to the proof of Theorem 4.3 via Lemma 4.4.
Let {Ti : i ∈ ω} and {Xi : i ∈ ω} be as in the statement of the
theorem. Define a partial recursive function f(x) by the stipulation that
f(m) = k iff i ∈ ω and (the Gödel number of ) ξ ∈ Xi are the least
numbers such that
Ti ` (R(m,m, k) ∧ ∃!zR(m,m, z)) → ξ.
⁷The result also appears in Sommaruga-Rosolemos (1991), stated for extensions of IΣ1,
with a proof reminiscent of the ones in Visser (1980) and Montagna (1982). Visser’s
result is stated for extensions of PA.
51
contributions to the metamathematics of arithmetic
If more than one sentence of this form is provable in Ti, choose the one
whose proof has the least Gödel number. Let e be an index for f , and
suppose that for some i, k ∈ ω, and ξ ∈ Xi,
Ti +R(e, e, k) ∧ ∃!zR(e, e, z) ` ξ.
Then f(e) = k, so I∆0 + exp ` R(e, e, k) ∧ ∃!zR(e, e, z), but then
Ti ` ξ, contradicting the assumptions on Ti and X . Let γ(x) be the Σn
formula ∃z(R(e, e, z) ∧ SatΣn(z, x)).
Let σ(x) be any Σn formula, and suppose, for a contradiction, that for
some i ∈ ω and ξ ∈ Xi,
Ti + ∀x(γ(x) ↔ σ(x)) ` ξ.
By Kripke’s trick,
Ti +R(e, e, pσq) ∧ ∃!zR(e, e, z) ` ∀x(γ(x) ↔ σ(x))
so
Ti +R(e, e, pσq) ∧ ∃!zR(e, e, z) ` ξ,
which is a contradiction. Hence for every i ∈ ω and every ξ ∈ Xi,
Ti + ∀x(γ(x) ↔ σ(x)) 0 ξ.
4.5 Scott’s lemma and Lindström’s proof
One of the most successful applications of independent formulae is due to
Scott (1962). To show that every countable Scott set can be realised as the
standard system of some prime model of PA, he generalises Mostowski’s
proof to obtain:
Theorem 4.13 (Scott’s lemma). Suppose that T is a consistent, r.e. exten-
sion of Q. For any Σn formula φ(x), there is then a Σn+1 formula ξ(x)
such that for any g, h ∈ ω2, if Tg = T+{φ(k)g(k) : k ∈ ω} is consistent,
so is Tg + {ξ(k)h(k) : k ∈ ω}.
52
flexibility in fragments
Lindström (1984) gives a generalisation of Scott’s lemma, similar to the
way in which Kripke’s theorem generalises Mostowski’s theorem. Since
Lindström (1984) is part of a departmental report series with limited cir-
culation, the result is not widely known, and the opportunity is taken to
repeat it and its proof below.
Lindström’s proof uses a slight modification of Kripke’s method: instead
of first constructing a suitable flexible function by appealing to the recur-
sion theorem and then feeding its output to a partial truth definition, the
flexible formula is constructed directly via the diagonal lemma. To give
an example of how this method can be applied, the following theorem is
proved.
Theorem 4.14 (Lindström, 1984, Proposition 1). Suppose that T is a con-
sistent, r.e. extension of I∆0 + exp, and that X is an r.e. set that is mono-
consistent with T. For each n > 0, there is then a Σn formula γ(x) such
that for every σ(x) ∈ Σn,
¬∀x(γ(x) ↔ σ(x)) /∈ X .
It is straightforward to construct a partial recursive function f with in-
dex e such that for every k, f(e) 6= k /∈ X , but in order for this to imply
that ¬∀x(γ(x) ↔ σ(x)) /∈ X (for a suitable choice of γ), it is required
that X is a deductively closed extension of I∆0 + exp. With this addi-
tional assumption the theorem is no stronger than Theorem 4.3, and this
makes it clear that Kripke’s trick depends on the deductive closure of the
set of sentences (i.e., the theory) used to define the function f . Here, the
partial recursive function f is instead defined in terms of Gödel numbers
of formulae, and the diagonalisation implemented by using the uniform
diagonal lemma rather than the recursion theorem.
Proof. Let T be a consistent, r.e. extension of I∆0 + exp, and let X be
an r.e. set monoconsistent with T. Fix n > 0, and let a partial recursive
function f be defined by the stipulation that f(pηq) = pσq iff
σ(x) ∈ Σn and ¬∀x(η(x) ↔ σ(x)) ∈ X .
53
contributions to the metamathematics of arithmetic
If there are many formulae of this kind, pick the one with the least Gödel
number. Let e be an index for f , and let by the uniform diagonal lemma
(Fact 2.14), γ(x) be a Σn formula such that
I∆0 + exp ` ∀x(γ(x) ↔ ∃z(R(e, pγq, z) ∧ SatΣn(z, x))).
Let σ(x) ∈ Σn and suppose, for a contradiction, that
¬∀x(γ(x) ↔ σ(x)) ∈ X .
Then f(pγq) = pσq, so I∆0 + exp ` R(e, pγq, pσq)∧ ∃!zR(e, pγq, z).
Using Kripke’s trick, it follows that I∆0 + exp ` ∀x(γ(x) ↔ σ(x)). But
then T + ¬∀x(γ(x)) ↔ σ(x)) is inconsistent, contradicting the assump-
tion that X is monoconsistent with T.
This method is now applied to prove Lindström’s generalisation of Scott’s
lemma.
Theorem 4.15 (Lindström, 1984, Proposition 2). Suppose that T is a con-
sistent, r.e. extension of I∆0 + exp. For any Σn formula φ(x), there is a
Σn+1 formula γ(x) such that for any g ∈ ω2, if
Tg = T + {φ(k)g(k) : k ∈ ω}
is consistent, then for every σ(x) ∈ Σn+1, Tg +∀x(γ(x) ↔ σ(x)) is also
consistent.
Proof. Fix n, and φ(x) ∈ Σn. Let f(psq, pηq) = pσq iff s is a binary
sequence of length m such that
σ(x) ∈ Σn and T + φ(0)(s)0 + · · ·+ φ(m)(s)m ` ¬∀x(η(x) ↔ σ(x)).
If there are many such σ’s, choose the one with the least Gödel number, and
if there are more than one such s for that particular choice of σ, choose the
shortest sequence. Let Seqφ(x) be the formula
∀y < l(x)((φ(y) → (x)y = 0) ∧ (¬φ(y) → (x)y = 1)),
54
flexibility in fragments
where l(x) denotes the length of the sequence x. Hence Seqφ expresses
that x is a sequence agreeing with the pattern of negations applied to φ. If
φ is Σn, then Seqφ is ∆n+1.
Let e be an index for f , and let γ(x) be a Σn+1 formula such that
T ` ∀x(γ(x) ↔ ∃s∃z(Seqφ(s) ∧R(e, s, pγq, z) ∧ SatΣn+1(z, x))).
Suppose that there is a g ∈ ω2 such that Tg is consistent but
Tg + ∀x(γ(x) ↔ σ(x))
is inconsistent. Then there is a shortest finite initial subsequence s of g
such that
T + φ(0)(s)0 + · · ·+ φ(m)(s)m ` ¬∀x(γ(x) ↔ σ(x)).
By construction of f , this implies f(psq, pγq) = pσq, so
T ` R(e, psq, pγq, pσq) ∧ ∃!zR(e, psq, pγq, z).
With s as above, Tg ` Seqφ(psq). Hence Tg ` ∀x(γ(x) ↔ σ(x)),
contradicting the assumption that Tg is consistent.
Theorem 4.13 follows from Theorem 4.15 by using the method from the
proof of Theorem 4.5.
4.6 Chaitin’s incompleteness theorem
Chaitin’s incompleteness theorem is a much-discussed incompleteness res-
ult, see e.g., van Lambalgen (1989); Raatikainen (1998); Franzén (2005);
Sjögren (2008). It is presented here for two reasons: first, because it can be
obtained as an immediate consequence of a minor modification of Kripke’s
lemma. Secondly, Chaitin’s theorem serves as a partial motivation for the
research reported in Woodin (2011), a paper that inspired much of the
work reported in Chapter 7 below.
The result can be stated in many different forms, each of which uses some
kind of complexity measure, or measure of ‘information content’, for finite
55
contributions to the metamathematics of arithmetic
binary strings (or the natural numbers used to represent these strings in
arithmetic). A binary string can then be defined to have high complexity,
or to be random, if the shortest description of an algorithm producing the
string (relative to some fixed method of describing algorithms) is at least
as long as the string itself.⁸ This conception leads Woodin to paraphrase
Chaitin’s theorem as:
[T]he property of randomness for finite binary sequences based
on information content is undecidable. (Woodin, 2011, p. 119)
The argument presented below appears, in a slightly different form, in van
Lambalgen (1989), where it is credited to Albert Visser and Dick de Jongh.
Assuming some fixed enumeration of recursive functions, the algorithmic
complexity of k, C(k), is defined as the least index e such that ϕe(0) = k
(Raatikainen, 1998).
Theorem 4.16 (E.g., Chaitin, 1974). For each sound arithmetic theory T,
there is a constant c such that T does not prove any true statements of the
form C(k) > c.
It is easy to find a constant witnessing this theorem (and more) by modi-
fying the proof of Kripke’s lemma as suggested in Section 4.4: let c be a
number such that for each k ∈ ω, the theory T+R(c, 0, k)∧∃!zR(c, 0, z)
is consistent. Observe that the expression C(k) = c can be formalised as
R(c, 0, k) ∧ ∀y<c¬R(y, 0, k). Hence the expression C(k) > c can be
formalised as
∃x(x > c ∧R(x, 0, k) ∧ ∀y<x¬R(y, 0, k)).
Theorem 4.17. Suppose that T is a consistent, r.e. extension of Q, and let
c be as above. Then no sentence of the form C(k) > c is provable in T.
Proof. Pick k ∈ ω, and suppose for a contradiction that T ` C(k) > c,
i.e.
T ` ∃x(x > c ∧R(x, 0, k) ∧ ∀y<x¬R(y, 0, k)).
In particular, T ` ¬R(c, 0, k), but by the modification of Kripke’s lemma,
the theory T +R(c, 0, k) is consistent. Hence T 0 C(k) > c.
⁸See, e.g., Li and Vitányi (1993).
56
5 Formalisation and end-extensions
By the completeness theorem for first-order logic, Lemma 4.4 establishes
the existence of models satisfying T + f(e) = k for any k ∈ ω. Trivially,
any such model is an end-extension of the standard modelN. The question
now arises whether this is a particular feature of the standard model, or if
there are other models of arithmetic that can be similarly end-extended. In
this chapter it is shown that there indeed are other models that have end-
extensions to models of T + f(e) = k for any k, and that the method
for constructing such end-extensions can be generalised to prove stronger
results of the same kind.
5.1 Formalisation of Kripke’s theorem
By inspection of the proof of Lemma 4.4, it is clear that for every k ∈ ω,
T + f(e) = k is consistent iff T is consistent, and the main observation
of Blanck (2016) is that this statement is formalisable in I∆0 + exp. In the
presence of Σ1-induction, this formalisation allows for the construction of
end-extensions of models of ConT, thus establishing:
Theorem 5.1 (Blanck, 2016). Suppose that S is a consistent, r.e. extension
of IΣ1, and that T is a consistent, r.e. extension of Q. For each n > 0,
there is then a Σn formula γ(x), such that:
1. S ` ConT → ∀x¬γ(x);
2. if σ(x) ∈ Σn, then every model of S + ConT can be end-extended
to a model of T + ∀x(γ(x) ↔ σ(x)).
The proof of this theorem rests on the next lemma, which is the afore-
mentioned formalisation of Kripke’s lemma in I∆0 + exp.
57
contributions to the metamathematics of arithmetic
Lemma 5.2 (Blanck, 2016). If T is a consistent, r.e. extension of Q, then
there is a formula with Gödel number e, such that:
1. I∆0 + exp ` ∀z(ConT → ¬R(e, e, z));
2. I∆0 + exp ` ∀z(ConT ↔ ConT+R(e,e,z)).
Proof. Let φ(x, z) := PrT(p¬R(x˙, x˙, z˙)q), and let e = pφ(x, z)q. Then
e has the desired properties. By definition of R(x, y, z):
I∆0 + exp ` ∀z(R(e, e, z) ↔ Sel{SatΣ1}(e, e, z)) (5.1)
which implies
I∆0 + exp ` ∀z(R(e, e, z) → SatΣ1(e, e, z)) (5.2)
which in turn gives
I∆0 + exp ` ∀z(R(e, e, z) → φ(e, z)). (5.3)
By construction of φ,
I∆0 + exp ` ∀z(R(e, e, z) → PrT(p¬R(e, e, z˙)q)) (5.4)
but by provable Σ1-completeness of Q,
I∆0 + exp ` ∀z(R(e, e, z) → PrT(pR(e, e, z˙)q)). (5.5)
Together with the derivability conditions, 5.4 and 5.5 give
I∆0 + exp ` ∀z(ConT → ¬R(e, e, z)) (5.6)
which concludes the proof of part 1. For part 2, observe that
I∆0 + exp ` ∃z¬ConT+R(e,e,z) ↔ ∃zPrT(p¬R(e, e, z˙)q) (5.7)
which by construction of φ implies
I∆0 + exp ` ∃z¬ConT+R(e,e,z) ↔ ∃zφ(e, z). (5.8)
58
formalisation and end-extensions
By the properties of the partial satisfaction predicate,
I∆0 + exp ` ∃z¬ConT+R(e,e,z) → ∃zSatΣ1(e, e, z) (5.9)
and
I∆0 + exp ` ∃z¬ConT+R(e,e,z) → ∃zSel{SatΣ1}(e, e, z). (5.10)
By definition of R(x, y, z), this implies
I∆0 + exp ` ∃z¬ConT+R(e,e,z) → ∃zR(e, e, z) (5.11)
so 5.6 and 5.11 together imply
I∆0 + exp ` ∀z(ConT → ConT+R(e,e,z)). (5.12)
The implication from right to left is immediate.
Proof of Theorem 5.1. Let S be a consistent, r.e. extension of IΣ1, and T a
consistent, r.e. extension of Q. Let n > 0, and let e be as in Lemma 5.2;
note that e depends on the choice of T. Then
γ(x) := ∃z(R(e, e, z) ∧ SatΣn(z, x))
is as desired.
(1) Let M be any model of S + ConT. By Lemma 5.2(1),
M |= ∀z¬R(e, e, z).
By reasoning within M, conclude that ∀x¬γ(x).
(2) Let σ(x) be any Σn formula. By Lemma 5.2(2),
M |= ConT+R(e,e,pσq).
Since M |= IΣ1 and T + R(e, e, pσq) is a Σ1-definable theory, an ap-
plication of the arithmetised completeness theorem (as stated in Fact 2.38)
now yields an end-extension N |= T + R(e, e, pσq) of M. By Kripke’s
trick, it follows that N |= ∀x(γ(x) ↔ σ(x)).
59
contributions to the metamathematics of arithmetic
The following result is due to Hamkins (2016), who quickly obtained it
after seeing a draft of Blanck and Enayat (2017). Hamkins’s proof makes
use of the Rosser tree introduced in Section 4.3, starting from a model of
PA + ¬ConPA. The result stands to Theorem 5.1 as Mostowski’s theorem
stands to Kripke’s theorem, and the proof presented here is therefore similar
to the proof of Theorem 4.5.
Theorem 5.3 (Hamkins, 2016, reformulated). Suppose that S is a con-
sistent, r.e. extension of IΣ1, and that T is a consistent, r.e. extension of
Q. There is a Σ1 formula ξ(x) such that for each M-definable function
f in M2, every model of S + ConT can be end-extended to a model of
T + {ξ(m)f(m) : m ∈M}.⁹
Proof sketch. Let M |= S + ConT. Let f be any M-definable function
in M2. Let ξ(x) be a Σ1 formula as in Theorem 5.1, and let X be the set
{ξ(m)f(m) : m ∈M}.
By Fact 2.40, M can be expanded to a model (M,A) |= WKL0. By
Fact 2.41, the compactness theorem is provable in WKL0. Reasoning
within (M,A), using the fact that f (and therefore X) is M-definable,
carry out the same compactness argument as in the proof of Theorem 4.5,
to establish (M,A) |= ConT+X . Since WKL0 is a conservative extension
of IΣ1, the arithmetised completeness theorem (as stated in Fact 2.38) can
now be used to construct an end-extension satisfying T +X .¹⁰
5.2 Formalisation of the GRMMKV theorem
The proof of the Gödel-Rosser-Mostowski-Myhill-Kripke-Visser theorem
can also be formalised within IΣ1 to show the existence of analogous end-
extensions.
Theorem5.4 (Blanck, 2016). Suppose that {Ti : i ∈ ω} is an r.e. family of
consistent, r.e. theories such that I∆0 + exp ` ∀i∀x(PrQ(x) → PrTi(x)),
and that {Xi : i ∈ ω} is an r.e. family of r.e. sets such that I∆0 + exp `
∀i∀ξ ∈ Xi(ConTi → ConTi+¬ξ). For each n > 0, there is then a Σn
formula γ(x) such that for each σ(x) ∈ Σn, each i ∈ ω and each ξ ∈ Xi,
⁹Hamkins’s result is stated for extensions S of PA, with T = S.
¹⁰This argument is, modulo minor differences, independently due to Ali Enayat.
60
formalisation and end-extensions
1. if M |= IΣ1 + ∀iConTi , then M |= ∀x¬γ(x);
2. every model of IΣ1 + ∀iConTi can be end-extended to a model of
Ti + ∀x(γ(x) ↔ σ(x)) + ¬ξ.
The method is similar to the one used in proving Lemma 5.2.
Lemma 5.5 (Blanck, 2016). Suppose that {Ti : i ∈ ω} is an r.e. family of
consistent, r.e. theories such that I∆0 + exp ` ∀x∀i(PrQ(x) → PrTi(x)),
and that {Xi : i ∈ ω} is an r.e. family of r.e. sets such that I∆0 + exp `
∀i∀ξ ∈ Xi(ConTi → ConTi+¬ξ). For each n > 0, there is then a Σn
formula γ(x) such that for each σ(x) ∈ Σn,
1. I∆0 + exp ` ∀i∀ξ ∈ Xi∀z
(
ConTi+¬ξ → ¬R(e, e, i, ξ, z)
)
2. I∆0 + exp ` ∀i∀ξ ∈ Xi∀z
(
ConTi+¬ξ → ConTi+R(e,e,i,ξ,z)+¬ξ
)
.
Proof. Let the Ti’s and Xi’s be as in the statement of the lemma. Let
φ(x, u, y, z) be the formula PrTu(pR(x˙, x˙, u˙, y˙, z˙) → y˙q), and let e =
pφq. To lighten the notation, assume that every formula below is prefixed
with ∀i∀ξ ∈ Xi. By definition of R,
I∆0 + exp ` ∀z
(
R(e, e, i, ξ, z) → φ(e, i, ξ, z)
)
(5.13)
so by construction of φ,
I∆0 + exp ` ∀z
(
R(e, e, i, ξ, z) → PrTi(pR(e, e, i, ξ, z˙) → ξq)
)
.
(5.14)
By provable Σ1-completeness of Q,
I∆0 + exp ` ∀z
(
R(e, e, i, ξ, z) → PrTi(pR(e, e, i, ξ, z˙)q)
)
, (5.15)
which together with (5.14) and the derivability conditions give
I∆0 + exp ` ∀z
(
R(e, e, i, ξ, z) → PrTi(pξq)
)
, (5.16)
whence
I∆0 + exp ` ∀z
(
ConTi+¬ξ → ¬R(e, e, i, ξ, z)
)
. (5.17)
61
contributions to the metamathematics of arithmetic
For the latter part, recall that by definition of φ,
I∆0 + exp ` ∃zPrTi(pR(e, e, i, ξ, z˙) → ξq) → ∃zφ(e, i, ξ, z), (5.18)
so by the properties of the partial satisfaction predicate,
I∆0 + exp ` ∃zPrTi(pR(e, e, i, ξ, z˙) → ξq) → ∃zSatΣ1(e, e, i, ξ, z),
(5.19)
and by assumption on R, working in I∆0 + exp,
I∆0 + exp ` ∃zPrTi(pR(e, e, i, ξ, z˙) → ξq) → ∃zR(e, e, i, ξ, z).
(5.20)
But then by (5.16) and (5.20),
I∆0 + exp ` ∃zPrTi(pR(e, e, i, ξ, z˙) → ξq) → PrTi(pξq), (5.21)
so it follows that
I∆0 + exp ` ∀z
(
ConTi+¬ξ → ConTi+R(e,e,i,ξ,z)+¬ξ
)
.
Proof of Theorem 5.4. Let the Ti’s and Xi’s be as in the statement of the
theorem, and let M |= IΣ1 + ∀iConTi . Then
M |= IΣ1 + ∀i∀ξ ∈ XiConTi+¬ξ
by assumption. Let e be as in Lemma 5.5, and let
γ(x) := ∃u∃y∃z
(
R(e, e, u, y, z) ∧ SatΣn(z, x)
)
.
(1) By Lemma 5.5(1), M |= ∀i∀ξ ∈ Xi∀z¬R(e, e, i, ξ, z). Hence
M |= ∀x¬γ(x).
(2) Pick j ∈ ω, ξ ∈ Xj , and σ(x) ∈ Σn. By Lemma 5.5(2), it follows
that M |= ConTj+R(e,e,j,pξq,pσq)+¬ξ, and since M |= IΣ1, the arithmet-
ised completeness theorem (Fact 2.38) provides an end-extension K of M
such that
K |= Tj +R(e, e, j, pξq, pσq) + ¬ξ.
By a reasoning similar to the one in the proof of Theorem 5.1, the model
is as desired.
62
formalisation and end-extensions
It may seem too strong an assumption that the model M satisfies the
consistency of all Ti’s in the r.e. family of theories. Similar reservations may
be made for the other internal quantification on i and ξ. This, however, is
required to ensure that γ(x) behaves in the intended way. A more useful
formulation would perhaps be along the lines that ‘ifM satisfies ConTi for
a particular choice of i, then there is a suitable end-extension’. This can be
accomplished by constructing a parametrised version γ(x, i, pξq).
Theorem 5.6. Suppose that {Ti : i ∈ ω} is an r.e. family of consistent, r.e.
theories extending Q. Suppose further that Xi is an r.e. family of r.e. sets
such that for any choice of i ∈ ω and ξ ∈ Xi, Ti 0 ξ.
Then there is a Σn formula γ(x, y, z) such that for each σ(x) ∈ Σn,
each i ∈ ω and each ξ ∈ Xi,
1. if M |= IΣ1 + ConTi+¬ξ, then M |= ∀x¬γ(x, i, pξq);
2. every model of IΣ1 +ConTi+¬ξ can be end-extended to a model of
Ti + ∀x(γ(x, i, pξq) ↔ σ(x)) + ¬ξ.
The proof can be obtained by an easy modification of the proofs of
Lemma 5.5 and Theorem 5.4.
5.3 Hierarchical generalisations
As in the case with Kripke’s theorem, there are also hierarchical generalisa-
tions of the formalisation results above. Here, a method is sketched for
converting the proofs of Theorem 5.1 and Lemma 5.2 to yield one such
generalisation.
Recall that PrT,Σn+1(x) is the Σn+1 formula
∃z(Σn+1(z) ∧ TrΣn+1(z) ∧ PrT(pz˙ → x˙q)),
and that ConT,Σn+1 is the Πn+1 formula ¬PrT,Σn+1(⊥). Moreover, re-
call that the Σn+1 formulaRn(x, y, z) is defined as Sel{SatΣn+1}(x, y, z).
Hence z is functionally dependent on x and y in IΣn+1.
Let φ(x, z) be the Σn+1 formula PrT,Σn+1(p¬Rn(x˙, x˙, z˙)q) and let
e = pφq. Let γ(x) be the Σn+1 formula ∃z(Rn(e, e, z)∧SatΣn+1(z, x)).
63
contributions to the metamathematics of arithmetic
Examine the proofs of Theorem 5.1 and Lemma 5.2 and replace all occur-
rences of PrT, ConT, R and SatΣ1 with PrT,Σn+1 , ConT,Σn+1 , Rn and
SatΣn+1 , respectively. The resulting proofs yield:
Lemma 5.7. Let n > 0. If T is a Σn+1-definable, consistent extension of
Q, then there is a Σn+1 formula with Gödel number e, such that:
1. IΣn ` ∀z(ConT,Σn+1 → ¬Rn(e, e, z));
2. IΣn ` ∀z(ConT,Σn+1 ↔ ConT,Σn+1+Rn(e,e,z)).
Theorem 5.8. Let n > 0. Suppose that S is a consistent, r.e. extension of
IΣn+1, and that T is a Σn+1-definable, consistent extension of Q. There
is a Σn+1 formula γ(x) such that:
1. S ` ConT,Σn+1 → ∀x¬γ(x);
2. if σ(x) ∈ Σn+1, then every model M of S + ConT,Σn+1 has a
Σn-elementary extension to a model of T + ∀x(γ(x) ↔ σ(x)).
Remark 5.9. That K is a Σn-elementary extension of M follows from the
fact that if K |= ThΣn+1(M) (as is the case above), then it must also be
the case that K |= ThΣn(M) ∪ ThΠn(M). Hence there is no room for
changing the truth-value of any Σn formula when passing to the extension.
IΣn+1 is used to ensure the existence of the desired extension, while IΣn
suffices to show that z in the Σn+1 formula Rn(x, y, z) is functionally
dependent on x and y, hence unique.
64
6 Characterisations of partial conservativity
The previous chapter establishes the existence of certain kinds of end-exten-
sions related to the concepts of flexibility and independence. As is known
since the late 1970s, end-extensions play an important role in characterisa-
tions of interpretability and partial conservativity, both of which are useful
tools in measuring and comparing the strength of theories. An illuminating
passage is found in the introductory chapter of Hájek and Pudlák (1993).
[W]hat more can we say about systems of arithmetic than
that they are all incomplete? There are at least four directions
in which the answer may be looked for:
(1) For each formula φ unprovable and non-refutable in an
arithmetic T we may ask, how conservative it is over T,
i.e. for which formulas ψ the provability of ψ in (T+φ)
implies the provability of ψ in T.
(2) We may further ask if (T + φ) is interpretable in T, i.e.
whether the notions of T may be redefined in T in such
a way that for the new notions all axioms of (T+φ) are
provable in T.
(3) Given T we may look for various natural sentences true
but unprovable in T (for example, various combinatorial
principles).
(4) Moreover, we may investigate models of T and look at
how they visualize our syntactic notions and features.
(Hájek and Pudlák, 1993, p. 3)
This chapter elaborates on the interesting relationship between these four
directions, especially concerning (1), (2), and (4). In particular, character-
isations of partial conservativity are given over non-r.e. theories, weak (es-
pecially non-reflexive) theories of arithmetic, and theories formulated in
65
contributions to the metamathematics of arithmetic
an extended language. Each of these relaxations gives rise to their own dif-
ficulties. Some of the characterisations are necessary prerequisites for the
results in Chapter 7.
6.1 The Orey-Hájek characterisation and its extensions
One of the cornerstones in the early study of the metamathematics of
formal arithmetic is the Orey-Hájek characterisation of interpretability.
Theorem 6.1. Let T and S be consistent, r.e. extensions of PA in the same
language. The following are equivalent:
1. S is interpretable in T;
2. S|k is interpretable in T for all k ∈ ω;
3. T ` ConS|k for all k ∈ ω.
The equivalence of (1) and (2) is due to Orey (1961): it is also known as
Orey’s compactness theorem. The equivalence of (1) and (3) is,
implicit in Feferman (1960), all but explicit in Orey (1961),
and fully explicit in Hájek (1971). (Lindström, 2003, p. 115)
By the independent work of Guaspari (1979) and Lindström (1979) it is
possible to include a fourth equivalent condition:
4. S is Π1-conservative over T.
It is well known that the success of the Orey-Hájek characterisation, as
presented above, depends on certain features of the theories S and T. Of
particular interest are reflection properties, sequentiality and whether or not
the theories prove the totality of the exponentiation function. For finitely
axiomatised theories, interpretability and Π1-conservativity no longer co-
incide (Pudlák, 1985; Hájek, 1987; Visser, 1990; Shavrukov, 1997; Joosten,
2004).
The following theorem is a general characterisation for r.e. theories ex-
tending PA, and it is used repeatedly throughout Chapter 7, referred to
66
characterisations of partial conservativity
as the OHGL characterisation. The equivalence of (1) and (4) is due to
Guaspari (1979), who writes that ‘[This method] for constructing end-
extensions seems to be well known’. The condition (3) is rarely (if ever)
included in these characterisations, but is almost definitionally equivalent
to condition (4). It is also a convenient condition to work with.
Theorem 6.2 (The Orey-Hájek-Guaspari-Lindström characterisation).
Suppose that T and S are consistent, r.e. extensions of PA in the same
language. Then the following are equivalent:
1. every model of T can be end-extended to a model of S;
2. every countable model of T can be end-extended a model of S;
3. for every model M of T, the theory ThΣ1(M) + S is consistent;
4. S is Π1-conservative over T;
5. T ` ConS|k for all k ∈ ω;
6. S is interpretable in T.
By putting together a number of observations of Guaspari (1979), it
is possible to state a hierarchical version of the above. To formulate this
version, Guaspari’s concept of provably Γ-faithful interpretations is con-
venient. Let t be an interpretation of S in T: then t is provably Γ-faithful
if, for every φ ∈ Γ, T ` t(pφq) → φ.
Theorem 6.3. Suppose that T and S are consistent, r.e. extensions of PA
in the same language. Then the following are equivalent:
1. every model of T has a Σn-elementary extension to a model of S;
2. every countable model of T has a Σn-elementary extension to a
model of S;
3. for every model M of T, the theory ThΣn+1(M) + S is consistent;
4. S is Πn+1-conservative over T;
5. T ` Con(S,Σn+1)|k for all k ∈ ω;
6. there is a provably Πn+1-faithful interpretation of S in T.
67
contributions to the metamathematics of arithmetic
6.2 A characterisation of partial conservativity over IΣ1
As suggested in the previous section, the OHGL characterisation (and even
the Orey-Hájek characterisation) breaks down when passing to weaker the-
ories of arithmetic, e.g., extensions of IΣ1. One reason is that whenever
T is finitely axiomatisable, it is impossible to have T ` ConT|k for all
k ∈ ω. Another reason is that, as noted above, interpretability and Π1-
conservativity no longer coincide. It is a major open problem whether
every model of IΣ1 has a proper end-extension to a model of IΣ1. Even
so, Fact 2.35 assures that every countable model of IΣ1 is isomorphic to a
proper initial segment of itself. This makes it possible to salvage parts of
the characterisation of partial conservativity for extensions of IΣ1.
Theorem 6.4 (Blanck and Enayat, 2017). Suppose that T and S are con-
sistent, r.e. extensions of IΣ1 in the same language. Then the following are
equivalent:
1. every countable model of T can be end-extended to a model of S;
2. for every model M of T, the theory S + ThΣ1(M) is consistent;
3. S is Π1-conservative over T;
4. for each n ∈ ω, T ` ConnS,Σ1 .
Proof. (1) ⇒ (2). Prove the contrapositive by supposing that (2) fails.
There is then a countable model M |= T such that ThΣ1(M) + S is
inconsistent. Hence there is a σ ∈ ThΣ1(M) such that S + σ ` ⊥. Since
Σ1 sentences are preserved when passing to an end-extension, this shows
that every end-extension ofMmust fail to satisfy S, which makes it evident
that (1) fails.
(2) ⇒ (3). Prove the contrapositive by supposing that (3) fails. There
is then a pi ∈ Π1 such that S ` pi and T + ¬pi is consistent. By the
completeness theorem, there is some model M |= T + ¬pi. But since
¬pi ∈ ThΣ1(M) and S ` pi, (2) must fail.
(3) ⇒ (4). Suppose (3), and let n ∈ ω. By small reflection (Fact 2.25),
S ` ConnS,Σ1 . Con
n
S,Σ1 is a Π1 sentence, and S is Π1-conservative over T,
so T ` ConnS,Σ1 .
68
characterisations of partial conservativity
(4) ⇒ (1). Suppose (4), and let M be a countable model of T. Assume,
without loss of generality, that M is non-standard. By (4),
∀n ∈ ωM |= ConnS,Σ1 ,
and since M |= IΣ1, M satisfies the overspill principle for Π1 formulae,
whence
M |= ConmS,Σ1
for some non-standardm ∈M . By McAloon’s theorem (Fact 2.39), there
is a submodel M0 |= PA that forms a non-standard initial segment of M,
all of whose elements are below m.
There is some a ∈ M that codes the set {n ∈ ω : M |= TrΣ1(n)} =
ThΣ1(M), i.e. the standard part of TrueΣ1(M), and this a can be chosen
to be below m. In other words, M |= ∀x(xεa → TrΣ1(x)), which
together with a < m ensures that
M0 |= ConS+{n:nεa}.
SinceM0 |= PA, the arithmetised completeness theorem (Fact 2.38) guar-
antees the existence of an end-extensionN ofM0 satisfying S+{n : nεa},
and therefore S+ThΣ1(M). SinceM0 ⊆e M, andM0 ⊆e N , it follows
that SSy(M) = SSy(M0) = SSy(N ). This, together with the fact that
N |= ThΣ1(M) allows Fact 2.35 to embed M as an initial segment of
N .
Remark 6.5. The equivalence of (3) and (4) seems to have been known to
experts for some time: for example, it figures in an unpublished note from
the early 1990s, due to Albert Visser. The same note contains a proof of
what is essentially Fact 2.25. Similar results also appear in Joosten (2004,
Chapter 2). The fact that (2) implies (1) follows, for extensions of PA, from
Theorem 2 of Woodin (2011). That (2) and (3) are related is easy to see,
and as the proof above suggests, the real difficulty lies in establishing that
(4) implies (1).
The proof of the theorem above lends itself to prove a hierarchical gener-
alisation. The equivalence of (1) and (3) for extensions of PA follows from
Theorem 6.5(i) of Guaspari (1979).
69
contributions to the metamathematics of arithmetic
Theorem 6.6 (Blanck and Enayat, 2017). Let T be a consistent, r.e. exten-
sion of IΣn+1 in the same language. Then the following are equivalent:
1. every countable model of T has a Σn-elementary extension to a
model of S;
2. for every model M of T, the theory S + ThΣn+1(M) is consistent.
3. S is Πn+1-conservative over T;
4. for each k ∈ ω, T ` ConkS,Σn+1 .
6.3 Language extensions
This section concerns rather specific improvements of Theorems 6.2 and
6.4 that are needed in the proofs of some of the results in Chapter 7. The
first such improvement is essentially due to Guaspari: the equivalence of
the new condition (3) with the others is immediate.
Theorem 6.7 (Guaspari, 1979, Theorem 6.5(i)). Let T be a consistent, r.e.
extension of PA formulated in a finite language L ⊇ LA. Then the
following are equivalent for anL -sentence φ:
1. every model of T can be end-extended to a model of T + φ;
2. every countable model of T can be end-extended to a model of T+φ;
3. for each model M of T, the theory T + ThΣ1(L )(M) + φ is con-
sistent;
4. T + φ is Π1(L )-conservative over T.
The next theorem is a new generalisation of Theorem 6.4 to extensions
of IΣ1 formulated in an extended language L (c) = LA ∪ {c}, where c
is a single new individual constant. Recall that if T is a theory formulated
in L (c) and T ` IΣn, then T ` IΣn(c). This generalisation, Theorem
6.8, is a refinement of Theorem 2 of Woodin (2011), which establishes the
implication (2) ⇒ (1) for theories extending PA. It is also exactly what is
used to prove the main theorem of Section 7.1.
70
characterisations of partial conservativity
Theorem 6.8 (Blanck and Enayat, 2017). Let T be a consistent, r.e. exten-
sion of IΣ1 formulated in a language L (c) = LA ∪ {c}. The following
are equivalent for anL (c)-sentence φ(c):
1. every countable model of T can be end-extended to a model of T +
φ(c);
2. for every model (M, s) of T, the theory T+φ(c)+ThΣ1(c)(M, s)
is consistent;
3. T + φ(c) is Π1(c)-conservative over T;
4. for each n ∈ ω, T ` ConnT,Σ1(c)+φ(c).
Proof. The proof is similar to the proof of Theorem 6.4, but some extra
bookkeeping is required because of the expanded language.
(1) ⇒ (2). Suppose that (2) fails. By the completeness theorem, and
the Löwenheim-Skolem theorem, there is a countable model (M, s) |= T
such that T + φ(c) + ThΣ1(c)(M, s) is inconsistent; it then follows that
T + ThΣ1(c) ` ¬φ(c). Suppose that (N , t) is an LA(c)-structure end-
extending (M, s), and that (N , t) |= φ(c). It follows that s = t, and
since Σ1(c) sentences are preserved when passing to (N , t), this shows
that (N , t) |= φ(c) ∧ ¬φ(c), which in turn makes it evident that (1) fails.
(2) ⇒ (3). Suppose that (3) fails. There is then a Π1(c) sentence pi
such that T + φ(c) ` pi and T + ¬pi is consistent. Let (M, s) be a
model of T +¬pi. Then T + φ(c) + ThΣ1(c)(M, s) is inconsistent, since
T + ¬pi ` ¬φ(c) and ¬pi ∈ Σ1(c).
(3) ⇒ (4). Suppose that (3) holds, and pick any n ∈ ω. Then by small
reflection, T + φ(c) ` ConnT,Σ1(c)+φ(c), and since Con
n
T,Σ1(c)+φ(c) is a
Π1(c) sentence, the conclusion follows from the Π1(c)-conservativity of
φ(c) over T.
(4) ⇒ (1). Suppose that (4) holds, and let (M, s) be any countable
model of T. Since (M, s) |= IΣ1, it follows that (M, s) |= IΣ1(c).
Therefore the model satisfies Π1(c)-overspill, so it follows that
(M, s) |= ConmT,Σ1(c)+φ(c)
for some non-standard m ∈M .
71
contributions to the metamathematics of arithmetic
By reasoning as in the proof of the corresponding clause of Theorem 6.4,
there is an initial submodel M0 |= PA of (M, s), all of whose elements
are below m, and an a < m that codes ThΣ1(c)(M, s).
Hence M0 |= PA + ConS+{n:nεa}, and Fact 2.38 gives rise to an end-
extension N of M0 such that (N , t) satisfies S + {n : nεa}. Since
SSy(M) = SSy(M0) = SSy(N ), and ThΣ1(c)(M, s) is contained in
the set coded by a, Fact 2.35 assures the existence of an embedding f of
(M, s) onto an initial segment of (N , t), with f(s) = t.
This theorem can also be generalised in the spirit of Theorem 6.6, and
again the equivalence of (1) and (3) for extensions of PA is due to Guaspari
(1979). His proof yields the additional information that if T extends PA
the assumption that M is countable can be removed, as in Theorem 6.7.
Theorem 6.9 (Blanck and Enayat, 2017). Let T be a consistent, r.e. ex-
tension of IΣn+1 formulated in the language L (c) = LA ∪ {c}. The
following are equivalent for anLA(c)-sentence φ(c):
1. every countable model of T has a Σn(c)-elementary extension to a
model of T + φ(c);
2. for every model (M, s) of T, the theory T+φ(c)+ThΣn+1(c)(M, s)
is consistent;
3. T + φ(c) is Πn+1(c)-conservative over T;
4. for each k ∈ ω, T ` ConkT,Σn+1(c)+φ(c).
6.4 Theories that are not recursively enumerable
On the one hand, many theories featuring in the metatheory of first-order
arithmetic are recursively enumerable (and therefore axiomatisable by a
primitive recursive set of axioms, by Craig’s trick). It is sometimes taken as
a minimal requirement for something to be a theory: that it must be pos-
sible to check whether or not a statement is an axiom of the theory. On the
other hand, in the study of models of arithmetic, non-r.e. sets of sentences
feature regularly, e.g., ThΠ1(M) for some model of arithmetic M.
72
characterisations of partial conservativity
As noted by Guaspari (1979), the assumption that a theory is r.e. can
be substituted by the assumption that the set of theorems of the theory is
coded in the model. The theorem below provides a characterisation of par-
tial conservativity for non-r.e. theories along the lines of the earlier results.
Although this theorem is essentially well known (it can be extracted from
Guaspari (1979), except for condition (2)), it is included here for sake of
completeness, and because it is used at one point in Section 7.3.
Definition 6.10. T proves the local consistency of S if, for each finite
subset F of S, T ` ConF .¹¹
Theorem 6.11. Suppose that T and S are consistent extensions of PA in
the same language. Then the following are equivalent:
1. for each M |= T, if S ∈ SSy(M), then M can be end-extended to
a model of S;
2. for every model M of T, the theory ThΣ1(M) + S is consistent;
3. S is Π1-conservative over T;
4. T proves the local consistency of S.
Proof. (1) ⇒ (2). Suppose that (2) fails, i.e. that there is a model M |= T
such that ThΣ1(M) + S is inconsistent. Hence there is a σ ∈ ThΣ1(M)
such that S + σ ` ⊥. Since Σ1 sentences are preserved when passing to
an end-extension, this shows that every end-extension of M must fail to
satisfy S, making it evident that (1) fails.
(2) ⇒ (3). Suppose (3) fails, i.e. that there is a pi ∈ Π1 such that S ` pi
and T + ¬pi is consistent. By the completeness theorem, there is a model
M |= T + ¬pi. Since ¬pi ∈ ThΣ1(M) and S ` pi, it follows that (2) fails.
(3) ⇒ (4). Suppose that S is Π1-conservative over T, and let F be any
finite subtheory of S. Since S is essentially reflexive, S ` ConF . But
ConF ∈ Π1 since F is finite, so T ` ConF .
(4) ⇒ (1). Suppose that T proves the local consistency of S, and let M
be a model of T such that S ∈ SSy(M).
¹¹In Guaspari (1979) the terminology is ‘S is strongly consistent with T’.
73
contributions to the metamathematics of arithmetic
Assume that s is a code for S in M, and let φ(x, y) be a Π1 formula
expressing ‘the first x elements of y are consistent’. Then M |= φ(n, s)
for all n ∈ ω. For suppose M |= ¬φ(n, s) for some n ∈ ω. Then there is
a finite subtheory F of S such that M |= ¬ConF . But T proves the local
consistency of S, and M |= T, a contradiction.
By the overspill principle, there is an m ∈M such that M |= φ(m, s).
The existence of the desired end-extension now follows from Fact 2.38.
74
7 Uniformly flexible formulae and Solovay
functions
Chapter 5 establishes the existence of a formula γ(x) ∈ Σn, such that for
every σ(x) ∈ Σn, every model M of T + ConT can be end-extended to a
model of T+ ∀x(γ(x) ↔ σ(x)). The question now arises of whether the
assumption that M satisfies ConT can be removed from this, and other,
results of Chapter 5. To see the relevance of this question, recall Gödel’s
second incompleteness theorem.
Theorem 7.1 (Gödel, 1931). Let T be a consistent, r.e. extension of I∆0+
exp. Then T + ¬ConT is consistent.
As argued in the introduction to Chapter 4, the existence of independ-
ent formulae (and therefore also of flexible formulae) strengthens the first
incompleteness theorem. Another way to improve the incompleteness the-
orem is to claim that T + ¬ConT is not only consistent, but also inter-
pretable in T. That this is indeed the case is the essence of Feferman’s
theorem on the interpretability of inconsistency.
Theorem 7.2 (Feferman, 1960). Let T be a consistent, r.e. extension of
I∆0 + exp. Then T + ¬ConT is interpretable in T.
In light of the OHGL characterisation (Theorem 6.2), this is equivalent
to every model of T having an end-extension to a model of T + ¬ConT.
Turning attention back to flexibility, it would be desirable to see a similar
improvement of Kripke’s theorem 4.3. Simply put, the question is:
Question 7.3. Is there, for any n > 0, a Σn formula γ(x) such that for
every σ(x) ∈ Σn, T + ∀x(γ(x) ↔ σ(x)) is interpretable in T?
Indeed, if the assumption that M |= ConT could be removed from
the formalisation of Kripke’s theorem, the question would have a positive
75
contributions to the metamathematics of arithmetic
answer. The existence of such a uniformly flexible formula γ(x) would then
yield not only an improvement of the first incompleteness theorem, but
also of the second, in the spirit of Feferman.
There are reasons to treat a number of special cases of this general prob-
lem separately. A somewhat recent result due to Woodin (2011) gives an
important uniform flexibility result for formulae with bounded extensions.
This result in conjunction with the formalisation of Kripke’s theorem in
Chapter 5 is what suggests the general question above. Woodin employs
a Solovay function for his proof – a versatile technique introduced by So-
lovay (1976). Section 7.1 gives an introduction to the method by reproving
Woodin’s theorem, and also by giving some important generalisations.
In Section 7.3, an affirmative answer to the question is given for n > 1,
while the trickier special case n = 1 is treated in Section 7.4. There, only
partial results are given. Finally, hierarchical generalisations are discussed
in Section 7.5.
7.1 Woodin’s theorem and its extensions
In Woodin (2011), the following theorem is established.
Theorem 7.4. Suppose that T is a consistent, r.e. extension of PA. There
is an r.e. set We such that:
1. PA ` ConT →We = ∅;
2. for each countable model M |= T, if s is an M-finite set such that
M |= We ⊆ s, then there is an end-extension of M satisfying
T +We = s.¹²
In Woodin’s paper, the purpose of the theorem is to drive a philosophical
argument about the distinction between determinism and nondetermin-
ism, an aspect not discussed in this thesis. Rather, the reason for including
¹²Strictly speaking, the expression We = ∅ is not a sentence in LA. Using the coding
machinery outlined in Chapter 2, it is possible to take this notation as shorthand for the
Π1 sentence ∀y∀z¬R(e, y, z), and the informal reading of this is ‘the Turing machine
with index e never produces any output’. Similarly, expressions like We = s can be
understood as shorthand for ∀y∀z(R(e, y, z) ↔ zεc), where c is a new constant
symbol. These considerations also apply to similar expressions in the sequel.
76
uniformly flexible formulae and solovay functions
Woodin’s result here is its relation to the question proposed in the introduc-
tion to this chapter, and its relation to flexible and independent formulae.
The following paragraphs expound on these connections.
First, recall that there is a straightforward connection between r.e. sets
Wn, and Σ1 formulae, in that every r.e. set can be numerated (in an ex-
tension of Q) by a Σ1 formula. Conversely, every set numerated in an
r.e. extension of Q is r.e. Given certain assumptions on the enumeration
of the r.e. sets and their representation within arithmetic, it is possible to
arrange so that the formula φ(x) with Gödel number pφq numerates the
r.e. set W
pφq. Such a correspondence can be arranged to be verifiable in
I∆0 + exp, and We can therefore be viewed as a Σ1 formula γ(x).¹³
Secondly, an M-finite set is one that is bounded within M, i.e. a setX
such that for all x ∈ X , M |= x ≤ m for some m ∈ M . In particular,
if M |= IΣn, then every set of the form {n ∈ ω : M |= σ(n)} for
σ(x) ∈ Σn is M-finite.
Moreover, the assumption that M |= We ⊆ s is necessary since Σ1
sentences persist when passing to an end-extension: ifM |= σ for σ ∈ Σ1,
andM⊆e N , thenN |= σ. Since n ∈We is expressible by a Σ1 formula,
We can never shrink when passing to an end-extension, only grow. For
instance, suppose that M |= We = {k} and M |= s = {n}, with k 6= n.
Then there can be no end-extension ofM in whichWe = s, since thenWe
would have to have ‘lost’ the element k in order to have the same extension
as s, and this is not possible.
Taken together these observations suggests that Woodin’s theorem can
be regarded as a generalisation of Mostowski’s theorem 4.5, rather than as a
generalisation of Kripke’s theorem 4.3. This is because Theorem 7.4 allows
for the construction of an end-extension N in which We has a previously
prescribed extension (i.e. one chosen from the finite sets ofM), rather than
an extension which is identical to that of some Σ1 formula σ(x), whatever
extension σ(x) may happen to have in N .
Following the publication of Woodin (2011), Ali Enayat and Volodya
Shavrukov (in unpublished manuscripts) improved Woodin’s theorem by
removing the countability assumption on the base model M.
¹³Cf. Fact 2.52 and the subsequent discussion.
77
contributions to the metamathematics of arithmetic
Theorem 7.5 (Woodin/Enayat and Shavrukov). Suppose that T is a con-
sistent, r.e. extension of PA. There is an r.e. set We, such that:
1. PA ` ConT →We = ∅;
2. for each model M |= T, if s is an M-finite set such that M |=
We ⊆ s, then there is an end-extension ofM satisfying T+We = s.
The Enayat-Shavrukov proof applies only to reflexive theories, e.g. the-
ories extending PA. It is also possible to derive the theorem directly from
Theorem 7.4, by using the strength of Theorem 6.7. However, for finitely
axiomatised theories such as IΣ1, more is needed to establish a similar result.
This is indeed possible by using methods inspired by the characterisation
of the modal logic of Π1-conservativity over extensions of IΣ1 (Hájek and
Montagna, 1990; Japaridze, 1994), thus establishing:
Theorem 7.6 (Blanck and Enayat, 2017). Suppose that T is a consistent,
r.e. extension of IΣ1. There is an r.e. set We, such that:
1. IΣ1 ` ConT →We = ∅;
2. for each countable model M |= T, if s is an M-finite set such that
M |= We ⊆ s, then there is an end-extension of M satisfying
T +We = s.
The three theorems above are derived, using the characterisations of par-
tial conservativity in Chapter 6, from the following lemma, which is an
adaptation of the construction used by Shavrukov in the original proof
of Theorem 7.5. The proof method for establishing these results differs
from the method used in Chapter 5, in that the set We is not obtained
by means of a partial satisfaction predicate, but rather constructed as a so
called Solovay function. The intellectual heritage of the construction below
goes from Solovay (1976), via Japaridze (1994), Woodin (2011), and the
Enayat-Shavrukov manuscripts, to Blanck and Enayat (2017). The present
concoction is inspired by all of these works.
Lemma 7.7. Suppose that T is a consistent, r.e. extension of IΣ1 in the
same language. There is an r.e. set We, such that:
78
uniformly flexible formulae and solovay functions
1. IΣ1 ` ConT →We = ∅;
2. for each k ∈ ω, T ` ∀ finite set s(We ⊆ s→ ConkT,Σ1+We=s).
Proof. The set We is defined in IΣ1, using the recursion theorem, by the
stagesWe,x in which it acquires its elements. An auxiliary function r(x) is
simultaneously defined.
Stage 0: Set We,0 = ∅, and r(0) = ∞.¹⁴
Stage x+ 1: Suppose r(x) = m. There are two cases:
Case A: s ⊇ We,x, n < m, and x witnesses a Σ1 sentence
σ(s) such that n is a proof in T of ∀t(σ(t) → We 6= t).
Then set We,x+1 = s and r(x+ 1) = n;
Case B: otherwise, set We,x+1 = We,x and r(x+ 1) = m.
Let We =
⋃
xWe,x.
Provably in IΣ1, We,x+1 ⊇ We,x, and r(x + 1) ≤ r(x). That a limit
R = limx r(x) exists is shown by repeating an argument due to Beklem-
ishev and Visser (2005). Reason in IΣ1:
By the Σ1-least number principle, let R be such that
∃x(r(x) = R)) ∧ ∀y<R¬∃x(r(x) = y)
i.e., R is the least value attained by r; then ∀x(r(x) ≥ R).
If m is such that r(m) = R, then ∀x≥m(R ≥ r(x)) since
∀x(r(x) ≥ r(x+1)). It follows that ∀x≥m(r(x) = R), so
the limit of r exists.
For each x with We,x+1 6= We,x, IΣ1 proves r(x + 1) < r(x), whence
there are only finitely many such x. So IΣ1 ` “We is finite”.
Note that for each k ∈ ω, T ` R > k. Fix k ∈ ω and argue in T:
Suppose R ≤ k. Let y be minimal such that r(y + 1) = R.
ThenWe = We,y+1 = s for some s such that R is a proof of
∀t(σ(t) →We 6= t), where σ(s) is a true Σ1 sentence.
¹⁴Here, and in what follows,∞ is a fictitious number greater than all the natural numbers.
It is possible to replace∞ with an ordinary number, at the cost of making the definition
of We and r(x) less transparent.
79
contributions to the metamathematics of arithmetic
But, by small reflection (Fact 2.25),
since We 6= s is proved from a true Σ1 sentence with a T-proof
not exceeding k, it must be true. The contradiction provesR > k.
To prove (1), argue for the contrapositive statement in IΣ1:
If We = s 6= ∅, then PrnT(p∀t(σ(t) →We 6= t)q) for some n.
Since We is finite, s ⊆ We is Σ1. Then PrT(ps ⊆ Weq) follows
by formalised Σ1-completeness. Now reason inside PrT:
There is u = We with u ⊇ s, so by construction, σ(u) is
true, and PrmT (p∀t(σ(t) →We 6= t)q) for some m ≤ n.
Using formalised small reflection, continue reasoning inside PrT:
Then ∀t(σ(t) →We 6= t) and σ(u), so We 6= u.
But then PrT(pWe = u ∧We 6= uq), so ¬ConT as desired.
To prove (2), first fix k ∈ ω. By small reflection, there is a proof n in T of
∀t(PrkT,Σ1(pWe 6= t˙q) →We 6= t).
Now reason in T:
Consider any finite s ⊇ We. Suppose x is a k-proof of We 6= s
in T+ThΣ1(N). Then s ⊇We,x+1, and therefore r(x+1) ≤ n
by construction of r(x + 1): here PrkT,Σ1(pWe 6= sq) is a true
sentence playing the role of σ(s). But n ≤ R < r(x + 1), and
the contradiction proves ConkT,Σ1+We=s.
With this lemma in place, it is easy to derive Theorems 7.4 through 7.6.
Proof of Theorems 7.4 and 7.6. Let T be a consistent, r.e. extension of IΣ1,
and let We be as in Lemma 7.7. Let M be a countable model of T, and
let s be an M-finite set such that M |= We ⊆ s.
By Lemma 7.7, for each k ∈ ω, T ` We ⊆ s → ConkT,Σ1+We=s. But
by Theorem 6.8 ((4)⇒ (1)), withM being countable, this implies thatM
can be end-extended to a model satisfying T +We = s.
Proof of Theorem 7.5. This follows directly from Theorem 7.4, by coupling
its conclusion with Theorem 6.7.
80
uniformly flexible formulae and solovay functions
7.2 Digression: On coding schemes
In fact, the theorem proved in Woodin (2011) is not phrased in terms of
r.e. sets, but rather in terms of Turing machines and finite binary sequences.
The correspondence between Turing machines, r.e. sets and Σ1-formulae
is easy to establish, but the translation between finite binary sequences and
finite sets in this setting require a few words on coding.
Theorem 7.8 (Woodin, 2011, Theorem 5). There exists e0 ∈ ω such that
for all countable modelsM |= PA, if s is the output of the Turing machine
with program e0 within M, and if t is an internal binary sequence of M
such that s is a proper initial segment of t, then there exists a countable
model N |= PA such that M is a proper initial segment of N and such
that t is the output of the Turing machine with program e0 within N .
This theorem can be derived from Theorem 7.4 in the following manner.
Fix a recursive function h : ω → <ω2 such that for every t ∈ <ω2 there
are infinitely many i such that h(i) = t. For the base case, suppose that n
is the first stage at which We is non-empty, and that We,n = s0 for some
finite set s0. Then the desired program e0 enumerates s0 in increasing order
as {ai : i < k} for k the size of s0 and outputs the sequence
f(s0) = h(a0)_ . . ._h(ak−1).
In general, if We,x+1 6= We,x, then e0 enumerates We,x+1 \We,x in in-
creasing order as {bj : j ≤ m} and replaces its previous output f(sx) by
f(sx+1) = f(sx)_u, where u = h(b0)_ . . ._h(bm−1).
Suppose that the output of e0 within M is s and let t be a proper, M-
finite prolongation of s. Then s = h(a0)_ . . ._h(ai) for some a0, . . . , ai
such that A = {a0, . . . , ai} = We within M. Let u be a sequence such
that s_u = t. By definition of h, there is an n ∈ ω such that n > ai
for all ai ∈ A and such that h(n) = u. By Theorem 7.4, there is an end-
extension N of M in which We = A ∪ {n}. But then the output of e0
within N is precisely s_u = t, as desired. This coding scheme can also be
applied to obtain sequence versions of Theorems 7.5 and 7.6.
To derive Theorem 7.4 from Theorem 7.8, first fix a recursive function
g : <ω2 → ω<ω. This g is required to have the additional property that
81
contributions to the metamathematics of arithmetic
for every t ∈ <ω2, and every s ∈ ω<ω, there is an u, properly extending t,
such that g(u) = s. For example, fix an enumeration 〈si, i ∈ ω〉 of ω<ω
in which every element occurs infinitely often, and for any t ∈ <ω2, let
g(t) = sn where n is the length of t. Now, define We in stages: if t0 is
the first output of e0, then set We,1 = g(t0), and generally, as soon as e0
generates a new output tx+1, then We,x+1 = g(tx) ∪ g(tx+1).
The paper Woodin (2011) also contains a notable philosophical inter-
pretation of (a corollary to the proof of ) Theorem 7.8. Although a thorough
treatment of Woodin’s philosophical argument is beyond the scope of this
thesis, there is reason to elaborate on the construction of the index e∗0 that
is used in his argument. Woodin writes:
Our construction of e0 actually gives rise to a Turing program
e∗0 that witnesses a more dramatic version of the property just
discussed. (Woodin, 2011, p. 120)
Even though Woodin formally, and informally, describes the behaviour of
this new program e∗0, there are no details on how to actually construct the
desired program, and that lacuna is bridged here.
Suppose that s is the output of Woodin’s program e0 within a model
M of PA. A central point of Woodin’s argumentation is that the piece of
information by which the sequence s is prolonged can be added as the one
and only new entry in an end-extension N , that is, in a single step. Let t be
a sequence to be added to the output of e0, i.e. such that s_t is the total
output of e0 in N .
If t can be added in a single step, then there can be no intermediate
end-extension K such that M ⊂e K ⊂e N , unless WKe0 (that is, We0
as calculated within K ) is equal to s or s_t. Otherwise, the program
e0 would have to have added t in two separate parts t1 and t2, such that
WKe0 = s
_t1 and WNe0 = s_t1_t2 = s_t, and this represent two steps,
as the terminology is used.
The point of the following coding scheme is to describe how a program
e∗0 can be constructed from the program e used in the proof of Theorem
7.5. Hence, this coding scheme treats the set-versions of Woodin’s theorem.
It is easy to see how a single-element extension of a set can be obtained in a
single step, but not as much so in the case of e.g. a two-element extension.
82
uniformly flexible formulae and solovay functions
Let C(n) be the non-empty finite set canonically coded by n + 1, e.g.
by writing n + 1 in base 2 and looking at the positions in which there is
a 1. Let e∗0 be the Turing machine program which, at any given stage of
computation, outputs C(a1)∪ · · · ∪C(an) if the output of e at the same
stage is {a1, . . . , an}.
Suppose that, in M, We∗0 = s for some M-finite set s, and that t is
an M-finite set properly extending s. By definition of e∗0, this means that
We = {a1, . . . , an} with M |= s = C(a1)∪ · · ·∪C(an). Let u = t\ s;
then u is an M-finite set. Choose m ∈ M such that M |= u = C(m).
Note that m /∈ s. There is then an end-extension N of M such that
We = {a1, . . . , an,m} as calculated in N , which in turn shows that
WNe∗0 = C(a1) ∪ · · · ∪ C(an) ∪ C(m) = t.
Hence the additional output u = C(m) is given in a single step.
The recently established fact that the Woodin-like theorems can be mod-
ified in such a way that any additional output can be added in a single
step has some repercussions on the structure of possible end-extensions ob-
tained by those theorems. For example, fix M and suppose WMe = s.
Let t = {m1,m2}, with m1,m2 ∈ M . By Theorem 7.5, there is an end-
extensionN1 ofM such thatWN1e = s∪{m1}, and an end-extensionN2
of M such that WN2e = s ∪ {m2}. Moreover, there is an end-extension
N1,2 ofM such thatWN1,2e = s∪{m1,m2}. If the additional outputs all
are given in a single step, then N1 6⊆e N1,2 and N2 6⊆e N1,2 even though
each of N1, N2 and N1,2 end-extends M.
Put in another way: if an element m is added to We at a stage k, then
it is only possible to add new elements to We at stages > k. Supposing
that M is such that the latest addition to We occurred at stage k, there
are end-extensionsN1 andN1,2 as above, both in which the latest addition
to We occurred at stage k + 1, but such that ‘the set which was added to
We at stage k + 1’ is {m1} in the first model and {m1,m2} in the latter.
Then, even if N1 is end-extended to a model N ′1 in which m2 is added to
We, so that WN
′
1e = WN1,2e , the Σ1-theory of any of these two models is
inconsistent with the theory of the other model.
83
contributions to the metamathematics of arithmetic
7.3 Uniformly flexible formulae
The purpose of this section is to establish the following:
Theorem 7.9. Suppose that T is a consistent, r.e. extension of PA. For
all n > 1, there is a Σn formula γ(x) such that for any σ(x) ∈ Σn,
T + ∀x(γ(x) ↔ σ(x)) is interpretable in T.
The proof combines Kripke’s trick from Chapter 4 with the Solovay func-
tions of Section 7.1, and can very roughly be outlined as follows. Modify
the set We of Theorem 7.6 so that it adds a single element every time it
grows. Then the desired formula γ(x) can be chosen as ‘x satisfies the
formula whose Gödel number is the latest addition to We’.
In more detail, the suggested modification amounts to turning We into
a Solovay function f(x), acquiring a new input-output pair when passing
to an end-extension. This function is defined in T using the recursion the-
orem, in such a way that, as x increases, f reaches a limit after a finite
number of steps. Formally, the limit of f is defined as the unique z satis-
fying the Σ2 formula λ(z) := ∃x∀y ≥ x(f(y) = z).
The function f is constructed to satisfy the additional property that, for
all n, k ∈ ω, T ` ConT|n+λ(k). The desired formula γ(x) is chosen to
express ‘x satisfies the formula whose Gödel number is the limit of f ’.
For everyM |= T and every σ(x) ∈ Σn, the existence of a non-standard
m ∈M such that M |= ConT|m+λ(pσq) follows by the overspill principle.
Fact 2.38 allows for the construction of an end-extension satisfying T +
λ(pσq), and therefore, by Kripke’s trick, ∀x(γ(x) ↔ σ(x)). The existence
of the interpretation then follows from the OHGL characterisation. It
remains to construct a Solovay function f with the desired properties, and
give a formal definition of γ(x).
Opposed to the focus of the earlier sections, the point here is not to qual-
ify for what theories T this may hold, but rather to investigate if there can
be a general method allowing for the construction of such a formula γ(x).
In order to avoid the proofs becoming needlessly complicated, suppose, for
the remainder of this chapter, that every theory mentioned is essentially re-
flexive, e.g. an extension of PA. With some additional work, it is possible
to replace PA with IΣ1 in the lemma below, but since the latter theory is
84
uniformly flexible formulae and solovay functions
finitely axiomatisable and therefore not reflexive, the interpretability result
would not follow.
Lemma 7.10. Let T be a consistent, r.e. extension of PA. There is a recur-
sive function f such that with
λ(z) := ∃x∀y ≥ x(f(y) = z)
the following holds:
1. PA ` ∃zλ(z);
2. ∀n, k ∈ ω, T ` ConT|n+λ(k).
Proof. The recursive function f(x) is defined in PA, using the recursion
theorem. An auxiliary rank function r(x) is simultaneously defined.
Stage 0: f(0) = 0, r(0) = ∞.
Stage x+ 1: Suppose r(x) = m. There are two cases:
Case A: n < m and x is a proof in T|n of ¬λ(k). Then set
f(x+ 1) = k, and r(x+ 1) = n;
Case B: otherwise, set f(x+1) = f(x), and r(x+1) = m.
Provably in PA, r(x+ 1) ≤ r(x), so there is an R = limx r(x). Every
time the value of f changes, r(x+ 1) < r(x), hence there can be at most
finitely many such x. It follows that (1) PA ` ∃zλ(z).
As in the proof of Lemma 7.7, note that for all n ∈ ω, T ` R > n. Fix
n ∈ ω, and reason in T:
Suppose R ≤ n. Let x be minimal such that r(x+ 1) = R.
Then f(x + 1) = k for some k, but since R is the limit of
r(x), k must be the limit of f(x). Hence λ(k) holds. By
construction of f and r, T|R proves ¬λ(k).
In view of essential reflexivity of T,
since ¬λ(k) is proved by T|R and therefore by T|n, it must
be true. The contradiction proves R > n.
85
contributions to the metamathematics of arithmetic
For (2), fix n, k ∈ ω and reason in T:
Suppose x is a proof of ¬λ(k) in T|n. By construction of r,
r(x+1) ≤ n, but as shown above, n < R ≤ r(x+1) holds.
The contradiction proves ConT|n+λ(k).
Proof of Theorem 7.9. Pick n > 1. Let f be as in Lemma 7.10, and let
γ(x) := ∃z(λ(z) ∧ SatΣn(z, x)).
By definition of λ(z), γ(x) is Σmax(2,n). Let σ(x) be any Σn formula, and
let M |= T. It follows from Lemma 7.10 that M |= ConT|n+λ(pσq) for
all n ∈ ω, so by overspill, M |= ConT|m+λ(pσq) for some non-standard
m ∈ M . The arithmetised completeness theorem (Fact 2.38) can now be
used to construct the desired end-extension K |= T + λ(pσq). But since
there can only be one object satisfying λ(z) in K, it follows that K |=
T + ∀x(γ(x) ↔ σ(x)). Since M was arbitrary, T + ∀x(γ(x) ↔ σ(x))
is interpretable in T by the OHGL characterisation.
This result can be used to prove a variation of Hamkins’s theorem 5.3.
The result below is stronger in that it provides end-extensions of any model
of PA, but weaker in that the formula ξ(x) can no longer be assured to be
Σ1.
Corollary 7.11. There is a Σ2 formula ξ(x) such that ifM |= T, and f is
an M-definable function in M2, then M can be end-extended to a model
satisfying T + {ξ(m)f(m) : m ∈M}.
Proof. LetM be any model of T, let f ∈ M2 beM-definable, let ξ(x) be
a Σ2 formula as in Theorem 7.9, and let X = {ξ(m)f(m) : m ∈M}.
The proof is similar to the proof of Theorem 5.3, but using the flexible
formula γ(x) of Theorem 7.9 in place of the one from Theorem 5.1.
This theorem is in one sense the best possible, in that the restriction to
M-definable functions is essential.
Remark 7.12. Let ξ(x) be any formula. There is a function f ∈ ω2 and
a model M |= PA such that M has no end-extension satisfying PA +
{ξ(n)f(n) : n ∈ ω}.
86
uniformly flexible formulae and solovay functions
Proof. Let ξ(x) be any formula and let M be a countable non-standard
model of PA. Suppose that, for each f ∈ ω2, there is an end-extensionNf
of M, satisfying Tf = PA + {ξ(n)f(n) : n ∈ ω}.
If ξ(x) is not independent over PA, this immediately leads to a contra-
diction. Hence, assume that ξ(x) is independent over PA so that for any
choice of f , the theory Tf is consistent and has a model Nf .
Suppose that Nf end-extends M: then ξ(x) represents a setXf in Nf ,
and by Fact 2.34, Xf ∈ SSy(M). For any two different f, g, it must
be the case that Xf 6= Xg. But since there are 2ℵ0 different f ’s, and M
was chosen to be countable, it is impossible for SSy(M) to contain all the
possible Xf ’s.
This result is related to a question posed by Taishi Kurahashi in private
communication. He asked whether there can be a Σ1 formula such that
T + {¬ξ(n) : n ∈ ω} is consistent, and for every f ∈ ω2, the theory T +
{ξ(n)f(n) : n ∈ ω} isΠ1-conservative over T+{¬ξ(n) : n ∈ ω}. In light
of Theorem 6.11, the examples produced above are not counterexamples
to the possible Π1-conservativity, since that would require an f such that
{n ∈ ω : M |= ξ(n)f(n)} is in SSy(M), but such that M has no end-
extension to a model satisfying T + {ξ(n)f(n) : n ∈ ω}.
7.4 Partial results on uniformly flexible Σ1 formulae
With the strong result of the previous section safely in hand, the question
remains whether there can exist a Σ1 formula with similar properties. It
is easy to see that the answer to the unqualified version of Question 7.3 is
negative for n = 1:
Suppose, that there is a Σ1 formula γ(x) that is uniformly flexible for Σ1
over PA. Then by the OHGL characterisation, for every σ(x) ∈ Σ1, every
M |= PA has an end-extension to a model of PA+∀x(γ(x) ↔ σ(x)). If
M is chosen such thatM |= ∃xγ(x) and σ(x) is chosen as theΣ1 formula
x 6= x, then this immediately leads to a contradiction. Hence the question
has to be qualified to rule out pathological counterexamples, suggesting the
following version which is phrased in terms of end-extensions:
87
contributions to the metamathematics of arithmetic
Question 7.13. Is there a Σ1 formula γ(x) such that for every σ(x) ∈ Σ1,
each model of PA + ∀x(γ(x) → σ(x)) has an end-extension to a model
of PA + ∀x(γ(x) ↔ σ(x))?
This question has a trivial positive answer, by letting γ(x) := x = x.
Then every model satisfying PA + ∀x(γ(x) → σ(x)) must also satisfy
∀x(γ(x) ↔ σ(x)). A further qualification is:
Question 7.14. Is there a Σ1 formula γ(x) such that for every σ(x) ∈ Σ1,
and every M |= PA,
1. if M |= ConPA, then M |= ∀x¬γ(x);
2. if M |= PA + ∀x(γ(x) → σ(x)) then there is an end-extension of
M satisfying PA + ∀x(γ(x) ↔ σ(x))?
By reformulating Theorem 7.5 in terms of Σ1 formulae rather than in-
dices for r.e. sets it is easy to see that the answer to the question is positive
when the choice of σ(x) is restricted to formulae with finite extensions in
the base model M. Theorem 5.1 shows that if the answer to the question
is negative in general, then a counterexample must come in the shape of
a σ(x) ∈ Σ1 and a model of PA + ¬ConPA + ∀x(γ(x) → σ(x)) with
no end-extension to a model of PA + ∀x(γ(x) ↔ σ(x)). However, if
attention is restricted to precisely models of PA + ¬ConPA, it is easy to
construct a silly formula having almost the properties asked for:
Remark 7.15. There is a Σ1 formula γ(x), such that for every σ(x) ∈ Σ1
and every M |= PA,
1. if M |= ConPA, then M |= ∀x¬γ(x);
2. if M |= ¬ConPA + ∀x(γ(x) → σ(x)), then there is an end-
extension of M satisfying PA + ∀x(γ(x) ↔ σ(x)).
Proof. Let γ(x) := ¬ConPA ∧ (x = x). Then (1) is immediate. For
(2), pick any M that satisfies PA + ¬ConPA + ∀x(γ(x) → σ(x)). Then
PA + ∀x(γ(x) ↔ σ(x)) + ThΣ1(M) is consistent. The existence of the
desired end-extension is now a consequence of Theorem 6.2.
88
uniformly flexible formulae and solovay functions
This result does not answer Question 7.14, since it is not guaranteed
that any model of PA + ConPA can be end-extended to a model of PA +
∀x(γ(x) ↔ σ(x)). Neither does the next result or its corollaries give
exactly what is asked for, but here the failure comes in the possibly non-
standard shape of the formula being satisfied in the end-extension.
Theorem 7.16. There is a Σ1 formula γ(x) such that for every M |= PA:
1. if M |= ConPA, then M |= ∀x¬γ(x), and for each σ(x) ∈ Σ1,
there is an end-extension N0 |= PA of M such that
N0 |= ∀x(γ(x) ↔ σ(x));
2. otherwise, there is an M-finite set of possibly non-standard Σ1 for-
mulae σ0(x), . . . , σs(x) such that
M |= ∀x(γ(x) ↔ σ0(x) ∨ · · · ∨ σs(x))
and for every σ(x) ∈ Σ1, there is an end-extensionN1 |= PA ofM
such that
N1 |= ∀x(γ(x) ↔ σ0(x) ∨ · · · ∨ σs(x) ∨ σ(x)).
Proof. Suppose, without loss of generality, that SatΣ1(z, x) is such that
every value of z encodes a Σ1 formula. Let We be as in Theorem 7.5, and
let, abusing language, γ(x) be the Σ1 formula ∃z(z ∈We ∧ SatΣ1(z, x)).
For (1), suppose that M |= ConPA. Then by Theorem 7.5, We = ∅
as calculated in M. Hence γ(x) is false for every x. Let σ(x) be any Σ1
formula. Again by the theorem, there is an end-extension of M in which
We = {pσq}, and the conclusion follows.
For (2), let {a0, a1, . . . , as} be We as calculated within M. For each
i ≤ s let σi(x) be the Σ1 formula SatΣ1(ai, x). By reasoning within M
it is easy to ascertain that
M |= ∀x(γ(x) ↔ σ0(x) ∨ · · · ∨ σs(x)).
Let σ(x) be any Σ1 formula. By Theorem 7.5, there is an end-extension
N1 |= PA of M in which We = {a0, . . . , as, pσq}. It follows that
N1 |= ∀x(γ(x) ↔ σ0(x) ∨ · · · ∨ σs(x) ∨ σ(x)).
89
contributions to the metamathematics of arithmetic
Remark 7.17. This is as good as it gets when it comes to applying Kripke’s
method to the problem at hand. The general form of the formulae γ(x)
used in Kripke-style proofs is ∃z(φ(z) ∧ SatΣn(z, x)), where the unique
object satisfying φ(z) can change when passing to an end-extension. The
uniqueness is necessary for γ(x) to have the same extension as the chosen
formula σ(x). If the condition φ(z) is Σ1, new witnesses to φ(z) can
be added, but the old ones can not be lost due to Σ1-persistence. This
means that there can never be a new unique object satisfying φ(z) in the
end-extension.
Corollary 7.18. Suppose that γ(x) is as in Theorem 7.16, and that We
as calculated within M is a finite set of natural numbers when viewed ex-
ternally. Then there is a standard formula σ0(x) :=
∨∨
ai∈We SatΣ1(ai, x)
such that M |= ∀x(γ(x) ↔ σ0(x)), and for every σ(x) ∈ Σ1, there is
an end-extension N2 |= PA of M such that
N2 |= ∀x(γ(x) ↔ σ0(x) ∨ σ(x)).
Corollary 7.19. If M, γ(x) and σ0(x) are as in Corollary 7.18, then if
σ(x) ∈ Σ1 is chosen such that PA ` ∀x(σ0(x) → σ(x)), there is an
end-extension N3 |= PA of M such that
N3 |= ∀x(γ(x) ↔ σ(x)).
The best partial result available at this point is the one below. It is due
to Volodya Shavrukov, and it is included here with his graceful permission.
For technical reasons, the result is phrased in terms of (indices for) r.e. sets,
rather than Σ1-formulae, but the translation between these is, as always,
straightforward.
Theorem 7.20 (Shavrukov, unpublished). Suppose that T is a consistent,
r.e. extension of PA. There is an r.e. set We such that:
1. N |= We = ∅;
2. for each j ∈ ω, every model M |= T can be end-extended to a
model K |= T +We =∗ Wj , where =∗ is equality modulo finite
differences.
90
uniformly flexible formulae and solovay functions
Proof. Using the recursion theorem, the setWe is defined (provably in PA)
by the stages We,x in which it acquires its elements, together with an aux-
iliary function r(x). Assume that if nothing is added to a set Wn at stage
x, then Wn,x = ∅.
Stage 0: We,0 = ∅. r(0) = ∞. Assume that the ordering of the r.e. sets
is such that W∞ is the empty set.¹⁵
Stage x+ 1: Suppose r(x) = m.
Case A: there is a proof in T|n of We 6=∗ Wm and n < m.
Then let We,x+1 be Wn,x+1, and set r(x+ 1) = n;
Case B: otherwise, We,x+1 = Wm,x+1, and r(x+ 1) = m.
Let We =
⋃
x∈ωWe,x.
The idea is that We remains empty until the procedure encounters an
n such that T|n proves that We 6=∗ ∅. At this stage, the procedure starts
enumerating Wn instead, until it encounters a smaller n′ such that T|n′
proves that We 6=∗ Wn′ , et cetera. Hence, at each stage x, x limits the
number of objects that have been put in We, as well as the number of
objects having been left out from the r.e. set Wr(x) currently enumerated,
suggesting that if this process comes to an end, for some y, We is equal to
Wr(y) modulo finite differences.
Provably in PA, r(x+ 1) ≤ r(x), so there exists R = limx r(x). Since
at each stage x at which We starts enumerating a new r.e. set, it must be
the case that r(x+ 1) < r(x), so there can be at most finitely many such
x. Hence:
PA ` “After a finite number of steps, We settles on which r.e.
set it enumerates.”
It also follows that T ` R > n for all n ∈ ω. Fix n and reason in T:
Suppose R ≤ n. Let x be minimal such that r(x+ 1) = R.
Then for all z > x, z ∈ We iff z ∈ WR, which implies
We =∗ WR. But by construction of r(x+ 1) it also follows
that T|R `We 6=∗ WR.
¹⁵Should this assumption on the ordering of r.e. sets feel uncomfortable, it is easy to divide
the construction of We in two separate procedures, bypassing the use of W∞.
91
contributions to the metamathematics of arithmetic
Since T is reflexive:
We 6=∗ WR is proved by T|R and therefore by T|n, so it must
be true. The contradiction proves R > n.
Since R ≤ n is T-equivalent to a Σ1 sentence, it would imply its own
provability in T. Since T is consistent, this implies R = ∞ in the real
world. Hence N |= We = ∅.
For (2), fix n and argue in T:
Pick j and suppose x is a proof of We 6=∗ Wj in T|n. By
construction of r, r(x + 1) ≤ n. But n < R ≤ r(x + 1),
and the contradiction proves Con(T|n+We =∗ Wj).
Let M |= T, and pick a j ∈ ω. By overspill, and the argument above,
M |= ConT|m+We=∗Wj for some non-standard m ∈ M . Fact 2.38 can
now be used to construct the end-extension K |= T +We =∗ Wj .
7.5 Hierarchical generalisations: Asking the right
question
As in the preceding chapters, it is time to discuss hierarchical generalisa-
tions. By modifying the proofs of Lemma 7.10 and Theorem 7.9 in a way
that is detailed below, it is possible to prove the following:
Theorem 7.21. Let T be a consistent, r.e. extension of PA. There is a Σn+2
formula γ(x) such that for every σ(x) ∈ Σn+2, every model of T has a
Σn-elementary extension satisfying T + ∀x(γ(x) ↔ σ(x)).
The necessary modifications can be outlined as follows.
Proof sketch. Fix n and let a ∆n+1 function f(x) be defined in PA by:
Stage 0: f(0) = 0, r(0) = ∞.
Stage x+ 1: Suppose r(x) = m. There are two cases:
Case A: i < m and x is a proof in (T + ThΣn+1(N))|i of
¬λ(k). Then set f(x+ 1) = k, and r(x+ 1) = i;
Case B: otherwise, set f(x+1) = f(x), and r(x+1) = m.
92
uniformly flexible formulae and solovay functions
This construction is admissible by the recursion theorem (Fact 2.53), and
f is then ∆n+1, since by Craig’s trick, T + ThΣn+1(N) has a deductively
equivalent Πn definition. Since f is ∆n+1, the formula λ(x) expressing
that x is the limit of f is Σn+2. Most of the proof then goes through as it
stands. For the final part, Let M |= T, fix n,m, k ∈ ω and reason in T:
Suppose that x is a proof in (T + ThΣn+1(N))|m of ¬λ(k).
Then r(x + 1) < m and m < R ≤ r(x + 1). The contra-
diction proves Con(T,Σn+1)|m+λ(k).
Let γ(x) be ∃z(λ(z) ∧ SatΣn+2(z, x)) and let σ(x) be any Σn+2 for-
mula. Since M satisfies overspill, there is a non-standard m ∈ M such
thatM |= Con(T,Σn+1)|m+λ(pσq). Now use Fact 2.38 to construct an end-
extension K satisfying T + ThΣn+1(M) + λ(pσq). Using Kripke’s trick,
conclude that K |= T + ThΣn+1(M) + ∀x(γ(x) ↔ σ(x)), whence K is
a Σn-elementary extension of M.
With this theorem in hand, it turns out that the success of Theorem 7.9
is a special case of a more general phenomenon. Hence, a more general
question, informed by the questions asked at the outset of this chapter and
the theorem above, can be phrased as:
Question 7.22. Is there a Σn+1 formula γ(x), such that N |= ∀x¬γ(x),
and for each Σn+1 formula σ(x), every model of T + ∀x(γ(x) → σ(x))
has a Σn-elementary extension satisfying T + ∀x(γ(x) ↔ σ(x))?
Remark 7.23. The additional assumption that the base model satisfies
∀x(γ(x) → σ(x)) reappears here to take into account the elementarity
for Σn formulae. Similar to the case of Σ1-persistence over end-extensions,
Σn+1 sentences persist when passing to a Σn-elementary extension.
An affirmative answer to this question would improve Theorems 7.5 and
7.21, as well as cast some light on the question asked in Section 7.4. Given
the general formulations of the hierarchical generalisations throughout this
thesis, it seems reasonable to claim that there is nothing special about the
case n = 0, i.e., the case concerning Σ1 formulae. Following this line of
thought – if an answer is given for any n, it is likely that the same proof or
disproof could be easily transformed to encompass the other cases as well.
93

8 Concluding remarks
A number of more or less interesting problems are left open in this thesis.
The first three of these originate in Chapter 3:
Question 8.1. Can the collection of sets of fixed points over T be charac-
terised among the creative sets?
Question 8.2. Is there a Γ formula θ(x) such that FixΓ(θ) is neither re-
cursive nor creative?
Question 8.3. IsFΓ an ultrafilter onRΓ?
An observation is that it seems difficult to say something in general
about the number of fixed points (up to provable equivalence) of a non-
extensional formula. This difficulty is related to the long-standing problem
of whether all Rosser sentences are provably equivalent or not.
A lesson to be learned from this thesis is the success of Kripke’s method in
establishing numerous generalisations of the first incompleteness theorem.
The method is prevalent throughout Chapters 4, 5 and 7, and is used in
some form in almost every proof. On the other hand, even when combined
with the powerful method of Solovay functions, each instance of a very
general problem remain unsolved:
Question 8.4. Suppose that T is a consistent, r.e. extension of PA. Is
there a Σn+1 formula γ(x), such that N |= ∀x¬γ(x), and for each Σn+1
formula σ(x), every model of T+∀x(γ(x) → σ(x)) has a Σn-elementary
extension satisfying T + ∀x(γ(x) ↔ σ(x))?
In particular, in the case n = 0, an affirmative answer would establish
the interpretability of T + ∀x(γ(x) ↔ σ(x)) in T + ∀x(γ(x) → σ(x)),
which would be a strengthening of Feferman’s theorem on the interpret-
ability of inconsistency. By complexity calculations, the possibility that
Kripke’s method can be used to establish such a result can be ruled out.
95
contributions to the metamathematics of arithmetic
As a contrast, Theorem 7.21 can be interpreted as saying that very much
can change at the Σn+2 level of a model of PA, while leaving the Σn level
completely untouched. Ensuring that the Σn+1 level can be preserved
seems to be much more difficult.
The final question listed here is due to Taishi Kurahashi.
Question 8.5. Is there a Σ1 formula ξ(x) such that T+{¬ξ(n) : n ∈ ω}
is consistent, and for each f ∈ ω2, the theory T + {ξ(n)f(n) : n ∈ ω} is
Π1-conservative over T + {¬ξ(n) : n ∈ ω}?
96
References
Beklemishev, L. (1998). Review: Per Lindström, Aspects of Incomplete-
ness. The Journal of Symbolic Logic, 63(4):1606–1608.
Beklemishev, L. and Visser, A. (2005). On the limit existence principles in
elementary arithmetic and Σ0n-consequences of theories. Annals of Pure
and Applied Logic, 136:56–74.
Beklemishev, L. D. (2005). Reflection principles and provability algebras
in formal arithmetic. Russian Mathematical Surveys, 60(2):197–268.
Bennet, C. (1986). Lindenbaum algebras and partial conservativity. Pro-
ceedings of the American Mathematical Society, 97(2):323–327.
Bernardi, C. (1981). On the relation provable equivalence and on parti-
tions in effectively inseparable sets. Studia Logica, 40(1):29–37.
Blanck, R. (2011). Metamathematical fixed points. Licentiate thesis, Uni-
versity of Gothenburg.
Blanck, R. (2016). Flexibility in fragments of Peano arithmetic. In Cégiel-
ski, P., Enayat, A., and Kossak, R., editors, New Studies in Weak Arith-
metics, Vol. 3, number 217 in CSLI Lecture Notes, pages 1–20. CSLI
Publications.
Blanck, R. and Enayat, A. (2017). Marginalia on a theorem of Woodin.
The Journal of Symbolic Logic, 82(1):359–374.
Carnap, R. (1937). The Logical Syntax of Language. Routledge & Kegan
Paul.
Chaitin, G. J. (1974). Information-theoretic limitations of formal systems.
Journal of the ACM, 21:403–424.
97
contributions to the metamathematics of arithmetic
Cornaros, Ch. and Dimitracopoulos, C. (2000). A note on end extensions.
Archive for Mathematical Logic, 39:459–463.
Craig, W. (1953). On axiomatizability within a system. The Journal of
Symbolic Logic, 18(1):30–32.
D’Aquino, P. (1993). A sharpened version of McAloon’s theorem on initial
segments of models of I∆0. Annals of Pure and Applied Logic, 61:49–62.
Dimitracopoulos, C. and Paris, J. (1988). A note on a theorem of H. Fried-
man. Zeitschrift für mathematische Logik und Grundlagen der Mathem-
atik, 34:13–17.
Ehrenfeucht, A. and Feferman, S. (1960). Representability of recursively
enumerable sets in formal theories. Archiv für mathematische Logik und
Grundlagenforschung, 5(1–2):37–41.
Feferman, S. (1960). Arithmetization of metamathematics in a general
setting. Fundamenta Mathematicae, 49:35–92.
Feferman, S. (1962). Transfinite recursive progressions of axiomatic theor-
ies. The Journal of Symbolic Logic, 27(3):259–316.
Feferman, S., Kreisel, G., and Orey, S. (1962). 1-consistency and faith-
ful interpretations. Archiv für mathematische Logik und Grundlagen-
forschung, 6(1–2):52–63.
Franzén, T. (2005). Gödel’s Theorem: An Incomplete Guide to its Use and
Abuse. A. K. Peters.
Gödel, K. (1930). Die Vollständigkeit der Axiome des logischen Funktion-
enkalküls. Monatshefte für Mathematik und Physik, 37:349–360.
Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Math-
ematica und verwandter Systeme, I. Monatshefte für Mathematik und
Physik, 38:173–198.
Grzegorczyk, A., Mostowski, A., and Ryll-Nardzewski, C. (1958). The
classical and the ω-complete arithmetic. The Journal of Symbolic Logic,
23(2):188–206.
98
references
Guaspari, D. (1979). Partially conservative extensions of arithmetic. Trans-
actions of the American Mathematical Society, 254:47–68.
Hájek, P. (1971). On interpretability in set theories. Commentationes
Mathematicae Universitatis Carolinae, 12(1):73–79.
Hájek, P. (1987). Partial conservativity revisited. Commentationes Math-
ematicae Universitatis Carolinae, 28(4):679–690.
Hájek, P. (1993). Interpretability and fragments of arithmetic. In Clote,
P. and Krajíček, J., editors, Arithmetic, Proof Theory, and Computational
Complexity, volume 23 of Oxford Logic Guides, pages 185–196. Claren-
don Press.
Hájek, P. and Montagna, F. (1990). The logic of Π1-conservativity. Archive
for Mathematical Logic, 30:113–123.
Hájek, P. and Pudlák, P. (1993). Metamathematics of First Order Arithmetic.
Perspectives in Mathematical Logic. Springer-Verlag.
Halbach, V. and Visser, A. (2014). Self-reference in arithmetic I. Review
of Symbolic Logic, 7(4):671–691.
Hamkins, J. D. (2016). Every function can be computable. http://jdh.
hamkins.org/every-function-can-be-computable/.
[Online; accessed 2017-04-30].
Harary, F. (1961). A very independent axiom system. The American Math-
ematical Monthly, 68(2):159–162.
Hilbert, D. and Bernays, P. (1934–1939). Grundlagen der Mathematik,
volume 1–2. Springer-Verlag.
Japaridze, G. (1994). A simple proof of arithmetical completeness for Π1-
conservativity logic. Notre Dame Journal of Formal Logic, 35(3):346–
354.
Jensen, D. and Ehrenfeucht, A. (1976). Some problem in elementary arith-
metics. Fundamenta Mathematicae, 92(3):223–245.
99
contributions to the metamathematics of arithmetic
Jeroslow, R. G. (1971). Consistency statements in formal theories. Funda-
menta Mathematicae, 72(1):17–40.
Jeroslow, R. G. (1975). Experimental logics and ∆02-theories. Journal of
Philosophical Logic, 4(3):253–267.
Joosten, J. J. (2004). Interpretability formalized. PhD thesis, Utrecht Uni-
versity.
Kaså, M. (2012). Experimental logics, mechanism and knowable consist-
ency. Theoria, 78(3):213–224.
Kaye, R. (1991). Models of Peano Arithmetic, volume 15 of Oxford Logic
Guides. Clarendon Press.
Kikuchi, M. and Kurahashi, T. (2016). Illusory models of Peano arithmetic.
The Journal of Symbolic Logic, 81(3):1163–1175.
Kikuchi, M. and Kurahashi, T. (20xx). Generalizations of Gödel’s incom-
pleteness theorems for Σn-definable theories of arithmetic. Manuscript.
Kleene, S. C. (1952). Introduction to Metamathematics. North-Holland.
Kossak, R. and Schmerl, J. (2006). The Structure of Models of Peano Arith-
metic, volume 50 of Oxford Logic Guides. Clarendon Press.
Kreisel, G. (1962). On weak completeness of intuitionistic predicate logic.
The Journal of Symbolic Logic, 27(2):139–158.
Kripke, S. A. (1962). “Flexible” predicates of formal number theory. Pro-
ceedings of the American Mathematical Society, 13(4):647–650.
van Lambalgen, M. (1989). Algorithmic information theory. The Journal
of Symbolic Logic, 54(4):1389–1400.
Li, M. and Vitányi, P. (1993). An Introduction to Kolmogorov Complexity
and Its Applications. Springer-Verlag.
Lindström, P. (1979). Some results on interpretability. In Proceedings of the
5th Scandinavian Logic Symposium 1979, pages 329–361.
100
references
Lindström, P. (1984). A note on independent formulas. In Notes on for-
mulas with prescribed properties in arithmetical theories, number 25 in
Philosophical Communications, Red Series, pages 1–5. Göteborgs Uni-
versitet.
Lindström, P. (2003). Aspects of Incompleteness. Number 10 in Lecture
Notes in Logic. A. K. Peters, 2nd edition.
Lindström, P. and Shavrukov, V. Yu. (2008). The ∀∃ theory of Peano Σ1
sentences. Journal of Mathematical Logic, 8(2):251–280.
Löb, M. H. (1955). Solution of a problem of Leon Henkin. The Journal
of Symbolic Logic, 20(2):115–118.
Löwenheim, L. (1915). Über Möglichkeiten im Relativkalkül. Mathemat-
ische Annalen, 76(4):447–470.
Maltsev, A. (1936). Untersuchungen aus dem Gebiete der mathematischen
Logik. Matématičéskij sbornik, n.s., 1:323–336.
McAloon, K. (1982). On the complexity of models of arithmetic. The
Journal of Symbolic Logic, 47(2):403–415.
Montagna, F. (1982). Relatively precomplete numerations and arithmetic.
Journal of Philosophical Logic, 11(4):419–430.
Montague, R. (1962). Theories incomparable with respect to relative inter-
pretability. The Journal of Symbolic Logic, 27(2):195–211.
Mostowski, A. (1952). On models of axiomatic systems. Fundamenta
Mathematicae, 39(1):133–158.
Mostowski, A. (1961). A generalization of the incompleteness theorem.
Fundamenta Mathematicae, 49(2):205–232.
Myhill, J. (1955). Creative sets. Zeitschrift für mathematische Logik und
Grundlagen der Mathematik, 1:97–108.
101
contributions to the metamathematics of arithmetic
Myhill, J. (1972). An absolutely independent set of Σ01-sentences. Zeit-
schrift für mathematische Logik und Grundlagen der Mathematik, 18:107–
109.
Orey, S. (1961). Relative interpretations. Zeitschrift für mathematische
Logik und Grundlagen der Mathematik, 7:146–153.
Paris, J. B. (1981). Some conservations results for fragments of arithmetic.
In Berline, C., McAloon, K., and Ressayre, J., editors, Model Theory and
Arithmetic, volume 890 of Lecture notes in Mathematics, pages 251–262.
Springer-Verlag.
Post, E. L. (1948). Degrees of recursive unsolvability. Bulletin of the Amer-
ican Mathematical Society, 54(7):641–642.
Pudlák, P. (1985). Cuts, consistency statements and interpretations. The
Journal of Symbolic Logic, 50(2):423–441.
Putnam, H. and Smullyan, R. M. (1960). Exact separation of recursively
enumerable sets within theories. Proceedings of the American Mathemat-
ical Society, 11:574–577.
Raatikainen, P. (1998). On interpreting Chaitin’s incompleteness theorem.
Journal of Philosophical Logic, 27(6):569–586.
Ressayre, J.-P. (1987). Nonstandard universes with strong embeddings,
and their finite approximations. In Logic and Combinatorics, volume 65
of Contemporary Mathematics, pages 333–358. American Mathematical
Society.
Robinson, A. (1963). On languages which are based on non-standard arith-
metic. Nagoya Mathematical Journal, 22:83–117.
Rogers, Jr., H. (1967). Theory of Recursive Functions and Effective Comput-
ability. McGraw-Hill.
Rosser, J. B. (1936). Extensions of some theorems of Gödel and Church.
The Journal of Symbolic Logic, 1(3):87–91.
102
references
Salehi, S. and Seraji, P. (2016). Gödel-Rosser’s incompleteness theorem,
generalized and optimized for definable theories. Journal of Logic and
Computation. Advance online article, doi:10.1093/logcom/exw025.
Scott, D. (1962). Algebras of sets binumerable in complete extensions
of arithmetic. In Dekker, J. C. E., editor, Recursive Function Theory,
volume 5 of Proceedings of Symposia in Pure Mathematics, pages 117–121.
American Mathematical Society.
Shavrukov, V. Yu. (1997). Interpreting reflexive theories in finitely many
axioms. Fundamenta Mathematicae, 152:99–116.
Simpson, S. G. (1999). Subsystems of Second Order Arithmetic. Springer-
Verlag.
Sjögren, J. (2008). On explicating the concept the power of an arithmetical
theory. Journal of Philosophical Logic, 37:183–202.
Skolem, T. (1920). Logisch-kombinatorische Untersuchungen über die
Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem The-
oreme über dichte Mengen. Videnskapsselskapets Skrifter, I. Matematisk-
naturvidenskabelig Klasse, 4:1–36.
Smoryński, C. (1984). Lectures on nonstandard models of arithmetic. In
Lolli, G., Longo, G., and Marcja, A., editors, Logic Colloquium ’82,
volume 112 of Studies in Logic and the Foundation of Mathematics, pages
1–70. North-Holland.
Smoryński, C. (1985). Self-Reference and Modal Logic. Springer-Verlag.
Smoryński, C. (1987). Quantified modal logic and self-reference. Notre
Dame Journal of Formal Logic, 28(3):356–370.
Smullyan, R. M. (1961). Theory of Formal Systems, volume 47 of Annals of
Mathematics Studies. Princeton University Press.
Solovay, R. M. (1976). Provability interpretations of modal logic. Israel
Journal of Mathematics, 25:287–304.
103
contributions to the metamathematics of arithmetic
Sommaruga-Rosolemos, G. (1991). Fixed Point Constructions in Various
Theories of Mathematical Logic. Bibliopolis.
Tarski, A. (1933). The concept of truth in formalized languages. In
Corcoran, J., editor, Logic, Semantics, Metamathematics, pages 152–278.
Hackett Publishing Company.
Tarski, A., Mostowski, A., and Robinson, R. M. (1953). Undecidable The-
ories. North-Holland.
Verbrugge, R. and Visser, A. (1994). A small reflection principle for
bounded arithmetic. The Journal of Symbolic Logic, 59(3):785–812.
Visser, A. (1980). Numerations, λ-calculus & arithmetic. In Seldin, J. P.
and Hindley, J. R., editors, To H. B. Curry: Essays on Combinatory Logic,
Lambda Calculus and Formalism, pages 259–284. Academic Press.
Visser, A. (1990). Interpretability logic. In Petkov, P., editor, Mathematical
Logic, pages 175–209. Plenum Press.
Wilkie, A. J. (1977). On the theories of end-extensions of models of arith-
metic. In Set Theory and Hierarchy Theory, volume 619 of Lecture Notes
in Mathematics, pages 305–310. Springer-Verlag.
Wong, T. L. (2016). Interpreting weak König’s lemma using the arithmet-
ized completeness theorem. Proceedings of the American Mathematical
Society, 144(9):4021–4024.
Woodin, W. H. (2011). A potential subtlety concerning the distinction
between determininsm and nondeterminism. In Heller and Woodin,
editors, Infinity, New Research Frontiers, pages 119–129. Cambridge Uni-
versity Press.
104
Sammanfattning
1 Inledning
En viktig insikt som den matematiska logiken gör är att sanning och bevis-
barhet är komplicerade begrepp. Den här avhandlingen bidrar till studiet av
den invecklade relationen mellan sanning och bevisbarhet i sådana formella
teorier som lämpar sig för att beskriva de naturliga talen 0, 1, 2, ….
Det mest inflytelserika tekniska resultatet som beskriver denna relation
är Gödels första ofullständighetssats: Välj ett motsägelsefritt formellt system
som är sådant att det finns en mekanisk metod för att avgöra om en given
sats är ett axiom i systemet eller ej. Om detta system är tillräckligt starkt
för att kunna uttrycka en viss del av den elementära aritmetiken, så är det
också tillräckligt starkt för att kunna konstruera en sats som handlar om
tal, som är sann men omöjlig att bevisa inom systemet (Gödel, 1931).
Avhandlingen behandlar flera typer av generaliseringar av ofullständig-
hetssatserna, främst genom studiet av så kallade oberoende och flexibla
formler. Det första temat är att försöka besvara frågan om vilka teorier som
kan bevisa vilka ofullständighetsresultat; detta är ett bidrag till studiet av
svaga aritmetiska teorier där Hájek och Pudlák (1993) är ett nyckelverk. Ett
annat tema rör möjligheten att generalisera ofullständighetsresultat till teo-
rier som inte är rekursivt enumerabla. Liknande frågor har behandlats av till
exempel Jeroslow (1975); Kaså (2012); Salehi och Seraji (2016). Det sista
temat rör Fefermans (1960) generalisering av Gödels andra ofullständig-
hetssats. Fefermans resultat säger att påståendet ”teorin T är motsägelsefri”
är interpreterbart (i en teknisk mening) i T, och här görs försök att bevisa
liknande resultat för oberoende och flexibla formler.
105
contributions to the metamathematics of arithmetic
2 Bakgrund
I detta kapitel presenteras nödvändigt bakgrundsmaterial. Läsaren förut-
sätts vara bekant med första ordningens logik, teorierna Q (Robinsons arit-
metik) och PA (Peanos aritmetik), den grundläggande teorin för rekursiva
funktioner, och naiv mängdteori.
3 Fixpunktsmängder
Fixpunktssatsen och dess variationer används ofta för att konstruera ”själv-
refererande” satser i form av fixpunkter: φ är en fixpunkt till θ(x) i T
omm T ` φ ↔ θ(pφq). Flera klassiska resultat kan bevisas med hjälp
av detta verktyg, däribland Gödels första ofullständighetssats, Tarskis re-
sultat att aritmetisk sanning inte är aritmetiskt definierbar, samt Löbs sats.
Lindström (2003) ger en bild av hur mångsidig tekniken är. I detta kapitel
studeras fixpunkter från ett annat perspektiv: givet enLA-formel θ(x), vad
kan vi säga om mängden av fixpunkter till θ(x)?
Det viktigaste resultatet är att varje fixpunktsmängd är kreativ i Rogers
(1967) tekniska bemärkelse, och att detta kan generaliseras till de begränsa-
de fixpunktsmängder som är disjunkta från någon annan sådan fixpunkts-
mängd. Detta resultat ger en marginell förstärkning av ett reslutat av Hal-
bach och Visser (2014). Bidrag görs också till studiet av den algebraiska
struktur som erhålls när rekursiva, begränsade fixpunktsmängder ordnas
under mängdinklusion.
4 Flexibilitet i fragment
Detta kapitel fyller flera syften. Först introduceras de centrala begreppen
oberoende och flexibla formler, och därefter ges en litteraturöversikt från
fältets begynnelse under tidigt 1960-tal fram till 2016. Ett annat syfte är
att framhålla Kripkes metod (1962) som överlägsen i att konstruera obe-
roende och flexibla formler. Därutöver tas tillfället att relatera de klassiska
resultaten till det modernare studiet av svaga aritmetiker, genom att upp-
skatta hur mycket matematisk induktion som behövs för att bevisa dessa
olika resultat.
106
sammanfattning
5 Formalisering och ändextensioner
Resultaten i kapitel 4 garanterar, tillsammans med fullständighetssatsen för
första ordningens logik, existensen av en rekursiv funktion f och en siffra
e som är sådana att det för varje k ∈ ω finns en modell som satisfierar
T + f(e) = k. Varje sådan modell är trivialt en ändextension av standard-
modellen. Frågan som behandlas här är om detta är en specialegenskap hos
standardmodellen, eller om det finns andra strukturer som har liknande
ändextensioner. Det viktigaste resultatet i detta kapitel är att varje modell
till T+ConT har sådana ändextensioner, och bevismetoderna kan finslipas
för att bevisa starkare resultat av liknande slag.
6 Karaktäriseringar av partiell konservativitet
Det är känt sedan det sena 1970-talet att ändextensioner av modeller till
aritmetik spelar en viktig roll i karaktäriseringar av interpreterbarhet och
partiell konservativitet, som båda är användbara begrepp för att jämföra
formella teoriers relativa styrka. Här generaliseras den så kallade OHGL-
karaktäriseringen (efter Orey, Hájek, Guaspari och Lindström) på tre sätt.
Karaktäriseringar ges av partiell konservativitet över svaga teorier, teorier
formulerade i utökade språk, samt teorier som inte är rekursivt enumerabla.
7 Uniformt flexibla formler och Solovayfunktioner
I kapitel 5 fastställs att det för varje n > 0 finns en formel γ(x) ∈ Σn, som
är sådan att för varje σ(x) ∈ Σn och varje modellM |= T+ConT så finns
en ändextension avM som satisfierar T+∀x(γ(x) ↔ σ(x)). Frågan som
behandlas i det här kapitlet är om antagandet att T satisfierar ConT kan
strykas. Om detta är möjligt så ger OHGL-karaktäriseringen upphov till
en interpretation av T+∀x(γ(x) ↔ σ(x)) i T, vilket skulle ge en förstärk-
ning av den generalisering av Gödels andra ofullständighetssats som härrör
från Feferman (1960). Här bevisas, med hjälp av så kallade Solovayfunk-
tioner, att antagandet kan strykas om n > 1. Det mest intressanta fallet är
dock just n = 1 och i detta fall ges partiella resultat bland annat genom att
generalisera ett resultat från Woodin (2011).
107