ON SYNONYMY IN PROOF-THEORETIC SEMANTICS. THE CASE OF 2Int.

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus SC2Int for the bi-intuitionistic logic 2Int. A distinctive feature of SC2Int is that it makes use of two kinds of sequents, one representing proofs, the other representing refutations. The structural rules of SC2Int, in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, mediated through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of 2Int. By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in SC2Int is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. [ABSTRACT FROM AUTHOR]