Integrating classical and intuitionistic type theory
From MaRDI portal
Publication:580341
DOI10.1016/0168-0072(86)90042-4zbMath0626.03049MaRDI QIDQ580341
Publication date: 1986
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0168-0072(86)90042-4
classical formalization; Epistemic Church's Thesis; epistemic notions; epistemic type theory; Funayama's Theorem; higher-order arithmetic in all finite types with full comprehension; intuitionistic formalization; synthesis of classical and constructive mathematics
03B45: Modal logic (including the logic of norms)
03F35: Second- and higher-order arithmetic and fragments
03F50: Metamathematics of constructive systems
03F25: Relative consistency and interpretations
Related Items
Reflecting in epistemic arithmetic, Epistemic and intuitionistic formal systems, Hypersequent calculi for intuitionistic logic with classical atoms, Maximality in modal logic, Provability in principle and controversial constructivistic principles
Cites Work