Relativized realizability in intuitionistic arithmetic of all finite types

DOI10.2307/2271946MaRDI QIDQ4177565zbMATH OpenOpenAlexFDO

Authors Nicolas D. Goodman

Publication date 1978

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2271946

zbMATH Keywords

Intuitionistic ArithmeticFinite TypesPartial Recursive FunctionsRelativized Realizability

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55)

Cited in

(16)

• Remarks on Herbrand normal forms and Herbrand realizations
• On Goodman realizability
• Proof theory of constructive systems: inductive types and univalence
• Relative and modified relative realizability
• A computational interpretation of forcing in type theory
• Extended bar induction in applicative theories
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY
• Proof-theoretical analysis: Weak systems of functions and classes
• A semantical proof of De Jongh's theorem
• Realizability Models Separating Various Fan Theorems
• On Relating Theories: Proof-Theoretical Reduction
• Arithmetical conservation results
• Quick cut-elimination for strictly positive cuts
• Generalizing realizability and Heyting models for constructive set theory
• Some results on cut-elimination, provable well-orderings, induction and reflection

This page was built for publication: Relativized realizability in intuitionistic arithmetic of all finite types

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