Efficient Metamathematics

Verbrugge L.C. - Efficient metamathematics (1993) ......Page 1
Contents ......Page 5
Dankwoord ......Page 7
Part I. Introduction and background ......Page 8
1.1 What is efficiency? ......Page 9
1.3 Interpretability and its logics ......Page 11
1.5 Efficient metamathematics of inefficient mathematics ......Page 12
1.6 What to expect from the rest of the dissertation? ......Page 13
2.1 Theories of arithmetic ......Page 15
2.2 Provability logic ......Page 17
2.3.1 IΔ0 + Ω1 ......Page 18
2.3.2 Buss’ systems of bounded arithmetic and the polynomial hierarchy ......Page 19
2.3.3 Metamathematics for bounded arithmetic ......Page 23
2.4 Interpretations ......Page 26
2.5 Interpretability logic ......Page 29
2.6 Definable cuts ......Page 31
2.7 Cuts may help to characterize interpretability ......Page 35
2.8.1 IΔ0 + EXP proves restricted consistency statements ......Page 38
2.8.2 Conservativity ......Page 42
2.8.3 Non-conservativity and incompleteness ......Page 43
Part II. Metamathematics for bounded arithmetic ......Page 47
3.1 Introduction ......Page 49
3.2 Σ-completeness and the NP = co-NP problem ......Page 51
3.3 The small reflection principle ......Page 54
3.4 Injection of small (but not too small) inconsistency proofs ......Page 66
4.1 Introduction ......Page 71
4.2 If S12 proves completeness for all Σ1-sentences, then NP ∩ co-NP = P ......Page 72
5.1 Introduction ......Page 73
5.2 Arithmetical preliminaries ......Page 74
5.3 Trees of undecidable sentences ......Page 77
5.4 Upper bounds on PLΩ ......Page 79
5.5 Disjunction property ......Page 82
Part III. Metamathematics for Peano arithmetic ......Page 85
6.1 Introduction ......Page 87
6.2 Feasible interpretations in various settings ......Page 88
6.3 Soundness of ILM for feasible interpretability over PA ......Page 96
6.4 Interpretability does not imply feasible interpretability ......Page 101
6.5 ILM is the logic of feasible interpretability over PA ......Page 105
7.1 Introduction ......Page 115
7.2 Preliminaries and notation ......Page 116
7.3 Characterizations of feasible interpretability ......Page 118
7.4 The set of Σb1-axiomatized theories feasibly interpretable over PA is Σ2-complete ......Page 121
7.5 Lindström’s general lemmas polynomialized ......Page 124
7.6 Feasible interpretability is Σ2-complete ......Page 127
Bibliography ......Page 131
Samenvatting ......Page 137