Propositions vs. Problems
| Thesis title in Czech: | Propozice vs. problémy |
|---|---|
| Thesis title in English: | Propositions vs. Problems |
| Key words: | logika problémů|logika propozic|teorie typů|Curry-Howardova korespondence |
| English key words: | logic of problems|logic of propositions|type theory|Curry-Howard correspondence |
| Academic year of topic announcement: | 2023/2024 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Logic (21-KLOG) |
| Supervisor: | Mgr. Vít Punčochář, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 22.02.2024 |
| Date of assignment: | 23.02.2024 |
| Administrator's approval: | approved |
| Confirmed by Study dept. on: | 23.02.2024 |
| Submitted/finalized: | no |
| Guidelines |
| According to Kolmogorov, intuitionistic logic describes logical relations among problems rather than among propositions. Kolmogorov observed that one can construct complex problems from simpler ones by means of standard logical operators like conjunction or disjunction. This means that problems have logical forms and one can consider a notion of a valid form: a particular form of problems is valid iff there is a uniform method by which one can solve all instances of that form. Kolmogorov argued that this notion of validity coincides with intuitionistic validity. Intuitionistic logic is closely related to modern type theory via the Curry-Howard correspondence. This correspondence has led to the “Propositions as Types” paradigm according to which propositions can be identified with types of type theory. However, in the light of the Kolmogorov’s interpretation of intuitionistic logic, one could use the Curry-Howard correspondence to identify types with problems rather than propositions. The goal of this thesis is to compare these two alternative understandings of type theory (“Propositions as Types” vs. “Problems as Types”) and to formulate and analyse philosophical arguments in favour or against these views. |
| References |
| Awodey, S., Bauer, A. (2004). Propositions as [Types], Journal of Logic and Computation, 14, 447-447. Kolmogorov, A. (1932). Zur Deutung der Intuitionistischen Logik. Mathematische Zeitschrift, 35, 58-65. Martin-Löf. M. (1984). Intuitionistic Type Theory. Bibliopolis. Rodin, A. (2023). Kolmogorov's Calculus of Problems and Its Legacy. arXiv:2307.09202v1.https://doi.org/10.48550/arXiv.2307.09202 The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ: Institute for Advanced Study. Wadler, P. (2015). Propositions as Types, Communications of the ACM, 58, 75–84. |