module PropositionalLogic where -- Look at the types of the following basic "combinators" in the lambda calculus: -- identity: I : {A : Set} → A → A I x = x -- composition: B : {A B C : Set} → (B → C) → (A → B) → A → C B g f x = g (f x) -- constant: K : {A B : Set} → A → B → A K x y = x -- generalized composition: S : {A B C : Set} → (A → B → C) → (A → B) → A → C S g f x = g x (f x) -- Haskell B Curry observed that the types of these combinators correspond to axioms of implication -- provided you read → as implication rather than function type. -- In a similar way conjunction corresponds to Cartesian product -- The constructor corresponds to the "introduction rule": data _&_ (A B : Set) : Set where <_,_> : A → B → A & B -- And the projections correspond to "elimination rules" fst : {A B : Set} → A & B → A fst < x , y > = x snd : {A B : Set} → A & B → B snd < x , y > = y -- disjunction = disjoint union (sum) -- constructors = introduction rules data _∨_ (A B : Set) : Set where inl : A → A ∨ B inr : B → A ∨ B -- definition by cases = proof by cases (elimination rule) case : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C case f g (inl x) = f x case f g (inr y) = g y comm-∨ : (A B : Set) → A ∨ B → B ∨ A comm-∨ A B p = {!!} -- the true proposition = the unit type data ⊤ : Set where <> : ⊤ -- the false proposition = the empty type data ⊥ : Set where -- definition by no case = proof by no case (falsity implies anything) nocase : {C : Set} → ⊥ → C nocase c = {!!} -- If we want to have the correspondence between constructor -- and introduction rule also for → we can -- define the following data type with one constructor: data _⊃_ (A B : Set) : Set where ⊃-intro : (A → B) → A ⊃ B -- the elimination rule is "modus ponens": mp : {A B : Set} → A ⊃ B → A → B mp f a = {!!} -- note: nocase is defined by an empty case analysis (pattern matching) -- but Agda requires a line "nocase ()" to express this, -- rather than just an empty set of patterns -- Negation ¬ : Set → Set ¬ A = A → ⊥ -- Excluded middle is not valid em : (A : Set) → A ∨ ¬ A em A = {!!} -- Double negation is not valid either dn : (A : Set) → ¬ (¬ A) → A dn A g = {!!} -- Exercise: Prove reversedn : (A : Set) → A → ¬ (¬ A) reversedn A a = {!!} triplenegation : (A : Set) → ¬ (¬ (¬ A)) → ¬ A triplenegation A t a = {!!} emdn : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A emdn em A nna = {!!} -- This is called the BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic -- or the Curry-Howard correspondence of propositions as types. Howard showed how to -- generalize this to predicate logic by introducing dependent types.