Many new results and new insights about classical and non-classical logics have been obtained using the sequent calculus, e.g. Gentzen’s consistency argument; interpolation, decidability, complexity for modal and substructural logics; (what else?). I would like to identify new results and insights about logics that were obtained using proof systems—other than the sequent calculus—that utilised some…
Revantha Ramanayake
Contraction on a leash
The contraction rule (c) (discussed also in this blog post) is a familiar obstacle to anyone aiming to use the sequent calculus to establish a property of the underlying logic. Simply stated the issue is that the premise of the rule is more complicated (contains more content) than its conclusion, and hence proof…
