Propositions vs. Problems
| Název práce v češtině: | Propozice vs. problémy |
|---|---|
| Název v anglickém jazyce: | Propositions vs. Problems |
| Klíčová slova: | logika problémů|logika propozic|teorie typů|Curry-Howardova korespondence |
| Klíčová slova anglicky: | logic of problems|logic of propositions|type theory|Curry-Howard correspondence |
| Akademický rok vypsání: | 2023/2024 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra logiky (21-KLOG) |
| Vedoucí / školitel: | Mgr. Vít Punčochář, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 22.02.2024 |
| Datum zadání: | 23.02.2024 |
| Schválení administrátorem: | bylo schváleno |
| Datum potvrzení stud. oddělením: | 23.02.2024 |
| Odevzdaná/finalizovaná: | ne |
| Zásady pro vypracování |
| 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. |
| Seznam odborné literatury |
| 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. |