Gaggles, Gentzen and Galois: A Proof Theory for Algebraizable Logics
Rajeev Gor?e
Automated Reasoning Project
[email protected]
April 16, 1995
Abstract
We show how the Gaggle Theory of Dunn gives a Gentzen-style proof theory for many algebraizable logics via the Display Logic of Belnap. At the heart of both systems lie the algebraic notions of residuation, Galois connections, and their duals.

Introduction It is well known that most non-classical logics have an underlying algebraic semantics. Many non-classical logics also have a relational semantics using Kripke models. In a series of papers [Dun91, Dun93b, Dun93a], Dunn has shown that there are deep connections between these algebraic and relational semantics where each n-ary connective in a logic has an n + 1-ary relational semantics.

The Display Logic [Bel82] of Belnap is a powerful Gentzen formulation which has been used to obtain Gentzen systems for non-classical logics like modal logic [Wan94], intuitionistic and intermediate logics [Gor95], and substructural logics [Res94]. As Belnap says Evidently, algebra is in the air, especially residuation" [Bel82, page 409].
We use the insights of Dunn to dissect Display Logic and uncover the roles played by residuation, Galois connections, and their duals.

The Binary Cases The collection of display rules shown below left involve three binary functions s, r1 and r2. The objects at the right are tonicity conditions for the three functions together with a pair of axiomatic rules that tell us something about the nesting of these functions.

x ` r1(z; y)

s(x; y) ` z

y ` r2(x; z)

r1(+; ?) a ` r1(s(a; b); b) s(r1(a; b); b) ` a
s(+; +) a ` r2(b; s(b; a)) s(b; r2(b; a)) ` a
r2(?; +) a ` r2(r1(b; a); b) a ` r1(b; r2(a; b))

The functions s and r1 form a dual residuated pair in the first position written drp1(s; r1); the functions s and r2 form a residuated pair in the second position written rp2(s; r2); and the functions r1 and r2 form a Galois connection in the first and second positions written gc1:2(r1; r2). The display rules, or the tonicity vectors together with the axiom pairs, are equivalent definitions of these concepts [Dun91].

Tonicity Again The tonicity of a binary function can be specified in two equivalent ways. The first is to use the explicit pair of rules shown below left.