hm.agda

-- Definitions
module hm where

data ⊥ : Set where

data V : Set where
  i : V

data _∧_ (φ ψ : Set) : Set where
  and-intro : φ → ψ → φ ∧ ψ

data _∨_ (φ ψ : Set) : Set where
  or-introl : φ → φ ∨ ψ
  or-intror : ψ → φ ∨ ψ

data _[_/_] {a} (φ : Set a) : V →  V → Set a where
  subst : φ →  (ζ : V) → (ξ : V) → φ [ ζ / ξ ]

data all : V → Set → Set where
  gen : (ζ : V) → (φ : Set) → all ζ φ

data ∃ : V → Set → Set where
  ex : (ζ : V) → (φ : Set) → ∃ ζ φ

¬_ : (φ : Set) → Set
¬ φ = φ → ⊥

infix 100 ¬_

_↔_ : (φ ψ : Set) → Set
_↔_ φ ψ = (φ → ψ) ∧ (ψ → φ)
infixl 5 _↔_


-- Axioms
S : {φ ψ χ : Set} → (φ → ψ → χ) → (φ → ψ) → φ → χ
S {φ} {ψ} {χ} =
  λ x y z → x z (y z)

K : {φ ψ : Set} → φ → ψ → φ
K {φ} {ψ} =
  λ x y → x

DI₁ : {φ ψ : Set} → φ → φ ∨ ψ
DI₁ = λ p → or-introl p

DI₂ : {φ ψ : Set} → ψ → φ ∨ ψ
DI₂ = λ q → or-intror q

DE : {φ ψ χ : Set} → (φ → χ) → (ψ → χ) → (φ ∨ ψ → χ)
DE x y (or-introl x₁) = x x₁
DE x y (or-intror x₁) = y x₁

CI : {φ ψ : Set} → φ → ψ → (φ ∧ ψ)
CI {φ} {ψ} x y = and-intro x y

CE₁ : {φ ψ : Set} → (φ ∧ ψ) → φ
CE₁ (and-intro x y) = x

CE₂ : {φ ψ : Set} → (φ ∧ ψ) → ψ
CE₂ (and-intro x y) = y

postulate
  UI : {φ ψ : Set}{ζ ξ : V} → all ζ (ψ → φ [ ζ / ξ ]) → (ψ → all ξ φ)
  UE : {φ : Set}{ξ τ : V} → all ξ φ → φ [ τ / ξ ]
  EI : {φ : Set}{ξ τ : V} → φ [ τ / ξ ] → ∃ ξ φ
  EE : {φ ψ : Set}{ξ ζ : V} → all ζ (φ [ ζ / ξ ] → ψ) → (∃ ξ φ → ψ)
  GEN : {φ : Set}{ζ ξ : V} → φ [ ζ / ξ ] → all ξ φ
  theorem5421₁ : {φ : Set}{ξ : V} → φ [ ξ / ξ ] → φ
  theorem5421₂ : {φ : Set}{ξ : V} → φ → φ [ ξ / ξ ]


-- Theorems
I : {φ : Set} → φ → φ
I {φ} = S {φ} {φ → φ} {φ} (K {φ} {φ → φ}) (K {φ} {φ})

B : {φ ψ χ : Set} → (ψ → χ) → (φ → ψ) → (φ → χ)
-- λ x y z → x (y z)
B {φ} {ψ} {χ} =
  let
    p1 = K {(φ → ψ → χ) → (φ → ψ) → φ → χ} {ψ → χ}
    p2 = p1 (S {φ} {ψ} {χ})
    p3 = K {ψ → χ} {φ}
    p4 = S {ψ → χ} {φ → ψ → χ} {(φ → ψ) → φ → χ}
  in
    p4 p2 p3

C : {φ ψ χ : Set} → (φ → ψ → χ) → (ψ → φ → χ)
C {φ} {ψ} {χ} =
  let
    s1 = S {φ} {ψ} {χ}
    k1 = K {ψ} {φ}
    k2 = K {(φ → ψ) → φ → χ} {ψ}
    s2 = S {ψ} {φ → ψ} {φ → χ}
    b1 = B {φ → ψ → χ} {(φ → ψ) → φ → χ} {ψ → (φ → ψ) → φ → χ} k2 s1
    k3 = K {ψ → φ → ψ} {φ → ψ → χ} k1
    k4 = K {(ψ → (φ → ψ) → φ → χ) → (ψ → φ → ψ) → ψ → φ → χ} {φ → ψ → χ} s2
    s3 = S {φ → ψ → χ} {ψ → (φ → ψ) → φ → χ} {(ψ → φ → ψ) → ψ → φ → χ} k4 b1
    s4 = S {φ → ψ → χ} {ψ → φ → ψ} {ψ → φ → χ} s3 k3
  in
    s4

W : {φ ψ : Set} → (φ → φ → ψ) → (φ → ψ)
W {φ} {ψ} =
  -- λ x y → x y y
  let
    k1 = K {φ → φ} {φ → φ → ψ} (I {φ})
    -- k  : (φ → φ → ψ) → φ → φ
    s1 = S {φ} {φ} {ψ}
    -- s1 : (φ → φ → ψ) → (φ → φ) → φ → ψ
    s2 = S {φ → φ → ψ} {φ → φ} {φ → ψ} s1 k1
    -- s2 : (φ → φ → ψ) → (φ → ψ)
  in
    s2

B′ : {φ ψ χ : Set} → (φ → ψ) → (ψ → χ) → (φ → χ)
B′ {φ}{ψ}{χ} =
  let
    c1 = C {ψ → χ} {φ → ψ} {φ → χ}
    b1 = B {φ}{ψ}{χ}
  in
    c1 b1

C⋆ : {φ ψ : Set} → φ → (φ → ψ) → ψ
C⋆ {φ} {ψ} =
  let
    k1 = K {φ} {φ → ψ}
    -- k1 : φ → (φ → ψ) → φ
    s1 = S {φ → ψ} {φ} {ψ} (I {φ → ψ})
    -- s1 : ((φ → ψ) → φ) → (φ → ψ) → ψ
    k2 = K {((φ → ψ) → φ) → (φ → ψ) → ψ} {φ} s1
    -- k2 : φ → ((φ → ψ) → φ) → (φ → ψ) → ψ
    s2 = S {φ} {(φ → ψ) → φ} {(φ → ψ) → ψ} k2 k1
  in
    s2

