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

Ivo Pezlar

doi:10.12775/LLP.2017.010

Authors

Ivo Pezlar Masaryk University

DOI:

https://doi.org/10.12775/LLP.2017.010

Keywords

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

Abstract

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.

Author Biography

Ivo Pezlar, Masaryk University

Department of Philosophy

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