The Concept of Proof in the Context of a Type-Theoretic Approach, III: Proofs as (Some) Types

The article is the third part of a study of the epistemological features of the concept of proof within the framework of a type-theoretic approach. The article discusses issues related to the concept of proof from the point of view of the classical version of the "propositions-as-types" doctrine (the Curry-Howard correspondence) and the modern version of the "propositions-as-some-types" doctrine (a version of the Curry-Howard correspondence from the point of view of homotopy type theory). This topic was partially discussed in the previous article. This article highlights a number of important aspects and nuances, examines the current state of research, and offers some epistemological conclusions. The Curry-Howard correspondence is a non-trivial connection between logic and typed computations. The semantics for intuitionistic logic according to the BHK-interpretation is traditionally given in terms of proofs. A statement is considered true if there is an evidence for it, and is considered false if there is a refutation for it. The BHK-interpretation allows us to talk about the dynamics and statics of proof. The type-theoretic approach is a variant of the interpretation of logical concepts and, accordingly, a new look at logic. This approach allows one to discover a certain kind of a "vertical unity" of logic. An updated view of the relationship between logic, typed lambda calculus, and category theory can be termed the doctrine of "propositions-as-some-types". Propositions are considered as types of a strictly defined type, while other types are not directly considered as propositions. This point of view can be illustrated by referring, for example, to the internal logic of topos or to homotopy type theory. The "propositions-as-types" doctrine assumes that every proposition corresponds to some type, and the proofs of a given proposition correspond to terms of that type. The situation is different with the understanding of logic within the framework of the "propositions-as-some-types" doctrine. Homotopy type theory offers some clarification of the status of logic and its concepts. Terms related to a certain type are still understood as different proofs (or rather objects-proofs), and differences between them can be easily abstracted away. The level of "pure" logic in the homotopy hierarchy is limited to -1 level, and logic becomes a "special case of geometry". This reduction is possible thanks to the powerful concept of identity. At the level of "pure" logic, there are rules for introduction and elimination, and, at higher levels, at which types are understood as fundamental groupoids, there are rules for constructing mathematical structures that lie outside of "pure" logic. Type theory is a more powerful tool for analyzing the concept of proof than traditional "pure" logic, which allows one to build systems for automatic and interactive proofs, much closer to ordinary mathematical proofs and mathematical intuition.

Keywords

Authors

References