-- exercise 7.38
-- φ ⊣⊢ ψ ⇔ ⊢ φ ↔ ψ
-- (⇒)
-- 仮定より
-- φ ⊢ ψ かつ ψ ⊢ φ
-- DT より
-- ⊢ φ → ψ
-- ⊢ ψ → φ
-- 1. φ → ψ   : DT
-- 2. ψ → φ   : DT
-- 3. (φ → ψ) → (ψ → φ) → (φ → ψ) ∧ (ψ → φ)   :  CI {φ → ψ} {ψ → φ}
-- 4. (φ → ψ) ∧ (ψ → φ) : MP 3, 1, 2
-- 5. φ ↔ ψ  : 定義
module Ex7_38l where
  private
    postulate
      φ : Set
      ψ : Set
      postulate₁ : φ → ψ
      postulate₂ : ψ → φ

  ex7_38l : φ ↔ ψ
  ex7_38l =
    let
      p1 = postulate₁
      -- φ → ψ
      p2 = postulate₂
      -- ψ → φ
      p3 = CI {φ → ψ}{ψ → φ}
      -- (φ → ψ) → (ψ → φ) → (φ → ψ) ∧ (ψ → φ)
      p4 = p3 p1 p2
      -- (φ → ψ) ∧ (ψ → φ)
    in
      p4

-- (<=)
-- 1. φ ↔ ψ   : 仮定
-- 2. (φ → ψ) ∧ (ψ → φ)  : 定義
-- 3. (φ → ψ) ∧ (ψ → φ) → φ → ψ : CE₁ {φ → ψ} {ψ → φ}
-- 4. φ → ψ  : MP 2, 3
-- 5. (φ → ψ) ∧ (ψ → φ) → ψ → φ : CE₂ {φ → ψ} {ψ → φ}
-- 6. ψ → φ  : MP 2, 5
-- φ を仮定するとMP 4から ψ を導出できる。
-- よって φ ⊢ ψ
-- ψ を仮定するとMP 6から φ を導出できる。
-- よって ψ ⊢ φ
-- よって φ ⊣⊢ ψ
module Ex7_38r where
  private
    postulate
      φ : Set
      ψ : Set
      postulate₁ : (φ ↔ ψ)
      postulate₂ : φ
      postulate₃ : ψ

  ex7_38r₁ : ψ
  ex7_38r₁ =
    let
      p1 = postulate₁
      -- φ ↔ ψ
      p2 = postulate₂
      -- φ
      p3 = CE₁ {φ → ψ}{ψ → φ}
      -- (φ → ψ) ∧ (ψ → φ) → φ → ψ
      p4 = p3 p1
      -- φ → ψ
    in
      p4 p2

  ex7_38r₂ : φ
  ex7_38r₂ =
    let
      p1 = postulate₁
      -- φ ↔ ψ
      p2 = postulate₃
      -- ψ
      p3 = CE₂ {φ → ψ}{ψ → φ}
      -- (φ → ψ) ∧ (ψ → φ) → ψ → φ
      p4 = p3 p1
      -- ψ → φ
    in
      p4 p2


-- exercise 7.39
ex1 : {φ ψ χ : Set} → (φ ∧ (ψ ∧ χ)) ↔ ((φ ∧ ψ) ∧ χ)
ex1 {φ}{ψ}{χ} =
  let
    -- (φ ∧ (ψ ∧ χ)) → ((φ ∧ ψ) ∧ χ)
    l1 = CE₁ {φ} {ψ ∧ χ}
    -- φ ∧ (ψ ∧ χ) → φ
    l2 = B {φ ∧ (ψ ∧ χ)}{ψ ∧ χ}{ψ} (CE₁ {ψ} {χ}) (CE₂ {φ} {ψ ∧ χ})
    -- φ ∧ (ψ ∧ χ) → ψ
    l3 = B {φ ∧ (ψ ∧ χ)}{ψ ∧ χ}{χ} (CE₂ {ψ} {χ}) (CE₂ {φ} {ψ ∧ χ})
    -- φ ∧ (ψ ∧ χ) → χ
    l4 = CI {φ}{ψ}
    -- φ → ψ → φ ∧ ψ
    l5 = B {φ ∧ (ψ ∧ χ)}{φ}{ψ → φ ∧ ψ} l4 l1
    -- φ ∧ (ψ ∧ χ) → (ψ → φ ∧ ψ)
    l6 = S {φ ∧ (ψ ∧ χ)}{ψ}{φ ∧ ψ} l5 l2
    -- φ ∧ (ψ ∧ χ) → φ ∧ ψ
    -- l5: φ ∧ (ψ ∧ χ) → ψ → φ ∧ ψ
    -- l2: φ ∧ (ψ ∧ χ) → ψ
    -- S: (φ → ψ → χ) → (φ → ψ) → φ → χ
    -- (φ ∧ (ψ ∧ χ) → ψ → φ ∧ ψ) → (φ ∧ (ψ ∧ χ) → ψ)
         -- → φ ∧ (ψ ∧ χ) → φ ∧ ψ
    l7 = CI {φ ∧ ψ} {χ}
    -- φ ∧ ψ → χ → (φ ∧ ψ) ∧ χ
    l8 = B {φ ∧ (ψ ∧ χ)}{φ ∧ ψ}{χ → (φ ∧ ψ) ∧ χ} l7 l6
    -- φ ∧ (ψ ∧ χ) → χ → (φ ∧ ψ) ∧ χ
    l9 = S {φ ∧ (ψ ∧ χ)}{χ}{(φ ∧ ψ) ∧ χ} l8 l3
    -- φ ∧ (ψ ∧ χ) → (φ ∧ ψ) ∧ χ

    -- (φ ∧ ψ) ∧ χ → φ ∧ (ψ ∧ χ)
    r1 = B {(φ ∧ ψ) ∧ χ}{φ ∧ ψ}{φ} (CE₁ {φ} {ψ}) (CE₁ {φ ∧ ψ} {χ})
    -- (φ ∧ ψ) ∧ χ → φ
    r2 = B {(φ ∧ ψ) ∧ χ}{φ ∧ ψ}{ψ} (CE₂ {φ} {ψ}) (CE₁ {φ ∧ ψ} {χ})
    -- (φ ∧ ψ) ∧ χ → ψ
    r3 = CE₂ {φ ∧ ψ} {χ}
    -- (φ ∧ ψ) ∧ χ → χ
    r4 = CI {ψ}{χ}
    -- ψ → χ → ψ ∧ χ
    r5 = B {(φ ∧ ψ) ∧ χ}{ψ}{χ → ψ ∧ χ} r4 r2
    -- (φ ∧ ψ) ∧ χ → χ → ψ ∧ χ
    r6 = S {(φ ∧ ψ) ∧ χ}{χ}{ψ ∧ χ}r5 r3
    -- (φ ∧ ψ) ∧ χ → ψ ∧ χ
    r7 = CI {φ}{ψ ∧ χ}
    -- φ → ψ ∧ χ → φ ∧ (ψ ∧ χ)
    r8 = B {(φ ∧ ψ) ∧ χ}{φ}{ψ ∧ χ → φ ∧ (ψ ∧ χ)}r7 r1
    -- (φ ∧ ψ) ∧ χ → ψ ∧ χ → φ ∧ (ψ ∧ χ)
    r9 = S {(φ ∧ ψ) ∧ χ}{ψ ∧ χ}{φ ∧ (ψ ∧ χ)} r8 r6
    -- (φ ∧ ψ) ∧ χ → φ ∧ (ψ ∧ χ)
  in
     CI {φ ∧ (ψ ∧ χ) → (φ ∧ ψ) ∧ χ} {((φ ∧ ψ) ∧ χ → φ ∧ (ψ ∧ χ))} l9 r9
