9 Connectives

PLFA explores various laws in propositional logic using the tools of the previous chapter: isomorphism, embedding, and propositional equivalence. In SF this is done using implication and sometimes "iff", and (following the Coq standard library) the connectives look like they do in mathematical logic. In Agda they look more like set connectives, which makes sense given the more explicit nature of Agda proofs, and the fact that these connectives are useful in contexts where they do not have a natural logical interpretation. In text, I will sometimes use the logical names and sometimes the set-operator names. Remembering the Unicode characters for the operators and the Emacs commands needed to generate each one may be the hardest part of this chapter!

An unexpected and delightful bonus is that the proof constructs correspond to useful programming language features. This strengthens the "proofs are programs" metaphor, and you may find yourself using it when reasoning in contexts far removed from this course.

9.1 Conjunction is product

A proof of a logical AND (conjunction) is, mathematically, a Cartesian product, and computationally a pair (two-element struct or record). The Agda operator is _×_ (in Agda mode, \x) and I usually pronounce it as "and" or "times", and sometimes "cross" (though it is not multiplication and it is not vector cross-product).

The usual mathematical convention for forming an element of a Cartesian product \(A \times B\) is \((a,b)\), and the Agda standard library uses this. In fact, since parentheses are already used in Agda for grouping, you can omit them or include them. But PLFA wants to use commas for other purposes later on, so it has slightly modified the mathematical notation by using (required) angle brackets instead, like \(\langle a,b \rangle\).

The corresponding Agda definition is the first time we are seeing "mixfix" notation, where the underscores indicating argument placement are in the middle of syntactic elements. Although the definition is written without spaces, when we use the constructor, spaces have to be inserted before and after arguments, otherwise the parser might see a variable name instead.

data _×_ (A : Set) (B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

We can define the destructors or eliminators of a conjunction, which are the projection functions picking out first or second elements of a pair.

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A

proj₁ ⟨ x , x₁ ⟩ = x

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B

proj₂ ⟨ x , x₁ ⟩ = x₁

In practice, we use these infrequently, instead using pattern matching (as on the left-hand side of these definitions) directly. These functions can be useful as arguments to function composition or other higher-order functions, but even there, they can be defined on the fly using a pattern lambda.

The Agda standard library uses a two-field record to define conjunction. This has certain advantages because of the way records are handled, which is explained in more detail by PLFA.

PLFA defines Booleans here primarily to provide an example of a two-element set. They are, of course, important computationally, and we will come back to them later.

Logically, \(A \land B\) and \(B \land A\) are equivalent, that is, \((A \land B) \iff (B \land A)\) always holds. But we saw in the Isomorphism chapter that propositional equivalence is weaker than isomorphism, and here we can make the stronger statement that \(A \times B \simeq B \times A\). We say that "conjunction is commutative up to isomorphism" (because it is not in general the case that \(A \times B = B \times A\)). Here are the proofs of commutativity and associativity using co-patterns.

×-comm : ∀ {A B : Set} → A × B ≃ B × A
to ×-comm ⟨ x , x₁ ⟩ = ⟨ x₁ , x ⟩
from ×-comm ⟨ x , x₁ ⟩ = ⟨ x₁ , x ⟩
from∘to ×-comm ⟨ x , x₁ ⟩ = refl
to∘from ×-comm ⟨ x , x₁ ⟩ = refl

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
to ×-assoc ⟨ ⟨ x , x₂ ⟩ , x₁ ⟩ = ⟨ x , ⟨ x₂ , x₁ ⟩ ⟩
from ×-assoc ⟨ x , ⟨ x₁ , x₂ ⟩ ⟩ = ⟨ ⟨ x , x₁ ⟩ , x₂ ⟩
from∘to ×-assoc ⟨ ⟨ x , x₂ ⟩ , x₁ ⟩ = refl
to∘from ×-assoc ⟨ x , ⟨ x₁ , x₂ ⟩ ⟩ = refl

9.2 Truth is unit

We define propositional "true" as ⊤ (in Agda mode, \top), the set with one element (constructed with tt). I pronounce it "true" or "top", and sometimes "unit". It is the left and right identity of conjunction up to isomorphism. Here are the proofs of identity using co-patterns.

⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
to ⊤-identityˡ ⟨ x , x₁ ⟩ = x₁
from ⊤-identityˡ x = ⟨ tt , x ⟩
from∘to ⊤-identityˡ ⟨ tt , x₁ ⟩ = refl
to∘from ⊤-identityˡ y = refl

⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
to ⊤-identityʳ ⟨ x , x₁ ⟩ = x
from ⊤-identityʳ a = ⟨ a , tt ⟩
from∘to ⊤-identityʳ ⟨ x , tt ⟩ = refl
to∘from ⊤-identityʳ a = refl

9.3 Disjunction is sum

A proof of a logical OR (disjunction) is, mathematically, disjoint union, and computationally a variant type (like a C union, but enforced). The Agda operator is _⊎_ (in Agda mode, \u+) and I usually pronounce it as "or" or "sum", and sometimes "union" (though it is not set union).

data _⊎_ : Set → Set → Set where

  inj₁ : ∀ {A B : Set}
    → A
      -----
    → A ⊎ B

  inj₂ : ∀ {A B : Set}
    → B
      -----
    → A ⊎ B

The constructors "inject" values into the disjunction. PLFA demonstrates functions that eliminate or use a disjunction, but in practice, once again, this is done on the fly using the same sort of pattern matching with which these functions are defined. Commutativity and associativity up to isomorphism are exercises for credit.

9.4 False is empty

We define propositional "false" as ⊥ (in Agda mode, \bot), the set with no elements (no constructors). It is the left and right identity of disjunction up to isomorphism. I pronounce it "false" or "bottom", and sometimes "empty". Working with it takes some getting used to, but it is used in defining negation (in the next chapter), so it’s worth the effort.

This section introduces the absurd pattern (), which means "nothing matches". It is slightly startling at first when Agda adds it during interaction.

Unlike the elimination functions described above, ⊥-elim is used more in practice, as we will see.

9.5 Implication is function

We’ve already been using the function type operator for implication, but in set theory, the set of all functions of type A → B is written Bᴬ and can be pronounced "B to the power A" and called "exponentiation". Some programming languages papers and references use this terminology, so it’s worth remembering.

Here is an asciicast of the first of the function space isomorphisms in PLFA, using co-patterns. Watching too many of these isomorphism proofs live can be tedious, so instead I suggest that you load the starter file and practice on the ones I did not show, peeking at the completed file if you get stuck. That should set you up well for the exercises to follow.

9.6 Distribution

Here we see an example of using the stronger forms of propositional equivalence to distinguish the strength of various properties. "Products distribute over sums" is an isomorphism, but "sums distribute over products" is an embedding. It’s worth coming up with a counterexample to show why the latter cannot be an isomorphism.

In doing the exercises, remember that you have the choice of using co-patterns as I have done here and in the asciicasts, or record syntax and lambdas as in PLFA, if you prefer.