Proof-theoretical analysis: Weak systems of functions and classes

DOI10.1016/0168-0072(88)90055-3zbMath0697.03032OpenAlexW2074338252MaRDI QIDQ911585

L. N. Gordeev

Publication date: 1988

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(88)90055-3

zbMATH Keywords

cut eliminationHeyting arithmeticintuitionistic logictransfinite inductionconservation for arithmetic sentencesextensional type theory without universesFeferman style theory of functions and classesMyhill-Friedman style set theoryrestricted induction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items

Metamathematical properties of a constructive multi-typed theory, Totality in applicative theories, Levels of truth, Generalizations of the Kruskal-Friedman theorems, Arithmetical conservation results, EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY, A Buchholz rule for modal fixed point logics, A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP, Generalizations of the one-dimensional version of the Kruskal-Friedman theorems, Notation systems for infinitary derivations, Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees, Proof Theory of Constructive Systems: Inductive Types and Univalence, Extended bar induction in applicative theories

Cites Work

• Realizability and intuitionistic logic
• Goodman's theorem and beyond
• A majorizing semantics for hyperarithmetic sentences
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Set theoretic foundations for constructive analysis
• Finite investigations of transfinite derivations
• Untersuchungen über das logische Schliessen. I
• Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Beweistheoretische Untersuchung der verzweigten Analysis
• Constructive mathematics and computer programming
• Disjunctive properties of intuitionistic systems
• A simplification of the Bachmann method for generating large countable ordinals
• Constructive set theory
• Principles of continuous choice and continuity of functions in formal systems for constructive mathematics
• Relativized realizability in intuitionistic arithmetic of all finite types
• The faithfulness of the interpretation of arithmetic in the theory of constructions
• A survey of proof theory
• On the interpretation of non-finitist proofs–Part II
• Algebraische und logistische Untersuchungen über freie Verbände
• On the interpretation of intuitionistic number theory
• Proof theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item