-- S : (φ → ψ → χ) → (φ → ψ) → φ → χ
-- B : (ψ → χ) → (φ → ψ) → (φ → χ)
-- CI : φ → ψ → (φ ∧ ψ)


ex2 : {φ ψ χ : Set} → (φ ∨ (ψ ∨ χ)) ↔ ((φ ∨ ψ) ∨ χ)
ex2 {φ}{ψ}{χ} =
  let
    l1 = B {φ}{φ ∨ ψ}{(φ ∨ ψ) ∨ χ}(DI₁ {φ ∨ ψ}{χ}) (DI₁ {φ} {ψ})
    -- φ → (φ ∨ ψ) ∨ χ
    l2 = B {ψ}{φ ∨ ψ}{(φ ∨ ψ) ∨ χ}(DI₁ {φ ∨ ψ}{χ}) (DI₂ {φ} {ψ})
    -- ψ → (φ ∨ ψ) ∨ χ
    l3 = DI₂ {φ ∨ ψ}{χ}
    -- χ → (φ ∨ ψ) ∨ χ
    l4 = DE {ψ}{χ}{(φ ∨ ψ) ∨ χ}l2 l3
    -- ψ ∨ χ → (φ ∨ ψ) ∨ χ
    l5 = DE {φ}{ψ ∨ χ}{(φ ∨ ψ) ∨ χ}l1 l4
    -- φ ∨ (ψ ∨ χ) → (φ ∨ ψ) ∨ χ
    -- DE : (φ → χ) → (ψ → χ) → (φ ∨ ψ → χ)


    r1 = DI₁{φ}{ψ ∨ χ}
    -- φ → φ ∨ (ψ ∨ χ)
    r2 = B {ψ}{ψ ∨ χ}{φ ∨ (ψ ∨ χ)}(DI₂ {φ}{ψ ∨ χ}) (DI₁ {ψ}{χ})
    -- ψ → φ ∨ (ψ ∨ χ)
    r3 = B {χ}{ψ ∨ χ}{φ ∨ (ψ ∨ χ)}(DI₂ {φ}{ψ ∨ χ}) (DI₂ {ψ}{χ})
    -- χ → φ ∨ (ψ ∨ χ)
    r4 = DE {φ}{ψ}{φ ∨ (ψ ∨ χ)} r1 r2
    -- φ ∨ ψ → φ ∨ (ψ ∨ χ)
    r5 = DE {φ ∨ ψ}{χ}{φ ∨ (ψ ∨ χ)} r4 r3
    -- (φ ∨ ψ) ∨ χ → φ ∨ (ψ ∨ χ)
  in
    CI {φ ∨ (ψ ∨ χ) → (φ ∨ ψ) ∨ χ}{(φ ∨ ψ) ∨ χ → φ ∨ (ψ ∨ χ)} l5 r5
    -- (φ ∨ (ψ ∨ χ)) ↔ ((φ ∨ ψ) ∨ χ)
-- DI₁ : {φ ψ : Set} → φ → φ ∨ ψ
-- DE : {φ ψ χ : Set} → (φ → χ) → (ψ → χ) → (φ ∨ ψ → χ)

ex3 : {φ ψ : Set} → (φ ∧ ψ) ↔ (ψ ∧ φ)
ex3 {φ}{ψ} =
  let
    l1 = CI {ψ}{φ}
    -- ψ → φ → ψ ∧ φ
    l2 = CE₂ {φ}{ψ}
    -- φ ∧ ψ → ψ
    l3 = B {φ ∧ ψ}{ψ}{φ → ψ ∧ φ} l1 l2
    -- φ ∧ ψ → φ → ψ ∧ φ
    l4 = CE₁ {φ}{ψ}
    -- φ ∧ ψ → φ
    l5 = S {φ ∧ ψ}{φ}{ψ ∧ φ} l3 l4
    -- φ ∧ ψ → ψ ∧ φ

    r1 = CI {φ}{ψ}
    -- φ → ψ → φ ∧ ψ
    r2 = CE₂ {ψ}{φ}
    -- ψ ∧ φ → φ
    r3 = B {ψ ∧ φ}{φ}{ψ → φ ∧ ψ} r1 r2
    -- ψ ∧ φ → ψ → φ ∧ ψ
    r4 = CE₁ {ψ}{φ}
    -- ψ ∧ φ → ψ
    r5 = S {ψ ∧ φ}{ψ}{φ ∧ ψ} r3 r4
    -- ψ ∧ φ → φ ∧ ψ
  in
    CI {φ ∧ ψ → ψ ∧ φ}{ψ ∧ φ → φ ∧ ψ}l5 r5
    -- (φ ∧ ψ) ↔ (ψ ∧ φ)
