Integrating classical and intuitionistic type theory (Q580341): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
Property / 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 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). | |||
Property / 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 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). / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F50 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F35 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B15 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B45 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F25 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 4016900 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
epistemic type theory | |||
Property / zbMATH Keywords: epistemic type theory / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
epistemic notions | |||
Property / zbMATH Keywords: epistemic notions / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
synthesis of classical and constructive mathematics | |||
Property / zbMATH Keywords: synthesis of classical and constructive mathematics / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
classical formalization | |||
Property / zbMATH Keywords: classical formalization / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
intuitionistic formalization | |||
Property / zbMATH Keywords: intuitionistic formalization / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
higher-order arithmetic in all finite types with full comprehension | |||
Property / zbMATH Keywords: higher-order arithmetic in all finite types with full comprehension / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
Funayama's Theorem | |||
Property / zbMATH Keywords: Funayama's Theorem / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
Epistemic Church's Thesis | |||
Property / zbMATH Keywords: Epistemic Church's Thesis / rank | |||
Normal rank |
Revision as of 18:38, 1 July 2023
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Integrating classical and intuitionistic type theory |
scientific article |
Statements
Integrating classical and intuitionistic type theory (English)
0 references
1986
0 references
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).
0 references
epistemic type theory
0 references
epistemic notions
0 references
synthesis of classical and constructive mathematics
0 references
classical formalization
0 references
intuitionistic formalization
0 references
higher-order arithmetic in all finite types with full comprehension
0 references
Funayama's Theorem
0 references
Epistemic Church's Thesis
0 references