Composition of deductions within the propositions as types paradigm

Plakát ke stažení

Kosta Došen argued in his papers Inferential Semantics (2015) and On the Paths of Categories (2016) that the propositions as types paradigm 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šen points out, is that the Curry-Howard isomorphism makes the associativity of deduction composition invisible. We will argue that this is not necessarily the case.