Page 8 - Textos de Matemática Vol. 40

vi
Contents
2
1.8.1 ThetheoryLFP........................ 45 1.8.2 Leastfixedpointoperator.................. 47 1.8.3 Discussion........................... 54
Explicit Mathematics 57
2.1 Explicitmathematics......................... 57 2.1.1 ThetheoryEETJ. ...................... 57 2.1.2 Elementarycomprehension. ................. 60 2.1.3 ProoftheoryofEETJ. .................... 61
2.2 Nameinduction............................ 61
2.2.1 ThetheoryNEM ....................... 62
2.2.2 AccessiblepartsinNEM................... 63
2.2.3 ModellingIDaccinNEM ................... 66 1
2.2.4 ModellingNEMinID1 .................... 67
2.3 Universesinexplicitmathematics.................. 70
2.3.1 The limit axiom and basic properties of universes . . . . . 71
2.3.2 ThetheoryT0. ........................ 76
2.3.3 Prooftheory. ......................... 77
2.3.4 Leastuniverses ........................ 77
2.3.5 Embedding of LUN within T0 + (Lim) + (LEM-UG) . . . . 82
2.3.6 Strictuniverses........................ 84
2.3.7 Nameinduction........................ 86
Truth Theories 89
3.1 Truththeoriesinthetotalsetting.................. 90 3.1.1 ThetheoryFON ....................... 90 3.1.2 Abstraction.......................... 92 3.1.3 Fixedpoints ......................... 94 3.1.4 Modelconstruction...................... 95 3.1.5 Prooftheory ......................... 97 3.1.6 Discussion........................... 98
3.2 Truththeoriesinthepartialsetting ................ 98 3.2.1 Ignoringundefinedterms .................. 99 3.2.2 Usingpointers ........................104
3.3 Streamsinscheme..........................108
3.4 UniversesoverFregestructures...................110 3.4.1 ThetheoryFSU .......................111 3.4.2 PropertiesofFSU ......................113 3.4.3 Hierarchiesofuniverses ...................116 3.4.4 Fixedpoints .........................118 3.4.5 EmbeddingsofIDα......................120 3.4.6 Theupperbounds ......................121
3.5 Supervaluation ............................132
3