Abstract
Kosta Došen argued in his papers Inferential Semantics Došen (in Inferential semantics, Springer, Berlin 2015) and On the Paths of Categories Došen (in On the paths of categories, Springer, Cham 2016) that the propositions-as-types paradigm is less suited for general proof theory because—unlike proof theory based on category theory—it emphasizes categorical proofs over hypothetical inferences. One specific instance of this, Došen points out, is that the Curry–Howard isomorphism makes the associativity of deduction composition invisible. We will show that this is not necessarily the case.
Similar content being viewed by others
Notes
There were, however, other crucial contributors as well, most importantly N. G. de Bruijn and Per Martin-Löf.
Došen uses them interchangeably; see e.g., [7], p. 149.
In compliance with the rejection of Schroeder-Heister’s first dogma of standard semantics (the priority of categorical over the hypothetical, see [30]).
In CTT, \(A \supset B\) is defined via the \(\Pi \) type, i.e., the type of dependent functions, specifically as \((\Pi x : A)B\) where B does not depend on x.
It is difficult to surmise who was the first to suggest this reduction, however, it appears as early as the 17th century in the book Artis Logicae Compendium by Henry Aldrich (1648–1710) and the general idea was around probably even earlier.
See [30].
Frege’s unpublished manuscript Boole’s Logical Calculus and the Concept-Script.
It is rather the other way around since the conclusion b(x) : B clearly displays its dependence on the variable x from the hypothesis.
Since it should be always clear from the context, we are overloading the symbol ‘\(\circ \)’ to mean any kind of composition, i.e., categorial, type-theoretical, or functional.
I am indebted to Ansten Klev, who pointed this out to me and suggested a remedy utilizing the higher-order presentation of CTT presented below.
See [21], p. 143.
References
Boole, G.: An Investigation of the Laws of Thought. Walton & Maberly, London (1854)
Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2–3), 95–120 (1988)
Curien, P.-L., Garner, R., Hofmann, M.: Revisiting the categorical interpretation of dependent type theory. Theor. Comput. Sci. 546, 99–119 (2014)
Curry, H.B., Feys, R.: Combinatory Logic, Volume 1 of Combinatory Logic. North-Holland Publishing Company, Amsterdam (1958)
Došen, K.: Deductive completeness. Bull. Symbol. Logic 2(3), 243–283 (1996)
Došen, K.: Abstraction and application in adjunction. In: Kadelburg, Z. (ed.), Proceedings of the Tenth Congress of Yugoslav Mathematicians, Faculty of Mathematics, pages 33–46, Belgrade. University of Belgrade (2001)
Došen, K.: Inferential semantics. In: Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning, pp. 147–162. Springer, Berlin (2015)
Došen, K.: On the paths of categories. In: Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics, pp. 65–77. Springer, Cham (2016)
Frege, G.: Posthumous Writings. Wiley, New York (1979)
Howard, W.A.: The formulae-as-types notion of construction. In: Curry, H.B., Hindley, J.R., Seldin, J.P. (eds.) To H.B. Curry: Essays on CombinatoryLogic, Lambda Calculus, and Formalism. Academic Press, Cambridge (1980)
Klev, A.: A comparison of type theory with set theory. In: Centrone, S., Kant, D., Sarikaya, D. (eds.) Reflections on the Foundations of Mathematics. Springer, Cham (2019)
Klev, A.: Name of the Sinus Function. In: Sedlár, I., Blicha, M. (eds.) The Logica Yearbook 2018. College Publications, London (2019)
Kreisel, G.: A survey of proof theory II. In: Renstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 109–170. North-Holland, Amsterdam (1971)
Lambek, J.: Functional completeness of cartesian categories. Ann Math Logic 6(3–4), 259–292 (1974)
Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge (1986)
Luo, Z.: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1990)
Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Clarendon Press, Oxford (1994)
Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Rose, H.E., Shepherdson, J.C. (eds.), Logic Colloquium ’73 Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. Elsevier (1975)
Martin-Löf, P.: Intuitionistic type theory. Studies in proof theory. Bibliopolis (1984)
Negri, S., von Plato, J., Ranta, A.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory: An Introduction. International Series of Monographs on Computer Science. Clarendon Press, Oxford (1990)
Nordström, B., Petersson, K., Smith, J.M.: Martin-Löf’s type theory, Handbook of Logic in Computer Science: Volume 5: Logic and Algebraic Methods. Oxford University Press, Oxford (2001)
Pezlar, I: Towards a More General Concept of Inference. Logica Universalis 8(1), (2014)
Pezlar, I.: The Placeholder View of Assumptions and the Curry-Howard Correspondence. Synthese (2020)
Prawitz, D.: Natural Deduction: A Proof-theoretical Study. Dover Books on Mathematics Series. Dover Publications, Mineola (1965)
Prawitz, D.: The Philosophical Position of Proof Theory. In: Olson, R.E., Paul, A.M. (eds.) Contemporary Philosophy in Scandinavia, page 123–134. John Hopkins Press, Baltimore (1972)
Rahman, S., McConaughey, Z., Klev, A., Clerbout, N.: A brief introduction to constructive type theory. In: Immanent Reasoning or Equality in Action, pages 17–55. Springer, Cham (2018)
Ryle, G.: The Concept of Mind. University of Chicago Press, Chicago (1949)
Whatley, R.: Elements of Logic. Printed for J. Mawman, London (1827)
Schroeder-Heister, P.: The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics. Synthese 187(3), 925–942 (2012)
Seely, R.A.G.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philosoph. Soc. 95(1), 33 (1984)
Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, Institute for Advanced Study (2013)
Wadler, P.: Propositions as Types. Commun. ACM 58(12), 75–84 (2015)
Acknowledgements
An earlier version of this paper was presented at a seminar organized by the Department of Logic of the Institute of Philosophy (The Czech Academy of Sciences) in Prague, February 2019. I would like to thank all the participants of this seminar for their helpful notes. A special thanks goes to Ansten Klev, whose valuable remarks helped to shape this paper.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Work on this paper was supported by Grant No. 19-12420S from the Czech Science Foundation, GA ČR.
Rights and permissions
About this article
Cite this article
Pezlar, I. Composition of Deductions within the Propositions-As-Types Paradigm. Log. Univers. 14, 481–493 (2020). https://doi.org/10.1007/s11787-020-00260-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11787-020-00260-3
Keywords
- General proof theory
- propositions as types
- Curry–Howard isomorphism
- constructive type theory
- categorial proof theory
- Cut rule
- composition of deduction