Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach

• Authors: Pezlar Ivo
• Languages of publication: EN

Abstracts

EN

In this paper we examine two approaches to the formal treatment of the notion of problem in the paradigm of algorithmic semantics. Namely, we will explore an approach based on Martin-Löf’s Constructive Type Theory (CTT), which can be seen as a direct continuation of Kolmogorov’s original calculus of problems, and an approach utilizing Tichý’s Transparent Intensional Logic (TIL), which can be viewed as a non-constructive attempt of interpreting Kolmogorov’s logic of problems. In the last section we propose Kolmogorov and CTT-inspired modifications to TIL-based approach. The focus will be on non-empirical (i.e., mathematical and logical) problems only.

Keywords

EN

logic of problems; algorithmic semantics; procedural semantics; Constructive Type Theory; Transparent Intensional Logic

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2017
• Volume: 26
• Issue: 4
• Pages: 473–508

Dates

published

2017-12-15

Contributors

author

Pezlar Ivo

• Department of Philosophy, Masaryk University, Arna Nováka 1, Brno, Czech Republic

References

• Church, A., “A set of postulates for the foundation of logic”, Annals of Mathematics 33, 2 (1932): 346–366. DOI: 10.2307/1968337
• Church, A., “A formulation of the simple theory of types”, The Journal of Symbolic Logic 5, 6 (1940): 56–68. DOI: 10.2307/2266170
• Curry, H.B., and R. Feys, Combinatory Logic, volume 1 of “Combinatory Logic”, North-Holland Publishing Company, 1958.
• De Bruijn, N., “Automath, a language for mathematics”, Technical report, Department of Mathematics, Eindhoven University of Technology, 1968.
• Duží, M., and B. Jespersen, “Procedural isomorphism, analytic information and β-conversion by value”, Logic Journal of IGPL 21, 2 (2013): 291–308. DOI: 10.1093/jigpal/jzs044
• Duží, M., and P. Materna, “Can concepts be defined in terms of sets?”, Logic and Logical Philosophy 19, 3 (2010): 195–242. DOI: 10.12775/LLP.2010.008
• Duží, M., B. Jespersen, and P. Materna, Procedural Semantics for Hyperintensional Logic: Foundations and Applications of Transparent Intensional Logic, “Logic, Epistemology, and the Unity of Science”, Springer, 2010. DOI: 10.1007/978-90-481-8812-3
• Gentzen, G., “Untersuchungen über das logische Schließen. I”, Mathematische Zeitschrift 39, 1 (1935): 176–210. DOI: 10.1007/BF01201353
• Girard, J.-Y., Proofs and Types, “Cambridge Tracts in Theoretical Computer Science” 7, Cambridge University Press, 1989.
• Granström, J.G., Treatise on Intuitionistic Type Theory, “Logic, Epistemology, and the Unity of Science”, Springer Netherlands, 2011. DOI: 10.1007/978-94-007-1736-7
• Heyting, A., Intuitionism: An Introduction, “Studies in Logic and the Foundations of Mathematics”, North-Holland Pub. Co., 1956.
• Horák, A., Computer Processing of Czech Syntax and Semantics, Librix.eu, Brno, Czech Republic, 2008.
• Howard, W.A., “The formulae-as-types notion of construction”, pages 479–490 in J.R. Hindley and J.P. Seldin (eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980.
• Jespersen, B., and M. Carrara, “A new logic of technical malfunction”, Studia Logica 101, 3 (2013): 547–581.DOI: 10.1007/s11225-012-9397-8
• Kolmogorov, A.N., “Zur Deutung der intuitionistischenLogik”, Mathematische Zeitschrift 35, 1 (1932): 58–65. English translation in Tikhomirov 1991, pp. 151–158 and Mancosu 1998, pp. 328–334. DOI: 10.1007/BF01186549
• Kolmogorov, A.N., “Letters of A.N. Kolmogorov to A. Heyting”, Russian Mathematical Surveys 43, 6 (1988): 89–93. DOI: 10.1070/RM1988v043n06ABEH001986
• Kolmogorov, A.N., “On the interpretation of intuitionistic logic”, pages 151–158 in V.M. Tikhomirov (ed.), Selected Works of A.N. Kolmogorov, volume 25 of “Mathematics and Its Applications (Soviet Series)”, Springer Netherlands, 1991. DOI: 10.1007/978-94-011-3030-1_19
• Kovář, V., A. Horák, and M. Jakubíček, “How to analyze natural language with Transparent Intensional Logic?”, pages 69–76 in P. Sojka and A. Horák (eds.), Proceedings of Recent Advances in Slavonic Natural Language Processing, RASLAN 2010.
• Martin-Löf, P., “An intuitionistictheory of types: Predicative part”, pages 73–118 in H.E. Rose and J.C. Shepherdson (eds.), Logic Colloquium ’73Proceedings of the Logic Colloquium, volume 80 of “Studies in Logic and the Foundations of Mathematics”, Elsevier, 1975. DOI: 10.1016/S0049-237X(08)71945-1
• Martin-Löf, P., “Hauptsatz for the intuitionistic theory of iterated inductive definitions”, pages 197–215 in J.E. Fenstad (ed.), Proceedings of the Second Scandinavian Logic Symposium (Oslo 1970), North-Holland, 1971.
• Martin-Löf, P., “About models for intuitionistic type theories and the notion of definitional equality”, pages 81–109, North-Holland Publishing Company, 1975.
• Martin-Löf, P., “Constructive mathematics and computer programming”, pages 153–175 in J.L. Cohen and J. Łoś et al. (eds.), Logic, Methodology and Philosophy of Science VI, 1979, North-Holland, 1982.
• Martin-Löf, P., Intuitionistic Type Theory, “Studies in Proof Theory”, Bibliopolis, 1984.
• Materna, P., Concepts and Objects, Acta Philosophica Fennica, Helsinki: Philosophical Society of Finland, vol. 63, 1998.
• Materna, P., Conceptual Systems, Logische Philosophie Logos, 2004.
• Materna, P., “Ordinary modalities”, Logique et Analyse 48, 57–70 (2005): 513–554.
• Materna, P., “The notion of problem, intuitionism and partiality”, Logic and Logical Philosophy 17, 4 (2008): 287–303. DOI: 10.12775/LLP.2008.016
• Materna, P., “Mathematical and empirical concepts”, pages 209–233 in J. Maclaurin (ed.), Rationis Defensor, volume 28 of “Studies in History and Philosophy of Science”, Springer Netherlands, 2012. DOI: 10.1007/978-94-007-3983-3_16
• Materna, P., “Is Transparent Intensional Logic a non-classical logic?”, Logic and Logical Philosophy 23, 1 (2014): 47–55. DOI: 10.12775/LLP.2013.032
• Melikhov, S.A., “A galois connection between classical and intuitionistic logics. I: Syntax”, 2013.
• Moschovakis, Y.N., “A logical calculus of meaning and synonymy”, Linguistics and Philosophy 29, 1 (2006): 27–89. DOI: 10.1007/s10988-005-6920-7
• Muskens, R., “Sense and the computation of reference”, Linguistics and Philosophy 28, 4 (2005): 473–504. DOI: 10.1007/s10988-004-7684-1
• Nordström, B., K. Petersson, and J.M. Smith, Programming in Martin-Löf’s Type Theory: An Introduction, International series of monographs on computer science, Clarendon Press, 1990.
• Nordström, B., K. Petersson, and J M. Smith, Martin-Löf’s Type Theory. Handbook of Logic in Computer Science, Volume 5, “Logic and Algebraic Methods”, Oxford University Press, Oxford, 2001.
• Pierce, B.C., Types and Programming Languages, MIT Press, 2002.
• Primiero, G., and B. Jespersen, “Two kinds of procedural semantics for privative modification”, Lecture Notes in Artificial Intelligence 6284: 251–271, 2010. DOI: 10.1007/978-3-642-14888-0_21
• Raclavský, J., “On the interaction of semantics and deduction in Transparent Intensional Logic (Is Tichý’s logic a logic?)”, Logic and Logical Philosophy 23, 1 (2014): 57–68. DOI: 10.12775/LLP.2013.035
• Raclavský, J., and P. Kuchyňka, “Conceptual and derivation systems”, Logic and Logical Philosophy 20, 1–2 (2011): 159–174. DOI: 10.12775/LLP.2011.008
• Raclavský, J., P. Kuchyňka, and I. Pezlar, Transparent Intensional Logic as Characteristica Universalis and Calculus Ratiocinator (in Czech), Brno: Masaryk University (Munipress), Brno, 2015.
• Ranta, A., Type-Theoretical Grammar, Indices, Clarendon Press, 1994.
• Simmons, H., Derivation and Computation: Taking the Curry-Howard Correspondence Seriously, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2000.
• Sørensen, M.H., and P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Volume 149 of “Studies in Logic and the Foundations of Mathematic”, Elsevier Science Inc., New York, NY, USA, 2006.
• Stergios, Ch., and Z. Luo, Modern Perspectives in Type-Theoretical Semantics, Springer Publishing Company, Incorporated, 1st edition, 2017. DOI: 10.1007/978-3-319-50422-3
• Sundholm, G., “Constructions, proofs and the meaning of logical constants”, Journal of Philosophical Logic 12, 2 (1983): 151–172. DOI: 10.1007/BF00247187
• Thompson, S., Type Theory and Functional Programming, International computer science series, Addison-Wesley, 1999.
• Tichý, P., “Foundations of partial type theory”, Reports on Mathematical Logic 14 (1982): 59–72.
• Tichý, P., “Constructions”, Philosophy of Science 53, 4 (1986): 514–534.
• Tichý, P., “Indiscernibility of identicals”, Studia Logica 45, 3 (1986): 251–273. DOI: 10.1007/BF00375897
• Tichý, P., The Foundations of Frege’s Logic, Foundations of Communication, de Gruyter, 1988.
• Tichý, P., V. Svoboda, B. Jespersen, and C. Cheyne (eds.), Pavel Tichý’s Collected Papers in Logic and Philosophy, Filosofia, 2004.
• The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013. https://homotopytypetheory.org/book
• van Dalen, D., “Interpreting intuitionistic logic”, in P.C. Baayen, D. van Dulst, and J. Oosterhoff (eds.), Proceedings, Bicentennial Congress, Wiskundig Genootschap, Amsterdam: Mathematisch Centrum, 1979.
• van Heijenoort, J., From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Source Books in the History of the Sciences, Harvard University Press, 1977.
• Wadler, Ph., “Propositions as types”, Draft, 29 November 2014. http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
• Whitehead, A.N., and B. Russell, Principia Mathematica, Cambridge University Press, 1910.
• Więckowski, B., “Constructive belief reports”, Synthese 192, 3 (2015): 603–633. DOI: 10.1007/s11229-014-0540-0

Identifiers

DOI

10.12775/LLP.2017.010