Syllogism is a tautology by nrolland

module Theorem where

open import Definitions
open import Data.Bool renaming(true to t;false to f)

module NoStructure where
  syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
  syllogism-is-tauto P Q R φ with ev P φ | ev Q φ | ev R φ
  ... | t | t | t = refl
  ... | t | t | f = refl
  ... | t | f | t = refl
  ... | t | f | f = refl
  ... | f | t | t = refl
  ... | f | t | f = refl
  ... | f | f | t = refl
  ... | f | f | f = refl

module MixingEvAndTraversal where
  syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
  syllogism-is-tauto P Q R phi with ev P phi
  syllogism-is-tauto P Q R phi | t with ev Q phi 
  syllogism-is-tauto P Q R phi | t | t with ev R phi
  syllogism-is-tauto P Q R phi | t | t | t = refl
  syllogism-is-tauto P Q R phi | t | t | f = refl
  syllogism-is-tauto P Q R phi | t | f = refl
  syllogism-is-tauto P Q R phi | f with ev Q phi 
  syllogism-is-tauto P Q R phi | f | t with ev R phi
  syllogism-is-tauto P Q R phi | f | t | t = refl
  syllogism-is-tauto P Q R phi | f | t | f = refl
  syllogism-is-tauto P Q R phi | f | f = refl

module Kawai where
  _⇒_ : Bool -> Bool -> Bool
  a ⇒ b = not a ∨  b

  syl : ∀ (p q r : Bool) -> ((p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r))) == t
  syl t t t = refl
  syl t t f = refl
  syl t f r = refl
  syl f t t = refl
  syl f t f = refl
  syl f f r = refl

  syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
  syllogism-is-tauto p q r c = syl (ev p c) (ev q c) (ev r c)


open Kawai public