-- B : (ψ → χ) → (φ → ψ) → (φ → χ)

ex4 : {φ ψ : Set} → (φ ∨ ψ) ↔ (ψ ∨ φ)
ex4 {φ}{ψ} =
  let
    l1 = DI₂ {ψ}{φ}
    -- φ → ψ ∨ φ
    l2 = DI₁ {ψ}{φ}
    -- ψ → ψ ∨ φ
    l3 = DE l1 l2
    -- φ ∨ ψ → ψ ∨ φ

    r1 = DI₁ {φ}{ψ}
    -- φ → φ ∨ ψ
    r2 = DI₂ {φ}{ψ}
    -- ψ → φ ∨ ψ
    r3 = DE r2 r1
    -- ψ ∨ φ → φ ∨ ψ
  in
    CI {φ ∨ ψ → ψ ∨ φ}{ψ ∨ φ → φ ∨ ψ} l3 r3
    -- (φ ∨ ψ) ↔ (ψ ∨ φ)
 -- DE : {φ ψ χ : Set} → (φ → χ) → (ψ → χ) → (φ ∨ ψ → χ)

ex5 : {φ : Set} → φ ↔ (φ ∧ φ)
ex5 {φ} =
  let
    l1 = CI {φ}{φ}
    -- φ → φ → φ ∧ φ
    l2 = I {φ}
    -- φ → φ
    l3 = S {φ}{φ}{φ ∧ φ}l1 l2
    -- φ → φ ∧ φ
    r1 = CE₁ {φ}{φ}
    -- φ ∧ φ → φ
  in
    CI {φ → φ ∧ φ}{φ ∧ φ → φ} l3 r1

ex6 : {φ : Set} → φ ↔ (φ ∨ φ)
ex6 {φ} =
  let
    l1 = DI₁ {φ}{φ}
    -- φ → φ ∨ φ
    r1 = DE {φ}{φ}{φ} (I {φ})(I {φ})
    -- φ ∨ φ → φ
  in
    CI {φ → φ ∨ φ}{φ ∨ φ → φ} l1 r1

ex7 : {φ ψ : Set} → φ ↔ (φ ∧ (φ ∨ ψ))
ex7 {φ}{ψ} =
  let
    l1 = CI {φ}{φ ∨ ψ}
    -- φ → φ ∨ ψ → φ ∧ (φ ∨ ψ)
    l2 = (DI₁ {φ}{ψ})
    -- φ → φ ∨ ψ
    l3 = S {φ}{φ ∨ ψ}{φ ∧ (φ ∨ ψ)} l1 l2
    -- φ → φ ∧ (φ ∨ ψ)
    r1 = CE₁ {φ}{φ ∨ ψ}
    -- φ ∧ (φ ∨ ψ) → φ
  in
    CI {φ → φ ∧ (φ ∨ ψ)}{φ ∧ (φ ∨ ψ) → φ}l3 r1

ex8 : {φ ψ : Set} → φ ↔ (φ ∨ (φ ∧ ψ))
ex8 {φ}{ψ} =
  let
    l1 = DI₁ {φ}{φ ∧ ψ}
    -- φ → φ ∨ (φ ∧ ψ)
    r1 = I {φ}
    -- φ → φ
    r2 = CE₁ {φ}{ψ}
    -- φ ∧ ψ → φ
    r3 = DE {φ}{φ ∧ ψ}{φ}r1 r2
    -- φ ∨ (φ ∧ ψ) → φ
  in
    CI {φ → φ ∨ (φ ∧ ψ)}{φ ∨ (φ ∧ ψ) → φ} l1 r3

-- 7.41
LNC : {φ : Set} → ¬ (φ ∧ ¬ φ)
LNC {φ} =
  let
    -- ¬ (φ ∧ ¬ φ)
    -- (φ ∧ ¬ φ) → ⊥
    p1 = CE₁ {φ}{¬ φ}
    -- φ ∧ ¬ φ → φ
    p2 = CE₂ {φ}{¬ φ}
    -- φ ∧ ¬ φ → ¬ φ
    -- = φ ∧ ¬ φ → φ → ⊥
    p3 = S {φ ∧ ¬ φ}{φ}{⊥}p2 p1
    -- φ ∧ ¬ φ → ⊥
  in
    p3

