Logical Frameworks for Truth and Abstraction (eBook)

Front Cover 1
Logical Frameworks for Truth and Abstraction: An Axiomatic Study 4
Copyright Page 5
Contents 10
Preface 6
Introduction 14
Part A: Combinators and Truth 24
Chapter I. Introducing operations 26
1. The basic language 27
2. Operations I: general facts 28
3. Operations II: elementary recursion theory 31
4A. The Church-Rosser theorem 35
4B. Term models 39
5. The graph model 41
6. An effective version of the extensional model D 47
Appendix 52
Chapter II. Extending operations with reflective truth 56
7. Extending combinatory algebras with truth 58
8. The theory of operations and reflective truth: simple consequences 64
9A. Type-free abstraction, predicates and classes 68
9B. Operations on predicates and classes 72
10A. The fixed point theorem for predicates 76
10B. Applications to semantScs and recursion theory 81
11. Non-extensionality 86
Appendix I: a property theoretic definition of the fixed point operator for predicates 89
Appendix II: on the explicit abstraction theorem 90
Appendix III: independence of truth predicates from the encoding of logical operators 93
Part B: Truth and recursion Theory 96
Chapter III. Inductive models and definability theory 98
12. Inductive models and the induction theorem 99
13. The envelope of an inductive model 101
14. The uniform ordinal comparison theorem for inductive models 104
15. Applications of the uniform ordinal comparison theorem 110
Chapter IV. Type-free abstraction with approximation operator 116
16. Approximating properties by classes 117
17. The approximation theorem for extensional operations and the fixed point theorem for monotone operations 122
18. Topology displayed: basic definitions 126
19. The representation theorem for explicitly CL-continuous operators 130
Appendix: alternative proofs 135
Chapter V. Type-free abstraction, choice and sets 138
20. Choice principles and the distinction between operations and functions 139
21. Admissible hulls: elementary facts 144
22. A model of admissible set theory 150
23. The boundedness theorem 157
Part C: Selected Topics 162
Chapter VI. Levels of implication and intensional logical equivalence 164
24. Myhill's levels of implication 165
25. Formal deducibility based on levels of implication and its proof-theoretic strength 171
26. Introducing an intensional equivalence relation 175
27. The infinitary reduction relation 178
28. The Church-Rosser theorem for 182
29. A model of type-free logic based on intensional equivalence 187
Chapter VII. On the global structure of models for reflective truth 190
30. The lattice of fixed point models for the neutral minimal theory 192
31. The sublattice of intrinsic fixed point models and the cardinality theorem 199
32. Variations on the encoding technique: non-modularity and other oddities 205
33. A model for an impredicative extension of reflective truth 211
34. On Kripke's classification of self-referential sentences 216
35. On the consistency of coinduction principles 220
Appendix: a variant to the basic operator F and the restriction axiom 222
Part D: Levels of Truth and Proof Theory 226
Chapter VIII. Levels of reflective truth 228
36. A language and axioms for reflective truth with levels 231
37. Simple consequences 233
38. Universes and the Weyl extended iteration principle 238
39. A recursion-theoretic model 243
40. Levels of truth and predicatively reducible subsystems of second-order arithmetic 251
41. Consistency of a reducibility principle for classes 257
42. Levels of truth and impredicative subsystems of second-order arithmetic 261
Appendix. on projectibility and stronger reflection 266
Chapter IX. Levels of truth and predicative well-orderings 270
43. On well-orderings 271
44. Ramified hierarchies 274
45. Predicative well-orderings I 282
46. Predicative well-orderings II 290
Chapter X. Reducing reflective truth with levels to finitely iterated reflective truth 298
47. A sequent calculus STLR for a theory of reflective truth with levels 299
48. Basic properties of STLR 304
49A. Elimination of the full level induction schema 306
49B. Elimination of unbounded level quantifiers 310
50. The infinitary sequent calculus IT~n of n-iterated reflective truth 316
51. Embedding STLR n into IT~n 318
Chapter XI. Proof-theoretic investigation of finitely iterated reflective truth 324
52. The ramified system RSn 325
53. Cut elimination 329
54. Some derivable sequents of RS n 333
55. Embedding ITn ~n into RS n 337
56. The upper bound theorem for IT~n 340
57. Upper bound theorems for TLR and its subsystems 342
58. Conclusion: the conservation theorems 348
Appendix. primitive recursive cut elimination for RS n 351
Part E: Alternative Views 362
Chapter XII. Non-reductive systems for type-free abstraction and truth 364
59. The core system VF- and transfinite induction 365
60. Supervaluation models of VF- 370
61. An abstract sequent calculus and truth 371
62. Cut elimination and related properties 377
63. A provability interpretation and the upper bound theorem 382
64. Reconciling supervaluation models with provability interpretation 388
Chapter XIII. The variety of non-reductive approaches 392
65. An inconsistency 393
66. On a truth theory of Friedman and Sheard 396
67. Fitch's models 399
68. Introducing semi-inductive definitions 403
69. Semi-inductive models for reflective truth 407
Chapter XIV. Epilogue. applications and perspectives 414
70A. A logical theory of constructions: informal motivations 415
70B. A logical theory of constructions: basic syntax 416
71. Axioms for the computation relations 420
72. Extending the logical theory of constructions with higher reflection 424
73. Proof-theoretic reduction 429
74. Perspectives. related work in Artificial Intelligence and Theoretical Linguistics 432
75. Sense and denotation as algorithm and value: subsuming theories of reflective truth under abstract recursion theory 435
Bibliography 438
Index 454
List of Symbols 466