Comparing Sense and Denotation in Bilateralist Proof Systems for Proofs and Refutations

Abstract

In this paper a framework to distinguish in a Fregean manner between sense and denotation of \(\lambda\)-term-annotated derivations will be applied to a bilateralist sequent calculus displaying two derivability relations, one for proving and one for refuting. Therefore, a two-sorted typed \(\lambda\)-calculus will be used to annotate this calculus and a Dualization Theorem will be given, stating that for any derivable sequent expressing a proof, there is also a derivable sequent expressing a refutation and vice versa. By having joint \(\lambda\)-term annotations for proof systems in natural deduction and sequent calculus style, a comparison with respect to sense and denotation between derivations in those systems will be feasible, since the annotations elucidate the structural correspondences of the respective derivations. Thus, we will have a basis for determining in which cases, firstly, derivations expressing a proof vs. derivations expressing a refutation and, secondly, derivations in natural deduction vs. in sequent calculus can be identified and on which level.