Kohlenbach Applied Proof Theory: Proof Interpretations and their Use in Mathematics

1. Auflage 2008
ISBN: 978-3-540-77533-1
Verlag: Springer Berlin Heidelberg
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 536 Seiten

Reihe: Springer Monographs in Mathematics

Autoren/Hrsg.

Kohlenbach, Ulrich

Inhaltsverzeichnis

1;Preface;6
2;Acknowledgements;10
3;Common Notations and Terminology;16
4;Introduction;19
5;Unwinding proofs (`Proof Mining');30
5.1;Introductory remark;30
5.2;Informal treatment of ineffective proofs;30
5.3;Herbrand's theorem and the no-counterexample interpretation;39
5.4;Exercises, historical comments and suggested further reading;55
6;Intuitionistic and classical arithmetic in all finite types;58
6.1;Intuitionistic and classical predicate logic;58
6.2;Intuitionistic (`Heyting') arithmetic HA and Peano arithmetic PA;61
6.3;Extensional intuitionistic (`Heyting') and classical (`Peano') arithmetic in all finite types;63
6.4;Fragments of (W)E-HA and (W)E-PA;69
6.5;Fragments corresponding to the Grzegorczyk hierarchy;71
6.6;Models of E-PA;84
6.7;Exercises, historical comments and suggested further reading;90
7;Representation of Polish metric spaces;94
7.1;Representation of real numbers;94
7.2;Representation of complete separable metric (`Polish') spaces;98
7.3;Special representation of compact metric spaces;105
7.4;Fragments, exercises, historical comments and suggested further reading;111
8;Modified realizability;113
8.1;The soundness and program extraction theorems;113
8.2;Remarks on fragments of E-HA;121
8.3;Exercises, historical comments and suggested further reading;123
9;Majorizability and the fan rule;124
9.1;A syntactic treatment of majorization and the fan rule;124
9.2;Exercises, historical comments and suggested further reading;129
10;Semi-intuitionistic systems and monotone modified realizability;130
10.1;The soundness and bound extraction theorems;130
10.2;Fragments, exercises, historical comments and suggested further reading;138
11;Gödel's functional (`Dialectica') interpretation;140
11.1;Introduction;140
11.2;The soundness and program extraction theorems;144
11.3;Fragments, exercises, historical comments and suggested further reading;153
12;Semi-intuitionistic systems and monotone functional interpretation;156
12.1;The soundness and bound extraction theorems;156
12.2;Applications of monotone functional interpretation;161
12.3;Examples of axioms : Weak König's lemma WKL;164
12.4;WKL as a universal sentence ;171
12.5;Fragments, exercises, historical comments and suggested further reading;175
13;Systems based on classical logic and functional interpretation;177
13.1;The negative translation;177
13.2;Combination of negative translation and functional interpretation;179
13.3;Application: Uniform weak König's lemma UWKL;192
13.4;Elimination of extensionality;194
13.5;Fragments of (W)E-PA;202
13.6;The computational strength of full extensionality;205
13.7;Exercises, historical comments and suggested further reading;209
14;Functional interpretation of full classical analysis;212
14.1;Functional interpretation of full comprehension;212
14.2;Functional interpretation of dependent choice;219
14.3;Functional interpretation of arithmetical comprehension;222
14.4;Functional interpretation of (IPP) by finite bar recursion;226
14.5;Models of bar recursion;227
14.6;Exercises, historical comments and suggested further reading;232
15;A non-standard principle of uniform boundedness;235
15.1;The 01-boundedness principle;235
15.2;Applications of 01-boundedness;244
15.3;Remarks on the fragments E-GnA;250
15.4;Exercises, historical comments and suggested further reading;253
16;Elimination of monotone Skolem functions;255
16.1;Skolem functions of type degree 1 in fragments of finite type arithmetic;255
16.2;Elimination of Skolem functions for monotone formulas;259
16.3;The principle of convergence for bounded monotone sequences of real numbers (PCM);274
16.4;01-CA and 01-AC;277
16.5;The Bolzano-Weierstraß property for bounded sequences in Rd;281
16.6;Exercises, historical comments and suggested further reading;284
17;The Friedman A-translation;285
17.1;The A-translation;285
17.2;Historical comments and suggested further reading;289
18;Applications to analysis: general metatheorems I;290
18.1;A general metatheorem for Polish spaces;290
18.2;Applications to uniqueness proofs;295
18.3;Applications to monotone convergence theorems;302
18.4;Applications to proofs of contractivity;303
18.5;Remarks on fragments of T;304
18.6;Historical comments and suggested further reading;306
19;Case study I: Uniqueness proofs in approximation theory;307
19.1;Uniqueness proofs in best approximation theory;307
19.2;Best Chebycheff approximation I;313
19.3;Best Chebycheff approximation II;338
19.4;Best L1-approximation;358
19.5;Exercises, historical comments and suggested further reading;386
20;Applications to analysis: general metatheorems II;387
20.1;Introduction;387
20.2;Main results in the metric and hyperbolic case;401
20.3;The case of normed spaces;420
20.4;Proofs of theorems 17.35, 17.52 and 17.69;430
20.5;Further variations;441
20.6;Treatment of several metric or normed spaces X1…,Xn simultaneously;445
20.7;A generalized uniform boundedness principle -UBX;446
20.8;Applications of -UBX;451
20.9;Fragments of A[…];460
20.10;Exercises, historical comments and suggested further reading;462
21;Case study II: Applications to the fixed point theory of nonexpansive mappings;464
21.1;General facts;464
21.2;Applications of the metatheorems from chapter 17;470
21.3;Logical analysis of the proof of the Borwein-Reich-Shafrir theorem ;477
21.4;Asymptotically nonexpansive mappings;505
21.5;Applications of proof mining in ergodic theory;508
21.6;Exercises, historical comments and suggested further reading;510
22;Final comments;512
23;References;516
24;List of formal systems and term classes;533
25;List of axioms and rules;534
26;Index;536