Page 5 - Textos de Matemática Vol. 38

Contents
Preface ................................... v
Fernando Ferreira
Proof Interpretations 1
1 Firstlecture.............................. 1
1.1 Thelanguageoffinitetypearithmetic . . . . . . . . . . . 1
1.2 Heytingarithmeticinallfinitetypes . . . . . . . . . . . . 2
1.3 Combinatorialcompleteness................. 3
1.4 Mainmodels ......................... 4
2 Secondlecture ............................ 10
2.1 Modifiedrealizability..................... 10
2.2 Extraction, conservation and characterization for modi-
fiedrealizability ....................... 11
2.3 Boundedmodifiedrealizability ............... 13
2.4 Extraction, conservation and characterization for bounded
modifiedrealizability..................... 16
2.5 Benignprinciples....................... 17
3 Thirdlecture ............................. 19
3.1 G¨odel’sDialecticainterpretation . . . . . . . . . . . . . . 19
3.2 Negativetranslation ..................... 21
3.3 The no-counterexample interpretation . . . . . . . . . . . 23
3.4 Eliminationofextensionality ................ 24
3.5 FragmentsandParsons’result ............... 25
4 Fourthlecture............................. 27
4.1 Intensionalmajorizability .................. 27
4.2 Boundedfunctionalinterpretation . . . . . . . . . . . . . 28
4.3 Extraction and conservation for the bounded functional interpretation......................... 31
4.4 Uniformboundedness .................... 33
5 Coda.................................. 36
Annotatedbibliography .......................... 38 Acknowledgments.............................. 41
iii