-- 8.4.3
Dist∧ : {φ ψ χ : Set} → (φ ∨ (ψ ∧ χ)) ↔ ((φ ∨ ψ) ∧ (φ ∨ χ))
Dist∧ {φ}{ψ}{χ} =
  let
    -- proof: (φ ∨ (ψ ∧ χ)) → ((φ ∨ ψ) ∧ (φ ∨ χ))
    l1 = DI₁ {φ}{ψ}
    -- φ → φ ∨ ψ
    l2 = CE₁ {ψ}{χ}
    -- ψ ∧ χ → ψ
    l3 = DI₂ {φ}{ψ}
    -- ψ → φ ∨ ψ
    l4 = B {ψ ∧ χ}{ψ}{φ ∨ ψ} l3 l2
    -- ψ ∧ χ → φ ∨ ψ
    l5 = DE {φ}{ψ ∧ χ}{φ ∨ ψ} l1 l4
    -- φ ∨ (ψ ∧ χ) → φ ∨ ψ

    l6 = DI₁ {φ}{χ}
    -- φ → φ ∨ χ
    l7 = B {ψ ∧ χ}{χ}{φ ∨ χ} (DI₂ {φ}{χ}) (CE₂ {ψ}{χ})
    -- ψ ∧ χ → φ ∨ χ
    l8 = DE {φ}{ψ ∧ χ} l6 l7
    -- φ ∨ (ψ ∧ χ) → φ ∨ χ

    l9 = CI {φ ∨ ψ} {φ ∨ χ}
    -- φ ∨ ψ → φ ∨ χ → (φ ∨ ψ) ∧ (φ ∨ χ)
    l10 = B {φ ∨ (ψ ∧ χ)}{φ ∨ ψ}{φ ∨ χ → (φ ∨ ψ) ∧ (φ ∨ χ)} l9 l5
    -- φ ∨ (ψ ∧ χ) → φ ∨ χ → (φ ∨ ψ) ∧ (φ ∨ χ)
    l11 = S {φ ∨ (ψ ∧ χ)}{φ ∨ χ}{(φ ∨ ψ) ∧ (φ ∨ χ)} l10 l8
    -- φ ∨ (ψ ∧ χ) → (φ ∨ ψ) ∧ (φ ∨ χ)

    -- ((φ ∨ ψ) ∧ (φ ∨ χ)) → (φ ∨ (ψ ∧ χ))
    r1 = CE₁ {φ ∨ ψ}{φ ∨ χ}
    -- (φ ∨ ψ) ∧ (φ ∨ χ) → φ ∨ ψ
    r2 = CE₂ {φ ∨ ψ}{φ ∨ χ}
    -- (φ ∨ ψ) ∧ (φ ∨ χ) → φ ∨ χ
    r3 = DI₁ {φ}{ψ ∧ χ}
    -- φ → φ ∨ (ψ ∧ χ)
    r4a = DE {φ}{ψ}{φ ∨ (ψ ∧ χ)}
    -- (φ → φ ∨ (ψ ∧ χ)) → (ψ → φ ∨ (ψ ∧ χ)) → φ ∨ ψ → φ ∨ (ψ ∧ χ)
    r4  = r4a r3
    -- (ψ → φ ∨ (ψ ∧ χ)) → φ ∨ ψ → φ ∨ (ψ ∧ χ)

    r5 = DI₁ {φ}{ψ ∧ χ}
    -- φ → φ ∨ (ψ ∧ χ)
    r6a = (K {φ → φ ∨ (ψ ∧ χ)}{ψ} r5)
    -- ψ → φ → φ ∨ (ψ ∧ χ)
    r6 = C {ψ}{φ}{φ ∨ (ψ ∧ χ)} r6a
    -- φ → ψ → φ ∨ (ψ ∧ χ)

    r7 = C {ψ}{χ}{ψ ∧ χ}(CI {ψ}{χ})
    -- χ → ψ → ψ ∧ χ
    r8 = DI₂ {φ}{ψ ∧ χ}
    -- ψ ∧ χ → φ ∨ (ψ ∧ χ)
    r9a = B {ψ}{ψ ∧ χ}{φ ∨ (ψ ∧ χ)}
    -- (ψ ∧ χ → φ ∨ (ψ ∧ χ)) → (ψ → ψ ∧ χ) → ψ → φ ∨ (ψ ∧ χ)
    r9  = r9a r8
    -- (ψ → ψ ∧ χ) → ψ → φ ∨ (ψ ∧ χ)
    -- r7: χ → (ψ → ψ ∧ χ)
    r10 = B {χ}{ψ → ψ ∧ χ}{ψ → φ ∨ (ψ ∧ χ)}r9 r7
    -- χ → ψ → φ ∨ (ψ ∧ χ)

    r11 = DE {φ}{χ}{ψ → φ ∨ (ψ ∧ χ)} r6 r10
    -- φ ∨ χ → ψ → φ ∨ (ψ ∧ χ)
    -- r2 : (φ ∨ ψ) ∧ (φ ∨ χ) → φ ∨ χ
    r12 = B {(φ ∨ ψ) ∧ (φ ∨ χ)}{φ ∨ χ}{ψ → φ ∨ (ψ ∧ χ)}r11 r2
    -- (φ ∨ ψ) ∧ (φ ∨ χ) → ψ → φ ∨ (ψ ∧ χ)
    r13 = B {(φ ∨ ψ) ∧ (φ ∨ χ)}{ψ → φ ∨ (ψ ∧ χ)}{φ ∨ ψ → φ ∨ (ψ ∧ χ)}r4 r12
    -- (φ ∨ ψ) ∧ (φ ∨ χ) → φ ∨ ψ → φ ∨ (ψ ∧ χ)
    -- r4: (ψ → φ ∨ (ψ ∧ χ)) → φ ∨ ψ → φ ∨ (ψ ∧ χ)

    -- r1: (φ ∨ ψ) ∧ (φ ∨ χ) → φ ∨ ψ
    r14 = S {(φ ∨ ψ) ∧ (φ ∨ χ)}{φ ∨ ψ}{φ ∨ (ψ ∧ χ)}r13 r1
    -- (φ ∨ ψ) ∧ (φ ∨ χ) → φ ∨ (ψ ∧ χ)
  in
    CI {φ ∨ (ψ ∧ χ) → (φ ∨ ψ) ∧ (φ ∨ χ)}{(φ ∨ ψ) ∧ (φ ∨ χ) → φ ∨ (ψ ∧ χ)} l11 r14


