Proof-theoretical analysis: Weak systems of functions and classes

DOI10.1016/0168-0072(88)90055-3zbMATH Open0697.03032OpenAlexW2074338252MaRDI QIDQ911585FDOQ911585

Authors: 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

Recommendations

• Provably recursive functions of constructive and relatively constructive theories
• An intuitionistic fixed point theory
• Proof-theoretic conservations of weak weak intuitionistic constructive set theories
• Minimal readability of intuitionistic arithmetic and elementary analysis
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. II

zbMATH Keywords

intuitionistic logiccut eliminationtransfinite inductionHeyting arithmeticconservation 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) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35)

Cites Work

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

Cited In (18)

• Levels of truth
• Notation systems for infinitary derivations
• Proof theory of constructive systems: inductive types and univalence
• Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees
• Generalizations of the one-dimensional version of the Kruskal-Friedman theorems
• Totality in applicative theories
• Metamathematical properties of a constructive multi-typed theory
• Generalizations of the Kruskal-Friedman theorems
• Title not available (Why is that?)
• Extended bar induction in applicative theories
• Title not available (Why is that?)
• A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
• EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY
• A Buchholz rule for modal fixed point logics
• Arithmetical conservation results
• Induction and inductive definitions in fragments of second order arithmetic
• Title not available (Why is that?)
• DIALOGUE THEORY OF PROOFS FOR ARITHMETIC, ANALYSIS, AND SET THEORY

This page was built for publication: Proof-theoretical analysis: Weak systems of functions and classes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q911585)