This talk will present an after-the-fact and historically distorted account of certain aspects of proof theory. The narrative will follow an attempt to rediscover, and justify from an algebraic point of view, the concept of a sequent, the system FL, the formula hierarchy and cut elimination for the system and some of its extensions; the analysis will be based purely on algebraic considerations.
The resulting Algebraic Proof Theory aims at providing a relational semantics setting that encompass aspects of both algebra and proof theory. As it applies to the non-distributive case, there are two sets of worlds in the semantics. This corresponds to the fact that (say finite) lattices, unlike distributive lattices, need both sets of join and meet irreducible elements for their description. The additional connectives can be added to this two-sorted structure leading to a creation of a module (over a semiring), a viewpoint that has been useful in other applications, as well, and views logical implication as akin to scalar multiplication in vector spaces.
The work is based on important considerations of H. Ono and C. Tsinakis and have been developed in collaboration with various researchers. (Any shortcomings of the narrative are of course the responsibility of the presenter.)