Mathematical Intuitionism: Introduction to Proof Theory: Introduction to Proof TheoryAmerican Mathematical Soc., 31 dic 1988 - 228 páginas This monograph is intended to present the most important methods of proof theory in intuitionistic logic, assuming the reader to have mastered an introductory course in mathematical logic. The book starts with purely syntactical methods based on Gentzen's cut-elimination theorem, followed by intuitionistic arithmetic where Kleene's realizability method plays a central role. The author then studies algebraic models and completeness theorems for them. After giving a survey on the principles of intuitionistic analysis, the last part of the book presents the cut-elimination theorem in intuitionistic simple theory of types with an extensionality rule. |
Índice
Arithmetic | 23 |
Algebraic Models | 59 |
Analysis | 125 |
Eliminability of Cuts in the Intuitionistic Simple Theory | 153 |
Appendix A An Algebraic Approach to Models of Realizability Type | 173 |
Appendix B A Strong Form of the Normalization Theorem | 185 |
Bibliography | 201 |
| 217 | |
Otras ediciones - Ver todo
Mathematical Intuitionism: Introduction to Proof Theory Al'bert Grigor'evič Dragalin No hay ninguna vista previa disponible - 1979 |
Mathematical Intuitionism: Introduction to Proof Theory: Introduction to ... Al'bert Grigor'evi_ Dragalin No hay ninguna vista previa disponible - 1988 |
Términos y frases comunes
addition algebraic model arithmetic assertion Assume atomic formula axiom scheme Baire space basic formula BK-models classical complete consistent constant construction of go constructive functions contains define definition denote derivable in HPC derivation 1r disjunction Dragalin elements equivalent evaluated formula example exists fact figure find finite sequence first fix formula go function symbols G b1 GHPC given go(n IDB(U implies individual objects induction with respect inductive hypothesis interpretation intuitionistic analysis intuitionistic logic intuitionistic predicate intuitionistic theories Kleene and Vesley Kreisel Kripke frame Kripke model lemma Let us consider logical connectives Math mathematics natural numbers obtained operations parameters pr.r predicate logic predicate symbol premiss primitive recursive primitive recursive function principle proof properties propositional logic prove pseudo-Boolean algebra quantifiers realizability recursive function reduction rules of inference satisfies semantics sentence sequent calculus specific suffices term of type theorem topological model topological space Troelstra true verification