Display Logic and Gaggle Theory

Greg Restall | Greg.Restall@anu.edu.au

Nuel Belnap's Display Logic [1] is a neat, uniform method for providing a cut-free consecution calculus for a wide range of formal systems. Mike Dunn's Gaggle Theory [3] is a neat, uniform presentation of the semantics for a wide range of formal systems. In this paper I will show that the two live together happily | many gaggle-theoretically presented logics can be given a display proof theory, and that many logics with a display proof theory can be algebraically presented in gaggle theory.

1 Gaggle Theory

Dunn [3] introduced the notion of a gaggle as a way to unify many different logics | modal, intuitionistic, many-valued, and substructural logics are examples of those which fit the general scheme.

Consider propositions, partially ordered by <=, the relation of entailment. In many different logics, there are properties relating the behaviour of connectives with the entailment relation. For example, in many logics containing a conditional !, it is possible to show the following:

If a <= b then c ! a <= c ! b.
If a <= b then b ! c <= a ! c.

Furthermore, if the partial order has a greatest element 1 and a least element , then we also have

! a = 1 and x ! 1 = 1

We can symbolise this by saying that in these logics ! has a race" of (?; +) 7! +, for the following reasons:

ffl The `limiting value' of the conditional as a whole is 1, when the inputs reach limits. So, we say the conditional as a whole has a `positive' value, and we give the output value a +".

ffl Now if the consequent of the conditional is `increased' then the value of the whole conditional is `increased'. As a result, the value of the second place in the input should have the same value as the output. So we have the second +".

ffl On the other hand, `increasing' the antecedent `decreases' the whole conditional. So the value of the first place in the input has the opposite sign to the output. This explains the ?" in the first place.

Note that the conditional of the `conditional logics' of Lewis and Stalnaker do not get this tonicity (or any other) as in these cases we do not have that if a <= b then b ! c <= a ! c.
In general, an n-ary connective f has a trace (o1; : : : ; on) 7! + if

ffl f(c1; : : : ; 1; : : : ; cn) = 1, if oi = + (where the 1 is in position i).

ffl f(c1; : : : ; ; : : : ; cn) = 1, if oi = ? (where the is in position i).

ffl If a <= b, and if oi = + then f(c1; : : : ; a; : : : ; cn) <= f(c1; : : : ; b; : : : ; cn).

ffl If a <= b, and if oi = ? then f(c1; : : : ; b; : : : ; cn) <= f(c1; : : : ; a; : : : ; cn).