Composition of Deductions within the Propositions-As-Types Paradigm
- PDF / 330,699 Bytes
- 13 Pages / 439.37 x 666.142 pts Page_size
- 12 Downloads / 148 Views
Logica Universalis
Composition of Deductions within the Propositions-As-Types Paradigm Ivo Pezlar Abstract. Kosta Doˇsen argued in his papers Inferential Semantics Doˇsen (in Inferential semantics, Springer, Berlin 2015) and On the Paths of Categories Doˇsen (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ˇsen 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. Mathematics Subject Classification. Primary 03F03; Secondary 03B40, 03B15. Keywords. General proof theory, propositions as types, Curry–Howard isomorphism, constructive type theory, categorial proof theory, Cut rule, composition of deduction.
1. Introduction and Motivation Kosta Doˇsen argued in his papers Inferential Semantics [7] and On the Paths of Categories [8] that the propositions-as-types paradigm (see, e.g., [33]) based on the Curry–Howard isomorphism is less suited for general proof theory because—unlike proof theory based on category theory—it makes prominent categorical proofs over hypothetical inferences. One specific instance of this, Doˇsen points out, is that the Curry–Howard isomorphism makes the associativity of deduction composition invisible. This is surprising, because both approaches are known to be equivalent (see [14,15]). We will examine Doˇsen’s claims and argue that approaches based on the Curry–Howard isomorphism Work on this paper was supported by Grant No. 19-12420S from the Czech Science Founˇ dation, GA CR.
I. Pezlar
Log. Univers.
do not necessarily favor proofs over inferences and that the associativity of deduction composition does not need to become hidden. This paper is structured as follows: first, we will briefly introduce notions relevant to our investigation (Sect. 2), then we will examine Doˇsen’s main argument and offer a counterproposal on how to deal with the composition of deductions within the propositions-as-types paradigm while keeping the associativity visible (Sect. 3).
2. Preliminary Notes We start with a short overview of the key vocabulary of this paper: General proof theory. An approach to proof theory proposed by [26] that views proofs themselves as the primary object of study. Proofs are no longer seen as just a formal device for studying logical consequence but as a subject matter worthy of its own philosophical investigation. See also [13]. Propositions-as-types paradigm A family of approaches based on the Brouwer– Heyting–Kolmogorov (BHK) interpretation of logical connectives and on the identification of propositions and types, also known as the Curry–Howard isomorphism or correspondence, initially observed by [4,10].1 In its simplest form, it refers to the correspondence between the implicational fragment of intuitionistic natural deduction and typed λ-calculus:
Data Loading...
