Publication details
Type-Theoretical Approaches to Problems and Solutions
| Authors | |
|---|---|
| Year of publication | 2015 |
| Type | Appeared in Conference without Proceedings |
| MU Faculty or unit | |
| Citation | |
| Description | We examine two possible approaches to the formal treatment of the notion of problem in the type-theoretical paradigm. More specifically, we will explore an approach put forward by Martin-Löf's Constructive Type Theory (abbr. CTT, based on BHK interpretation of intuitionistic logic and Curry-Howard-de Bruijn correspondence), which can be seen as a direct continuation of Kolmogorov's original calculus of problems, and an approach put forward by Materna utilizing Tichý's Transparent Intensional Logic (abbr. TIL, based on partial lambda calculus and ramified classical type theory), which can be viewed as a realist attempt of interpreting Kolmogorov's logic of problems. Thus both of these theories can be seen as building upon Kolmogorov's first key insight that (constructive) logic is better understood as dealing with problems rather than with propositions. We conclude that neither of these theories can be considered at their current state as providing satisfactory account of the notion of problem. CTT due to its insufficient treatment of empirical problems (specifically, it is unclear how to apply the concepts of canonical and non-canonical proofs in the realm of empirical discourse). TIL due to its incomplete analysis of non-empirical problems (specifically, its inability to track, and thus distinguish different logical proofs). We propose our own approach called Transparent Intensional Logic of Problems (abbr. TILP, an extension based on modified TIL emulating some of the properties of CTT) that tries to combine strengths of both approaches without retaining any of their weak points. Further, TILP can be seen as building upon Kolmogorov's second (and often neglected) key insight that (constructive) logic is best understood as dealing with both problems and propositions, but without conflating them together. |
| Related projects: |