A Model–Theoretic Approach to Proof Theory

Proof theory for lattice-ordered groups

10.29007/3szk ◽

2018 ◽

Author(s):

George Metcalfe

Keyword(s):

Proof Theory ◽

Family Resemblance ◽

Substructural Logics ◽

Residuated Lattices ◽

Cut Elimination ◽

Theoretic Approach ◽

Gentzen Systems ◽

Ordered Groups ◽

Lattice Ordered Groups ◽

Mv Algebras

Proof theory can provide useful tools for tackling problems in algebra. In particular, Gentzen systems admitting cut-eliminationhave been used to establish decidability, complexity, amalgamation, admissibility, and generation results for varieties of residuated lattices corresponding to substructural logics. However, for classes of algebras bearing some family resemblance to groups, such as lattice-ordered groups, MV-algebras, BL-algebras, and cancellative residuated lattices, the proof-theoretic approach has met so far only with limited success.The main aim of this talk will be to introduce proof-theoretic methods for the class of lattice-ordered groups and to explain how these methods can be used to obtain new syntactic proofs of two core theorems: namely, Holland's result that this class is generated as a variety by the lattice-ordered group of order-preserving automorphisms of the real numbers, and the decidability of the word problem for free lattice-ordered groups.

Download Full-text

Higher-level Inferences in the Strong-Kleene Setting: A Proof-theoretic Approach

Journal of Philosophical Logic ◽

10.1007/s10992-021-09639-z ◽

2021 ◽

Author(s):

Pablo Cobreros ◽

Elio La Rosa ◽

Luca Tranchini

Keyword(s):

Proof Theory ◽

Sequent Calculus ◽

Theoretic Approach ◽

Philosophical Logic ◽

Huge Number ◽

Natural Manner

AbstractBuilding on early work by Girard (1987) and using closely related techniques from the proof theory of many-valued logics, we propose a sequent calculus capturing a hierarchy of notions of satisfaction based on the Strong Kleene matrices introduced by Barrio et al. (Journal of Philosophical Logic 49:93–120, 2020) and others. The calculus allows one to establish and generalize in a very natural manner several recent results, such as the coincidence of some of these notions with their classical counterparts, and the possibility of expressing some notions of satisfaction for higher-level inferences using notions of satisfaction for inferences of lower level. We also show that at each level all notions of satisfaction considered are pairwise distinct and we address some remarks on the possible significance of this (huge) number of notions of consequence.

Download Full-text