scientific article; zbMATH DE number 1215498

From MaRDI portal
Publication:4215635

zbMath0911.03031MaRDI QIDQ4215635

A. S. Troelstra

Publication date: 27 April 1999


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



Related Items

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