scientific article; zbMATH DE number 1215498

zbMath0911.03031MaRDI QIDQ4215635

A. S. Troelstra

Publication date: 27 April 1999

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

zbMATH Keywords

intuitionistic arithmeticfunctional interpretationconstructive semanticsabstract realizabilityrealizability interpretationintuitionistic higher order systemsnumerical realizability

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) First-order arithmetic and fragments (03F30) Other constructive mathematics (03F65) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Related Items (29)

Algebraic proofs of cut elimination ⋮ Unnamed Item ⋮ A constructive game semantics for the language of linear logic ⋮ Realizability for Peano arithmetic with winning conditions in HON games ⋮ Intuitionistic completeness of first-order logic ⋮ Arithmetical conservation results ⋮ EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY ⋮ Choice and independence of premise rules in intuitionistic set theory ⋮ Mining the surface: witnessing the low complexity theorems of arithmetic ⋮ Revisiting the conservativity of fixpoints over intuitionistic arithmetic ⋮ On the independence of premiss axiom and rule ⋮ The Logic of Justification ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Primitive recursive selection functions for existential assertions over abstract algebras ⋮ Verificationism and Classical Realizability ⋮ Functional interpretations of linear and intuitionistic logic ⋮ Aspects of predicative algebraic set theory. II: Realizability ⋮ Uniform Heyting arithmetic ⋮ Realizability models refuting Ishihara's boundedness principle ⋮ Strongly uniform bounds from semi-constructive proofs ⋮ Logical problems of functional interpretations ⋮ Analyzing realizability by Troelstra's methods ⋮ A game-semantic model of computation ⋮ Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) ⋮ Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe ⋮ Saturated models of universal theories ⋮ On measure quantifiers in first-order arithmetic ⋮ Mathematics based on incremental learning -- excluded middle and inductive inference

This page was built for publication: