Comparing Sense and Denotation in Bilateralist Proof Systems for Proofs and Refutations - Ayhan, Sara (Bulletin of the Section of Logic, 2025)
In this paper a framework to distinguish in a Fregean manner between sense and denotation of \(λ\)-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 \(λ\)-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 \(λ\)-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.