Theory of proofs (arithmetic and analysis)

DOI10.1007/BF01084980zbMath0413.03031OpenAlexW2080849083MaRDI QIDQ1260035

Grigori Mints

Publication date: 1975

Published in: Journal of Soviet Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01084980

zbMATH Keywords

surveycalculi of sequentsfunctional interpretation of classical analysisnormalization of higher order logic

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Functionals in proof theory (03F10)

Cites Work

• A characterization of the Veblen-Schütte functions by means of functionals
• Some problems of completeness of arithmetic
• A new concept of predicative truth and definability
• Consistency proofs of subsystems of classical analysis
• Cut elimination theorem for second order arithmetic with the \(\Pi^ 1_ 1\)-comprehension axiom and the \(\omega\)-rule
• A proof of cut-elimination theorem in simple type-theory
• Combinators, \(\lambda\)-terms and proof theory
• Proof theory and intuitionistic systems
• Ein syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die intuitionistische Typenlogik
• Ein starker Normalisationssatz für die intuitionistische Typentheorie
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• The correspondence between cut-elimination and normalization
• Disjunctive properties of intuitionistic systems
• Über zwei Bezeichnungssysteme für Ordinalzahlen
• Redundancies in the Hilbert-Bernays derivability conditions for Gödel's second incompleteness theorem
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Vergleich zweier Bezeichnungssysteme für Ordinalzahlen
• The faithfulness of the interpretation of arithmetic in the theory of constructions
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• Systems of predicative analysis, II: Representations of ordinals
• Intensional interpretations of functionals of finite type I
• Completeness and Hauptsatz for second order logic1
• A survey of proof theory
• Formalized recursive functionals and formalized realizability
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Formal systems for some branches of intuitionistic analysis
• Simultane Rekursionen in der Theorie der Funktionale endlicher Typen
• Induction and transfinite induction in intuitionistic systems
• A characterization of Takeuti's ordinal diagrams of finite order
• A Formally Constructive Model for Barrecursion of Higher Types
• On barinduction of higher types for decidable predicates
• Beweistheoretische Charakterisierung einer Erweiterung der Grzegorczyk-Hierarchie
• A Note on Indicator-Functions
• A system of abstract constructive ordinals
• On n-quantifier induction
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item