Dist∨ : {φ ψ χ : Set} → (φ ∧ (ψ ∨ χ)) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ))
Dist∨ {φ}{ψ}{χ} =
  let
    -- (φ ∧ (ψ ∨ χ)) → ((φ ∧ ψ) ∨ (φ ∧ χ))
    l1 = CE₁ {φ} {ψ ∨ χ}
    -- φ ∧ (ψ ∨ χ) → φ
    l2 = CE₂ {φ} {ψ ∨ χ}
    -- φ ∧ (ψ ∨ χ) → ψ ∨ χ
    l3 = C {φ}{ψ}{φ ∧ ψ}(CI {φ}{ψ})
    -- ψ → φ → φ ∧ ψ
    l4 = DI₁ {φ ∧ ψ}{φ ∧ χ}
    -- φ ∧ ψ → (φ ∧ ψ) ∨ (φ ∧ χ)
    l5 = B {ψ}{φ → φ ∧ ψ}{φ → (φ ∧ ψ) ∨ (φ ∧ χ)}
      (B{φ}{φ ∧ ψ}{(φ ∧ ψ) ∨ (φ ∧ χ)} l4) l3
    -- ψ → φ → (φ ∧ ψ) ∨ (φ ∧ χ)
    -- /χ → φ → (φ ∧ ψ) ∨ (φ ∧ χ)
    -- /ψ ∨ χ → φ → (φ ∧ ψ) ∨ (φ ∧ χ)

    l6 = C {φ}{χ}{φ ∧ χ}(CI {φ}{χ})
    -- χ → φ → φ ∧ χ
    l7 = DI₂ {φ ∧ ψ}{φ ∧ χ}
    -- φ ∧ χ → (φ ∧ ψ) ∨ (φ ∧ χ)
    l8 = B {χ}{φ → φ ∧ χ}{φ → (φ ∧ ψ) ∨ (φ ∧ χ)}
      (B {φ}{φ ∧ χ}{(φ ∧ ψ) ∨ (φ ∧ χ)}l7) l6
    -- χ → φ → (φ ∧ ψ) ∨ (φ ∧ χ)

    l9 = DE {ψ}{χ}{φ → (φ ∧ ψ) ∨ (φ ∧ χ)} l5 l8
    -- ψ ∨ χ → φ → (φ ∧ ψ) ∨ (φ ∧ χ)
    -- l1 φ ∧ (ψ ∨ χ) → φ
    -- l2 φ ∧ (ψ ∨ χ) → ψ ∨ χ
    l10 = B {φ ∧ (ψ ∨ χ)}{ψ ∨ χ}{φ → (φ ∧ ψ) ∨ (φ ∧ χ)}l9 l2
    -- φ ∧ (ψ ∨ χ) → φ → (φ ∧ ψ) ∨ (φ ∧ χ)
    l11 = S {φ ∧ (ψ ∨ χ)}{φ}{(φ ∧ ψ) ∨ (φ ∧ χ)}l10 l1
    -- φ ∧ (ψ ∨ χ) → (φ ∧ ψ) ∨ (φ ∧ χ)

    -- ((φ ∧ ψ) ∨ (φ ∧ χ)) → (φ ∧ (ψ ∨ χ))
    r1 = B (CI {φ}{ψ ∨ χ}) (CE₁{φ}{ψ})
    -- φ ∧ ψ → φ
    -- φ → ψ ∨ χ → φ ∧ (ψ ∨ χ)
    -- φ ∧ ψ → ψ ∨ χ → φ ∧ (ψ ∨ χ)
    r2 = B (DI₁ {ψ}{χ})(CE₂ {φ}{ψ})
    -- φ ∧ ψ → ψ ∨ χ
    r3 = S {φ ∧ ψ}{ψ ∨ χ}{φ ∧ (ψ ∨ χ)}r1 r2
    -- φ ∧ ψ → φ ∧ (ψ ∨ χ)
    r4 = B (CI {φ}{ψ ∨ χ}) (CE₁{φ}{χ})
    -- φ ∧ χ → ψ ∨ χ → φ ∧ (ψ ∨ χ)
    r5 = B (DI₂ {ψ}{χ})(CE₂ {φ}{χ})
    -- φ ∧ χ → ψ ∨ χ
    r6 = S {φ ∧ χ}{ψ ∨ χ}{φ ∧ (ψ ∨ χ)} r4 r5
    -- φ ∧ χ → φ ∧ (ψ ∨ χ)
    r7 = DE{φ ∧ ψ}{φ ∧ χ}{φ ∧ (ψ ∨ χ)} r3 r6
    -- (φ ∧ ψ) ∨ (φ ∧ χ) → φ ∧ (ψ ∨ χ)
  in
    CI l11 r7

DM∨ : {φ ψ : Set} → ¬ (φ ∨ ψ) ↔ ¬ φ ∧ ¬ ψ
DM∨ {φ}{ψ} =
  let
    -- Proof: ¬ (φ ∨ ψ) → ¬ φ ∧ ¬ ψ
    l1 = C⋆{φ ∨ ψ}{⊥}
    -- φ ∨ ψ → (φ ∨ ψ → ⊥) → ⊥
    -- φ → φ ∨ ψ
    -- ψ → φ ∨ ψ
    l2 = B {φ}{φ ∨ ψ}{¬ (φ ∨ ψ ) → ⊥} l1 (DI₁ {φ}{ψ})
    -- φ → ¬ (φ ∨ ψ) → ⊥
    l3 = C {φ}{¬ (φ ∨ ψ)}{⊥}l2
    -- ¬ (φ ∨ ψ) → φ → ⊥
    -- ¬ (φ ∨ ψ) → ¬ φ
    l4 = B {ψ}{φ ∨ ψ}{¬ (φ ∨ ψ ) → ⊥} l1 (DI₂ {φ}{ψ})
    -- ψ → ¬ (φ ∨ ψ) → ⊥
    l5 = C {ψ}{¬ (φ ∨ ψ)}{⊥}l4
    -- ¬ (φ ∨ ψ) → ψ → ⊥
    -- ¬ (φ ∨ ψ) → ¬ ψ
    l6 = CI {¬ φ}{¬ ψ}
    -- ¬ φ → ¬ ψ → ¬ φ ∧ ¬ ψ
    l7 = B {¬ (φ ∨ ψ)}{¬ φ}{¬ ψ → ¬ φ ∧ ¬ ψ}l6 l3
    -- ¬ (φ ∨ ψ) → ¬ ψ → ¬ φ ∧ ¬ ψ
    l8 = S {¬ (φ ∨ ψ)}{¬ ψ}{¬ φ ∧ ¬ ψ}l7 l5
    -- ¬ (φ ∨ ψ) → ¬ φ ∧ ¬ ψ

    -- Proof: ¬ φ ∧ ¬ ψ → ¬ (φ ∨ ψ)
    r1 = CE₁ {¬ φ}{¬ ψ}
    -- ¬ φ ∧ ¬ ψ → ¬ φ
    -- ¬ φ ∧ ¬ ψ → φ → ⊥
    r2 = C {¬ φ ∧ ¬ ψ}{φ}{⊥} r1
    -- φ → ¬ φ ∧ ¬ ψ → ⊥
    r3 = C {¬ φ ∧ ¬ ψ}{ψ}{⊥}(CE₂ {¬ φ}{¬ ψ})
    -- ψ → ¬ φ ∧ ¬ ψ → ⊥
    r4 = DE {φ}{ψ}{¬ φ ∧ ¬ ψ → ⊥} r2 r3
    -- φ ∨ ψ → ¬ φ ∧ ¬ ψ → ⊥
    r5 = C {φ ∨ ψ}{¬ φ ∧ ¬ ψ}{⊥}r4
    -- ¬ φ ∧ ¬ ψ → φ ∨ ψ → ⊥
  in
    CI {¬ (φ ∨ ψ) → ¬ φ ∧ ¬ ψ}{¬ φ ∧ ¬ ψ → ¬ (φ ∨ ψ)}l8 r5

