1.4.8. Duality

The properties of ⊤ and ⊥ take a particularly symmetric form when stated in the context of relative exhaustiveness.

as a premise as an alternative
Tautology if Γ, ⊤ ⇒ Δ, then Γ ⇒ Δ  ⇒ ⊤
Absurdity ⊥ ⇒  if Γ ⇒ ⊥, Δ, then Γ ⇒ Δ

That is, while ⊤ contributes nothing as a premise and may be dropped, it is sufficient by itself as the only alternative (no matter how small our set of premises). And while ⊥ is sufficient by itself as a premise (no matter how small the set of alternatives is), it contributes nothing as an alternative and may be dropped.

The symmetry here might be traced to the symmetry of relative exhaustiveness: since ⊤ and ⊥ are contradictory, having one as an assumption comes to the same thing as having the other as an alternative according to the basic law of relative exhaustiveness discussed in 1.4.5. However, there is a more general idea behind this symmetry that will apply also to cases where sentences are not contradictory.

We will spend a moment looking more closely at the pattern that contradictoriness provides for here in order to make it easier to recognize in other cases. To take the simplest example of symmetry in the table above, we might state the lower left and upper right as follows:

⊥⇒
⊤⇐

(where an arrow running right to left is understood to have its alternatives on its left and its premises on its right). That is, the difference lies in interchanging Absurdity and Tautology and reversing the direction of the arrow—or, what comes to the same thing, interchanging premises and alternatives. If we apply the same transition to the principle at the upper left we get

if Γ, ⊥ ⇐ Δ, then Γ ⇐ Δ

or, rewriting so the arrows run left to right (without change of premises and alternatives),

if Δ ⇒ ⊥, Γ, then Δ ⇒ Γ

which differs from the principle for Absurdity as an alternative on the lower right above only in the interchange of Γ and Δ; and, since each could be any set, exchanging them does not alter the content of the principle. The possibility of this sort of transformation can be expressed by saying that ⊤ and ⊥ on the one hand and premise (or assumption) and alternative on the other constitute pairs of dual terms. We will run into other pairs of dual terms later.

Glen Helman 15 Aug 2006