Integrating classical and intuitionistic type theory

DOI10.1016/0168-0072(86)90042-4zbMath0626.03049OpenAlexW2075853353MaRDI QIDQ580341

Robert C. Flagg

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

zbMATH Keywords

classical formalizationEpistemic Church's Thesisepistemic notionsepistemic type theoryFunayama's Theoremhigher-order arithmetic in all finite types with full comprehensionintuitionistic formalizationsynthesis of classical and constructive mathematics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Relative consistency and interpretations (03F25)

Related Items

Maximality in modal logic, Provability in principle and controversial constructivistic principles, Hypersequent calculi for intuitionistic logic with classical atoms, Reflecting in epistemic arithmetic, Epistemic and intuitionistic formal systems

Cites Work

• Epistemic arithmetic is a conservative extension of intuitionistic arithmetic
• Proof theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item