scientific article; zbMATH DE number 3614784

Publication date: 1978

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Peano Arithmetic Type Theory Heyting Arithmetic Higher Order Arithmetic Intuitionistic Set Theory Provably Recursive Functions

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Recursive functions and relations, subrecursive hierarchies (03D20) Intuitionistic mathematics (03F55)

Related Items

On theorems of Gödel and Kreisel: Completeness and Markov's principle, A semantic approach to conservativity, A constructive valuation semantics for classical logic, A strong normalization result for classical logic, The Friedman‐Translation for Martin‐Löf's Type Theory, Fluctuations, effective learnability and metastability in analysis, Group completions and limit sets of Kleinian groups, Program extraction from classical proofs, Intrinsic theories and computational complexity, The Peirce translation, Core Gödel, Dialectica interpretation of well-founded induction, A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic, Satisfiability is false intuitionistically: a question from Dana Scott, AN ESCAPE FROM VARDANYAN’S THEOREM, The FAN principle and weak König's lemma in Herbrandized second-order arithmetic, Intermediate logics and the de Jongh property, Realizability algebras III: some examples, Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version, Classical realizability and arithmetical formulæ, CONSERVATION THEOREMS ON SEMI-CLASSICAL ARITHMETIC, Internal models of system F for decompilation, Proof-theoretical analysis: Weak systems of functions and classes, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, Automated Constructivization of Proofs, A Classical Sequent Calculus with Dependent Types, A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract), A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP, What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Verificationism and Classical Realizability, Induction, constructivity, and grounding, An intuitionistic version of Ramsey's theorem and its use in program termination, Axioms for control operators in the CPS hierarchy, Classical realizability in the CPS target language, The greatest common divisor: A case study for program extraction from classical proofs, Intuitionistic validity in \(T\)-normal Kripke structures, Programs from proofs using classical dependent choice, The computational content of arithmetical proofs, A realizability interpretation for classical analysis, Intuitionistic open induction and least number principle and the Buss operator, A complexity analysis of functional interpretations, Epistemic and intuitionistic formal systems, Refined program extraction from classical proofs, Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic, Pedagogical second-order \(\lambda \)-calculus, A New Translation for Semi-classical Theories — Backtracking without CPS, The metamathematics of ergodic theory, Intuitionistically provable recursive well-orderings, Not all Kripke models of \(\mathsf{HA}\) are locally \(\mathsf{PA}\), Dynamical algebraic structures, pointfree topological spaces and Hilbert's program. (Structures algébriques dynamiques, espaces topologiques sans points et programme de Hilbert), Large sets in intuitionistic set theory, PRENEX NORMAL FORM THEOREMS IN SEMI-CLASSICAL ARITHMETIC, Maximal ideals in countable rings, constructively, The lack of definable witnesses and provably recursive functions in intuitionistic set theories