Integrating classical and intuitionistic type theory (Q580341)

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 reflecting their characteristic features. (3) Certain problematic principles of intuitionism, which normally conflict with classical logic, are consistent with (EF), when appropriately formulated. In this paper, building on the ideas discussed above, we pursue the theme of integrating classical and intuitionistic mathematics in the setting of type theory. By `type theory' we understand the system of higher-order arithmetic in all finite types with full comprehension. Formal systems (IT), (TT), and (ET) for intuitionistic, classical and epistemic type theory are set up. The translation of \textit{S. Shapiro} [Intensional mathematics, Stud. Logic Found. Math. 113, 11-46 (1985; Zbl 0559.03036)] is extended to an interpretation, \((\cdot)^{\square}\), of (IT) into (ET). We observe that Funayama's Theorem is provable in (IT) and we apply it to the set of truth values. From this an interpretation, \((\cdot)^{\diamond}\), of (ET) into (IT) is constructed, which is in a certain sense inverse to \((\cdot)^{\square}\). This is applied to show that \((\cdot)^{\square}\) is faithful and consequently that (ET) is a conservative extension of (IT). We also describe a sound and faithful interpretation of (TT) into (ET). The existence and disjunction properties are extended to (ET), and, finally, we show Epistemic Church's Thesis is consistent with (ET).