Obstacles of a truly bilateral sequent calculus
Sara Ayhan
In proof-theoretic semantics it is assumed that the meaning of logical connectives is given by the rules of inference governing them in some underlying proof system. A bilateralist take on this can be understood as demanding of a proof system to display not only rules giving the connectives’ provability conditions but also their refutability conditions. Thus, with such an approach the bilateralism is implemented on the level of derivability, i.e., our proof system is bilateral by displaying two derivability relations, one for proving and one for refuting. While in natural deduction this seems rather straightforwardly feasible by dualizing proof rules (see, e.g., [1]), in a sequent calculus this does not seem trivially realizable. After all, here two derivability relations are inherent: one within sequents expressed by the sequent sign and one between sequents expressed by the horizontal lines. So, it seems that if we are serious about having a bilateral sequent calculus, both relations need to be dualized.
I will show, however, that in such a setting an apparent asymmetry between the notions of proof and refutation arises, which means we achieve the opposite of our original aim - to establish more bilaterality. The reasons for this are related to deeper issues that we need to think about, such as our notion of refutation and our understanding of derivability in natural deduction and in sequent calculus. Therefore, I will argue, either we accept that there are limits as to how bilateral we can design a sequent calculus or we need to give up certain prima facie intuitive background assumptions concerning derivability.
Bibliography
- Heinrich Wansing,A more general general proof theory,Journal of Applied Logic,vol. 25 (2017), pp.23–46.