Integrating classical and intuitionistic type theory

DOI10.1016/0168-0072(86)90042-4zbMATH Open0626.03049OpenAlexW2075853353MaRDI QIDQ580341FDOQ580341

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proof theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Epistemic arithmetic is a conservative extension of intuitionistic arithmetic
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (13)

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

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)