Cuts and Completions: Algebraic aspects of structural proof theory
Frederik Möllerström Lauridsen

Abstract:
In this thesis, entitled Cuts and Completions: Algebraic aspects of structural proof theory, we look at different aspects of the interplay between structural proof theory and algebraic semantics for several non-classical propositional logics. Concretely, we explore connections between proof theory and algebra as they relate to structural sequent and hypersequent calculi for intermediate and substructural logics. Such  connections are particularly strong for logics associated with the levels P_3 and N_2 of the substructural hierarchy introduced by Ciabattoni, Galatos, and Terui. Therefore, we investigate different algebraic aspects of these two levels. Among the algebraic aspects considered, completions of lattices and lattice-based algebras take on a prominent role.
  
In Chapter 2 we consider the question of which intermediate logics admit a structural hypersequent calculus. This question is answered by introducing the notion of (∧, 0, 1)-stable logics which is a strengthening of the notion of (∧, ∨, 0, 1)-stable logics introduced by Guram and Nick Bezhanishvili. We show that the (∧, 0, 1)-stable logics are precisely the intermediate logics which admit a structural hypersequent calculus. We further investigate these logics in their own right, showing in particular that they are all sound and complete with respect to a first-order definable class of partially ordered sets. 

In Chapter 3 we introduce various notions of MacNeille and canonical transferability for finite lattices analogous to Grätzer's notion of (ideal) transferability. We show how finite transferable lattices give rise to universal classes of lattices closed under completions. We focus mainly on providing necessary or sufficient conditions for a finite distributive lattice to be MacNeille transferable for different classes of Heyting algebras. Lastly, we discuss how MacNeille and canonical transferability of finite distributive lattices is related to the problem of establishing the elementarity and the canonicity of (∧, ∨, 0, 1)-stable logics.
 
Chapter 4 contains an investigation of the concept of hyper-MacNeille completions introduced by Ciabattoni, Galatos, and Terui as it applies in the setting of Heyting algebras. We single out the notion of a De Morgan supplemented Heyting algebra as being central for understanding the hyper-MacNeille completions of Heyting algebras. We show that the MacNeille and hyper-MacNeille completions coincide for De Morgan supplemented Heyting algebras. Furthermore, we show that the hyper-MacNeille completion of any Heyting algebra is the MacNeille completion of some De Morgan supplemented Heyting algebra. Lastly, we provide necessary and sufficient conditions for the hyper-MacNeille completion of a Heyting algebra to be a regular completion.  

Finally, in Chapter 5 we establish a Glivenko-style property for the variety of integrally closed residuated lattices with respect to the variety of lattice-ordered groups. This is used to construct a non-standard sequent calculus for the equational theory of integrally closed residuated lattices. Using this calculus we prove the decidability of the equational theory of integrally closed residuated lattices. Lastly, we compare the equational theory of integrally closed residuated lattices with the equational theories of pseudo BCI-algebras, semi-integral residuated partially ordered monoids, and algebras for Casari's comparative logic.