Integrating classical and intuitionistic type theory
type: Item
instance of: scholarly article
title: Integrating classical and intuitionistic type theory
zbMATH Open document ID: 0626.03049
DOI: 10.1016/0168-0072(86)90042-4
author: Robert C. Flagg
published in: Annals of Pure and Applied Logic
publication date: 1986-01-01T00:00:00Z
review text: Constructive assertions and arguments have begun to assume an increasing importance within classical mathematics. There are two standard ways in which these constructive assertions and arguments are understood. One way is to work within systems based on intuitionistic logic, thus giving an interpretation to the logical operations different from the classical one. Another approach is to stay within classical mathematics by giving some sort of set-theoretic interpretation to the epistemic notions involved. Both of these approaches suffer from certain defects. In the first, we are forced to abandon such powerful principles as the Law of Excluded Middle and the Axiom of Choice. Thus these principles cannot bear in any way on constructive problems. In the second approach the interpretations given to the epistemic notions are usually complex and nonintuitive, so they are somewhat difficult to work with. The need thus arises for the development of a simple conceptual framework extending classical mathematics and including certain features of intuitionistic mathematics. There are three natural conditions that such a framework should meet in order that it serve as a reasonable synthesis of classical and constructive mathematics. These are most easily stated in terms of a particular mathematical theory which has a classical formalization (CF) and an intuitionistic formalization (IF). We would then like to have a new formal system (EF) satisfying: (1) There is an interpretation \((\cdot)^{\square}\) of (IF) into (EF) and an interpretation \((\cdot)^ !\) of (CF) into (EF), both of which are sound and faithful: for each sentence \(\sigma\) of (IF), \(\vdash_{EF}\sigma^{\square}\) if and only if \(\vdash_{IF}\sigma\); and for each sentence \(\sigma\) of (CF), \(\vdash_{EF}\sigma^ !\) if and only if \(\vdash_{CF}\sigma.\) (2) In (EF) there are available (definable) operators corresponding to both the intuitionistic and classical logical operators and possessing properties reflecti…
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03F25
zbMATH DE Number: 4016900
zbMATH Keywords: epistemic type theory
zbMATH Keywords: epistemic notions
zbMATH Keywords: synthesis of classical and constructive mathematics
zbMATH Keywords: classical formalization
zbMATH Keywords: intuitionistic formalization
zbMATH Keywords: higher-order arithmetic in all finite types with full comprehension
zbMATH Keywords: Funayama's Theorem
zbMATH Keywords: Epistemic Church's Thesis
MaRDI profile type: Publication
full work available at URL: 0168-0072(86)90042-4
OpenAlex ID: W2075853353
cites work: Q3214890
cites work: Q4726244
cites work: Epistemic arithmetic is a conservative extension of intuitionistic arithmetic
cites work: Q3671978
cites work: Q4145861
cites work: Q5623688
cites work: Q3720593
cites work: Q3214891
cites work: Q3347874
cites work: Proof theory
description: scientific article; zbMATH DE number 4016900