It is quite well understood that propositional logics are tightly connected to ordered algebras via algebraic completeness, and because of this connection proof theory is often useful in the algebraic context too. A prominent example is that one deductively proves the interpolation theorem for a given logic in order to derive the algebraic amalgamation property for the corresponding variety as a corollary. Other examples include uniform interpolation, disjunction property, local deduction theorem, and termination of complete proof search with their corresponding algebraic properties. Proof theory is, however, not merely an external device for deriving algebraic consequences as corollaries. The connection is even tighter, and it also works inside algebra as a source of various algebraic constructions. For instance, Mae-hara's sequent-based method for proving the interpolation theorem gives rise to a direct construction of an algebra required for the amalgamation property. Finding a new variant of sequent calculus (such as hypersequent calculus) amounts to finding a new variant of MacNeille completions (generalizations of Dedekind's completion Q → R). Proving cut elimination for such a generalized sequent calculus is closely related to proving that a variety is closed under the corresponding generalized completions. Finally, transforming Hilbert axioms into Gentzen rules is not only important for proving cut elimination and related conservativity results, but also crucial for ensuring that the above proof theoretic constructions do work in algebra properly.
展开▼
