Integrating classical and intuitionistic type theory

DOI10.1016/0168-0072(86)90042-4MaRDI QIDQ580341zbMATH OpenOpenAlexFDO

Authors 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) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35) Relative consistency and interpretations (03F25)

Recommendations

• Epistemic and intuitionistic formal systems
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Epistemic set theory is a conservative extension of intuitionistic set theory
• scientific article; zbMATH DE number 1302061
• Interpreting classical theories in constructive ones

Cites work

• scientific article; zbMATH DE number 3427308 (Why is no real title available?)
• scientific article; zbMATH DE number 3427309 (Why is no real title available?)
• scientific article; zbMATH DE number 3891353 (Why is no real title available?)
• scientific article; zbMATH DE number 3825806 (Why is no real title available?)
• scientific article; zbMATH DE number 3950520 (Why is no real title available?)
• scientific article; zbMATH DE number 3574077 (Why is no real title available?)
• scientific article; zbMATH DE number 3999912 (Why is no real title available?)
• scientific article; zbMATH DE number 3348101 (Why is no real title available?)
• Epistemic arithmetic is a conservative extension of intuitionistic arithmetic
• Proof theory

Cited in

(13)

• DIALOGUE THEORY OF PROOFS FOR ARITHMETIC, ANALYSIS, AND SET THEORY
• Propositional forms of judgemental interpretations
• Classical truth in higher types
• scientific article; zbMATH DE number 3841847 (Why is no real title available?)
• Reflecting in epistemic arithmetic
• A strong multi-typed intuitionistic theory of functionals
• Proof-theoretic semantics for classical mathematics
• Hypersequent calculi for intuitionistic logic with classical atoms
• scientific article; zbMATH DE number 1746890 (Why is no real title available?)
• Maximality in modal logic
• Epistemic and intuitionistic formal systems
• Provability in principle and controversial constructivistic principles
• Combining Classical and Intuitionistic Implications

This page was built for publication: Integrating classical and intuitionistic type theory

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