DM∧₁ : {φ ψ : Set} → ¬ φ ∨ ¬ ψ → ¬ (φ ∧ ψ)
DM∧₁ {φ}{ψ} =
  let
    p1 = CE₁ {φ}{ψ}
    -- φ ∧ ψ → φ
    p2 = C⋆ {φ}{⊥}
    -- φ → (φ → ⊥) → ⊥
    p3 = B {φ ∧ ψ}{φ}{¬ φ → ⊥}p2 p1
    -- φ ∧ ψ → ¬ φ → ⊥
    p4 = B{φ ∧ ψ}{ψ}{¬ ψ → ⊥}(C⋆ {ψ}{⊥})(CE₂{φ}{ψ})
    -- φ ∧ ψ → ¬ ψ → ⊥
    p5 = C {φ ∧ ψ}{¬ φ}{⊥}p3
    -- ¬ φ → φ ∧ ψ → ⊥
    p6 = C {φ ∧ ψ}{¬ ψ}{⊥}p4
    -- ¬ ψ → φ ∧ ψ → ⊥
    p7 = DE {¬ φ}{¬ ψ}{φ ∧ ψ → ⊥}p5 p6
    -- ¬ φ ∨ ¬ ψ → φ ∧ ψ → ⊥
    -- ¬ φ ∨ ¬ ψ → ¬ φ ∧ ψ
  in
    p7

DM∧₂′ : {φ ψ : Set} → ¬ ¬ (φ ∧ ψ) → ¬ ¬ φ ∨ ¬ ¬ ψ
DM∧₂′ {φ}{ψ} =
  -- ((φ ∧ ψ → ⊥) → ⊥) → ((φ → ⊥) → ⊥) ∨ ((ψ → ⊥) → ⊥)
  let
    p1 = C⋆ {¬ (φ ∧ ψ)}{⊥}
    -- ¬ (φ ∧ ψ) → (¬ (φ ∧ ψ) → ⊥) → ⊥
    p2 = DM∧₁ {φ}{ψ}
    -- ¬ φ ∨ ¬ ψ → ¬ (φ ∧ ψ)
    p3 = B p1 p2
    -- ¬ φ ∨ ¬ ψ → (¬ (φ ∧ ψ) → ⊥) → ⊥
    p4 = C p3
    -- (¬ (φ ∧ ψ) → ⊥) → ¬ φ ∨ ¬ ψ → ⊥
    -- ¬ ¬ (φ ∧ ψ) → ¬ (¬ φ ∨ ¬ ψ)
    p5 = CE₁ (DM∨ {¬ φ}{¬ ψ})
    -- ¬ (¬ φ ∨ ¬ ψ) → ¬ (¬ φ) ∧ ¬ (¬ ψ)
    p6 = B p5 p4
    -- (¬ (φ ∧ ψ) → ⊥) → ¬ (¬ φ) ∧ ¬ (¬ ψ)
    p7 = CE₁ {¬ (¬ φ)}{¬ (¬ ψ)}
    -- ¬ (¬ φ) ∧ ¬ (¬ ψ) → ¬ (¬ φ)
    p8 = B (DI₁ {¬ (¬ φ)}{¬ (¬ ψ)}) p7
    -- ¬ (¬ φ) ∧ ¬ (¬ ψ) → ¬ (¬ φ) ∨ ¬ (¬ ψ)
    p9 = B p8 p6
  in
    p9
-- DM∨ : {φ ψ : Set} → ¬ (φ ∨ ψ) ↔ ¬ φ ∧ ¬ ψ
-- DM∧₁ : {φ ψ : Set} → ¬ φ ∨ ¬ ψ → ¬ (φ ∧ ψ)

-- (UI) ∀ζ(ψ → φ[ζ/ξ]) → (ψ → ∀ ξ φ)   (ζ ∉ fv(ψ) ∪ fv(∀ξφ))
-- (UE) ∀ξφ → φ[τ/ξ]
-- (EI) φ[τ/ξ] → ∃ξφ
-- (EE) ∀ζ(φ[ζ/ξ] → ψ) → (∃ξφ → ψ)   (ζ ∉ fv(ψ) ∪ fv(∃ξφ))
-- GEN φ[ζ/ξ]   ⇒   ∀ξφ   (ζ ∉ fv(前提) ∪ fv(∀ξφ))

-- 例. 7.49
-- ⊢ ∀ξ∀ζφ → ∀ζ∀ξφ
-- ∀ξ∀ζφ ⊢ ∀ζ∀ξφ を証明し、演繹定理を用いる
-- 1. ∀ξ∀ζφ   前提
-- 2. ∀ξ∀ζφ → (∀ζφ)[ξ/ξ]   UE{∀ζφ}
-- 3. ∀ζφ[ξ/ξ]     1, 2, MP
-- 4. ∀ζφ          3, 定理5.42(1)
-- 5. ∀ζφ → φ[ζ/ζ]   UE{φ}
-- 6. φ[ζ/ζ]       4, 5, MP
-- 7. φ[ξ/ξ]       6, 定理5.42(1)
-- 8. ∀ξφ          7, GEN, ξ ∉ fv(∀ξ∀ζφ) ∪ fv(∀ξφ)
-- 9. ∀ξφ[ζ/ζ]     8, 定理5.42(1)
-- 10 ∀ζξφ         9, GEN, ζ ∉ fv(∀ξ∀ζφ) ∪ fv(∀ζ∀ξφ)


