Negation

• The missing logical operator, ¬ (“not”), is a little funny

• It is closely related to ⊥ (“nonsense”):

¬p ≡ p → ⊥

• In Haskell, ⊥ is a type with no elements

• It's the type of value that is(n't) returned by an infinite loop

• or by a calculation that throws a fatal exception

• In practice, it never comes up

• The Haskell type checker always infers a more general type:

        undefined          ::  a

        loop x = loop x
        -- loop   :: b -> a
        -- loop x :: a

• In Haskell, ¬p ≡ p → ⊥ is a function that takes p and fails to return

• In logic, we have:

• From p ∧ ¬p, conclude ⊥ (⊥I)

• From ⊥, conclude anything (⊥E)

• Easy exercise:

(¬p ∧ p) → ⊥
(p -> Void, p) → Void