Realizability and intuitionistic logic

DOI10.1007/BF00485463zbMath0537.03043OpenAlexW4232423688MaRDI QIDQ792319

A. S. Troelstra, Justus Diller

Publication date: 1984

Published in: Synthese (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00485463

zbMATH Keywords

type theoryabstract realizabilityextensional realizabilityformulae-as-typesproof-interpretationproof-interpretation of intuitionistic logical operatorsrealizability interpretationstyped systems

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Metamathematics of constructive systems (03F50) Relative consistency and interpretations (03F25)

Related Items

The fundamental problem of general proof theory ⋮ Extensional realizability ⋮ A Comparison of Type Theory with Set Theory ⋮ Identity and sortals (and Caesar) ⋮ Proof-theoretical analysis: Weak systems of functions and classes ⋮ A light-weight integration of automated and interactive theorem proving ⋮ The seeming interdependence between the concepts of valid inference and proof ⋮ Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)

Uses Software

• Automath

Cites Work

• Intuitionism. An introduction
• Constructions, proofs and the meaning of logical constants
• Goodman's theorem and beyond
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• The Overlap of Random Particles and Similar Problems: Expressions for Variance of Coverage and its Analogue
• On the interpretation of intuitionistic number theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item