-- 練習問題7.50
-- ⊢ ¬¬∀ξφ → ∀φ
-- ¬¬∀ξφ ⊢ ∀φ を証明し、演繹定理
-- 1. ¬¬∀ξφ  前提
--   (∀ξφ → ⊥) → ⊥
-- 2. ∀ξφ → φ[ξ/ξ]   UE
-- 3. ∀ξφ → φ        2, 定理5.42(1)
-- 4. φ → (φ → ⊥) → ⊥  C⋆
-- 5. ∀ξφ →  (φ → ⊥) → ⊥   B, 4, 3
-- 6. (φ → ⊥) → ∀ξφ → ⊥    C, 5
-- 7. (φ → ⊥) → ⊥      B, 1, 6
-- 8. ¬¬φ[ξ/ξ]         7, 定理5.42(1)
-- 9. ∀φ            8, GEN, ξ ∉ fv(¬¬∀ξφ) ∪ fv(∀φ)
--
-- ⊢ ∃ξ¬φ → ¬∀ξφ
-- 1. ∀ξ(¬φ[ξ/ξ] → ¬∀ξφ) → (∃ξ¬φ → ¬∀ξφ)  EE
-- 2. ∀ξ(¬φ → ¬∀ξφ) → (∃ξ¬φ → ¬∀ξφ)  1, 定理5.42(1)
-- 3. ∀ξφ → φ[ξ/ξ]        UE
-- 4. ∀ξφ → φ             3, 定理5.42(1)
-- 5. φ → (φ → ⊥) → ⊥     C⋆
-- 6. ∀ξφ → (φ → ⊥) → ⊥   B, 5, 4
-- 7. (φ → ⊥) → ∀ξφ → ⊥   C, 6
--    ¬φ → ¬∀ξφ
-- 8. (¬φ → ¬∀ξφ)[ξ/ξ]    7, 定理5.42(1)
-- 9. ∀ξ(¬φ → ¬∀ξφ)       8, GEN, ξ∉∀ξ(¬φ → ¬∀ξφ)
-- 10. ∃ξ¬φ → ¬∀ξφ        2, 9, MP

-- ⊢ ∀ξ¬φ → ¬∃ξφ
-- ∀ξ¬φ ⊢ ¬∃ξφ を証明し、演繹定理
-- 1. ∀ξ¬φ     前提
--      ∀ξ (φ → ⊥)
-- 2. ∀ξ(φ[ξ/ξ] → ⊥) → (∃ξφ → ⊥)   EE, ξ∉fv(⊥)∪fv(∃ξφ)
-- 3. ∀ξ(φ[ξ/ξ] → ⊥)     1, 定理5.42(1)
-- 4. ∃ξφ → ⊥            2, 3, MP
--    ¬∃ξφ

-- ⊢ ¬∃ξφ → ∀ξ¬φ
-- ¬∃ξφ ⊢ ∀ξ¬φ を証明し、演繹定理
-- 1. ¬∃ξφ       前提
-- ∃ξφ → ⊥
-- 2. φ[ξ/ξ] → ∃ξφ   EI
-- 3. φ → ∃ξφ        2, 定理5.42(1)
-- 4. φ → ⊥          B, 2, 1
-- 5, ¬φ[ξ/ξ]        4, 定理5.42(1)
-- 6. ∀ξ¬φ           5, GEN, ξ∉fv(¬∃ξφ)∪fv(∀ξ¬φ)

module hj where
EFQ : {φ : Set} → ⊥ → φ
EFQ ()

ex7531 : {φ ψ : Set} → (¬ φ ∨ ψ) → φ → ψ
ex7531 {φ}{ψ} =
  let
    p1 = C⋆ {φ}{⊥}
    -- φ → (φ → ⊥) → ⊥
    p2 = C{φ}{¬ φ}{⊥} p1
    -- ¬ φ → φ → ⊥
    p3 = EFQ {ψ}
    -- ⊥ → ψ
    p4 = B {φ}{⊥}{ψ}p3
    -- (φ → ⊥) → φ → ψ
    p5 = B p4 p2
    -- ¬ φ → φ → ψ

    p6 = K{ψ}{φ}
    -- ψ → φ → ψ
    p7 = DE{¬ φ}{ψ}{φ → ψ} p5 p6
  in
    p7

ex7532 : {φ ψ : Set} → (¬ ¬ φ → ¬ ¬ ψ) → ¬ ¬ (φ → ψ)
  -- (¬ ¬ φ → ¬ ¬ ψ) → ¬ (φ → ψ) → ⊥
ex7532 {φ}{ψ} p q =
  let
    p1 = p
    -- ¬ ¬ φ → ¬ ¬ ψ
    p2 = q
    -- ¬ (φ → ψ)
    p3 = C⋆ {φ}{⊥}
    -- φ → (φ → ⊥) → ⊥
    p4 = EFQ {ψ}
    -- ⊥ → ψ
    p5 = B {(φ → ⊥)}{⊥}{ψ} p4
    -- ((φ → ⊥) → ⊥) → (φ → ⊥) → ψ
    p6 = B {φ}{¬ ¬ φ}{(φ → ⊥) → ψ}p5 p3
    -- φ → (φ → ⊥) → ψ
    p7 = C {φ}{φ → ⊥}{ψ}p6
    -- (φ → ⊥) → φ → ψ
    p8 = B {¬ φ}{φ → ψ}{⊥}p2 p7
    -- (φ → ⊥) → ⊥
    -- ¬ ¬ φ
    p9 = p1 p8
    -- ¬ (¬ ψ)
    p10 = K {ψ}{φ}
    -- ψ → φ → ψ
    p11 = B p2 p10
    -- ψ → ⊥
    p12 = p9 p11
  in
    p12

-- f g = f (λ x → g (λ p → ⊥-elim (x p))) (λ q → g (λ x → q))