Hilbert system formalization in Agda

Hilbert.agda

module Hilbert where

-- postulate
--   Identifier : Set
--   a b c x y z : Identifier
--   bot : Identifier

infixr 4 _=>_

data Expression : Set where
  -- atom : Identifier → Expression
  _=>_ : Expression → Expression → Expression

variable
  -- A B C X Y Z : Expression
  α β γ δ φ ψ ξ : Expression

postulate
  ⊥ : Expression

infix 7 ¬_
¬_ : Expression → Expression
¬ E = E => ⊥

infixr 5 _∨_
_∨_ : Expression → Expression → Expression
E ∨ F = ¬ E => F

infixr 6 _∧_
_∧_ : Expression → Expression → Expression
E ∧ F = ¬ (¬ E ∨ ¬ F)


-- Based on: https://en.wikipedia.org/wiki/Hilbert_system#Logical_axioms

data Tautology : Expression → Set where
  -- Axioms
  -- A₁ : (φ : Expression) → Tautology (φ => φ)
  A₂ : (φ ψ : Expression) → Tautology (φ => (ψ => φ))
  A₃ : (φ ψ ξ : Expression) → Tautology ((φ => (ψ => ξ)) => ((φ => ψ) => (φ => ξ)))
  A₄ : (φ ψ : Expression) → Tautology ((¬ φ => ¬ ψ) => (ψ => φ))
  -- Modus Ponens
  MP : {φ ψ : Expression} → Tautology φ → Tautology (φ => ψ) → Tautology ψ

A₁ : (φ : Expression) → Tautology (φ => φ)
A₁ φ = t₅
  where
    t₁ : Tautology (φ => (φ => φ) => φ)
    t₁ = A₂ φ (φ => φ)

    t₂ : Tautology (φ => φ => φ)
    t₂ = A₂ φ φ

    t₃ : Tautology ((φ => (φ => φ) => φ) => (φ => φ => φ) => φ => φ)
    t₃ = A₃ φ (φ => φ) φ

    t₄ : Tautology ((φ => φ => φ) => φ => φ)
    t₄ = MP t₁ t₃

    t₅ : Tautology (φ => φ)
    t₅ = MP t₂ t₄


-- Equivalence / Deduction theorem

-- from-meta : (Tautology α → Tautology β) → Tautology (α => β)
-- from-meta {α} {β} f = {!-c !}

to-meta : Tautology (α => β) → (Tautology α → Tautology β)
to-meta Tα=>β Tα = MP Tα Tα=>β


-- Extra lemmas

prepend-meta : (α : Expression) → Tautology β → Tautology (α => β)
prepend-meta {β} α Tβ = MP Tβ (A₂ β α)


-- insert-meta : (α β γ : Expression) → Tautology (α => γ) → Tautology (α => β => γ)
insert-meta : (β : Expression) → Tautology (α => γ) → Tautology (α => β => γ)
-- insert-meta α β γ Tα=>γ = MP Tα=>γ (MP (MP (A₂ γ β) (A₂ (γ => β => γ) α)) (A₃ α γ (β => γ)))
insert-meta {α} {γ} β Tα=>γ = t₆
  where
    t₁ : Tautology ((α => γ => β => γ) => (α => γ) => α => β => γ)
    t₁ = A₃ α γ (β => γ)

    t₂ : Tautology ((γ => β => γ) => α => γ => β => γ)
    t₂ = A₂ (γ => β => γ) α

    t₃ : Tautology (γ => β => γ)
    t₃ = A₂ γ β

    t₄ : Tautology (α => γ => β => γ)
    t₄ = MP t₃ t₂
    -- t₄ = prepend-meta α (A₂ γ β)

    t₅ : Tautology ((α => γ) => α => β => γ)
    t₅ = MP t₄ t₁

    t₆ : Tautology (α => β => γ)
    t₆ = MP Tα=>γ t₅

-- lift :

reorder : Tautology ((α => β => γ) => (β => α => γ))
reorder {α} {β} {γ} = t₈
  where
    H = (α => β => γ)

    t₀ : Tautology (H => H)
    t₀ = A₁ H

    t₁ : Tautology (H => ((α => β) => α => γ) => β => (α => β) => α => γ)
    -- t₁ = MP (A₂ ((α => β) => α => γ) β) (A₂ (((α => β) => α => γ) => β => (α => β) => α => γ) H)
    t₁ = MP (A₂ ((α => β) => α => γ) β) (A₂ _ _)

    t₂ : Tautology (H => (α => β => γ) => (α => β) => α => γ)
    t₂ = MP (A₃ α β γ) (A₂ _ _)

    t₃ : Tautology (H => (β => (α => β) => α => γ) => (β => α => β) => β => α => γ)
    t₃ = MP (A₃ β (α => β) (α => γ)) (A₂ _ _)

    t₄ : Tautology (H => (α => β) => α => γ)
    t₄ = MP t₀ (MP t₂ (A₃ _ _ _))

    t₅ : Tautology (H => β => (α => β) => α => γ)
    t₅ = MP t₄ (MP t₁ (A₃ _ _ _))

    t₆ : Tautology (H => (β => α => β) => β => α => γ)
    t₆ = MP t₅ (MP t₃ (A₃ _ _ _))

    t₇ : Tautology (H => β => α => β)
    t₇ = MP (A₂ β α) (A₂ _ _)

    t₈ : Tautology (H => β => α => γ)
    t₈ = MP t₇ (MP t₆ (A₃ _ _ _))

reorder-meta : Tautology (α => β => γ) → Tautology (β => α => γ)
-- reorder-meta Tα=>β=>γ = MP (A₂ β α)
--                      (MP (MP (MP Tα=>β=>γ (A₃ α β γ)) (A₂ ((α => β) => α => γ) β))
--                       (A₃ β (α => β) (α => γ)))
reorder-meta {α} {β} {γ} Tα=>β=>γ = t₈
  where
    t₁ : Tautology (((α => β) => α => γ) => β => (α => β) => α => γ)
    t₁ = A₂ ((α => β) => α => γ) β

    t₂ : Tautology ((α => β => γ) => (α => β) => α => γ)
    t₂ = A₃ α β γ

    t₃ : Tautology ((β => (α => β) => α => γ) => (β => α => β) => β => α => γ)
    t₃ = A₃ β (α => β) (α => γ)

    t₄ : Tautology ((α => β) => α => γ)
    t₄ = MP Tα=>β=>γ (t₂)

    t₅ : Tautology (β => (α => β) => α => γ)
    t₅ = MP t₄ t₁

    t₆ : Tautology ((β => α => β) => β => α => γ)
    t₆ = MP t₅ t₃

    t₇ : Tautology (β => α => β)
    t₇ = A₂ β α

    t₈ : Tautology (β => α => γ)
    t₈ = MP t₇ t₆

-- replace-meta : Tautology (β => γ) → Tautology (α => β) → Tautology (α => γ)
-- replace-meta = {!!}

insert-meta' : (β : Expression) → Tautology (α => γ) → Tautology (α => β => γ)
insert-meta' β Tα=>γ = reorder-meta (prepend-meta β Tα=>γ)

syllogism : Tautology ((α => β) => (β => γ) => (α => γ))
-- syllogism {α} {β} {γ} = reorder-meta (MP (A₂ (β => γ) α)
--                        (MP
--                         (MP (A₃ α β γ) (A₂ ((α => β => γ) => (α => β) => α => γ) (β => γ)))
--                         (A₃ (β => γ) (α => β => γ) ((α => β) => α => γ))))
syllogism {α} {β} {γ} = reorder-meta t₆
  where
    t₁ : Tautology
           (((β => γ) => (α => β => γ) => (α => β) => α => γ) =>
            ((β => γ) => α => β => γ) => (β => γ) => (α => β) => α => γ)
    t₁ = A₃ (β => γ) (α => β => γ) ((α => β) => α => γ)

    t₂ : Tautology
           (((α => β => γ) => (α => β) => α => γ) =>
            (β => γ) => (α => β => γ) => (α => β) => α => γ)
    t₂ = A₂ ((α => β => γ) => (α => β) => α => γ) (β => γ)

    t₃ : Tautology ((β => γ) => (α => β => γ) => (α => β) => α => γ)
    t₃ = MP (A₃ α β γ) t₂

    t₄ : Tautology (((β => γ) => α => β => γ) => (β => γ) => (α => β) => α => γ)
    t₄ = MP t₃ t₁

    t₅ : Tautology ((β => γ) => α => β => γ)
    t₅ = A₂ (β => γ) α

    t₆ : Tautology ((β => γ) => (α => β) => α => γ)
    t₆ = MP t₅ t₄

syllogism-meta : Tautology (α => β) → Tautology (β => γ) → Tautology (α => γ)
-- syllogism-meta {α} {β} {γ} Tα=>β Tβ=>γ = MP Tα=>β (MP (MP Tβ=>γ (A₂ (β => γ) α)) (A₃ α β γ))
-- syllogism-meta {α} {β} {γ} Tα=>β = to-meta (to-meta {α => β} {(β => γ) => (α => γ)} syllogism Tα=>β)
syllogism-meta {α} {β} {γ} Tα=>β = to-meta (to-meta syllogism Tα=>β)

mp : Tautology (α => (α => β) => β)
mp {α} {β} = t₇
  where
    t₁ : Tautology ((α => β) => (α => β))
    t₁ = A₁ (α => β)

    t₂ : Tautology (((α => β) => α => β) => ((α => β) => α) => (α => β) => β)
    t₂ = A₃ (α => β) α β

    t₃ : Tautology (α => (α => β) => α)
    t₃ = A₂ α (α => β)

    t₄ : Tautology (((α => β) => α) => (α => β) => β)
    t₄ = MP t₁ t₂

    -- t₅ : {!Tautology ((β => γ) => (α => β) => (α => γ))!}
    -- t₅ = reorder-meta syllogism

    t₅ : Tautology ((((α => β) => α) => ((α => β) => β)) => (α => ((α => β) => α)) => (α => ((α => β) => β)))
    t₅ = reorder-meta (syllogism {α} {(α => β) => α} {(α => β) => β})
    -- t₅ = reorder-meta (A₂ (α => (α => β) => β) (((α => β) => β) => (α => β) => β))

    t₆ : Tautology ((α => (α => β) => α) => α => (α => β) => β)
    t₆ = MP t₄ t₅

    t₇ : Tautology (α => (α => β) => β)
    t₇ = MP t₃ t₆

-- syllogism-4 : Tautology ((α => β => γ) => (γ => δ) => (α => β => δ))
-- syllogism-4 {α} {β} {γ} {δ} = {!reorder-meta syllogism -t 120!}
  -- where
  --   t₁ : Tautology (((α => β) => γ) => (γ => δ) => (α => β) => δ)
  --   t₁ = syllogism {α => β} {γ} {δ}

    -- t₂ : Tautology ((α => β => γ) => (γ => δ) => (α => β) => δ)
    -- t₂ = syllogism-meta {α => β => γ} {((α => β) => γ)} {(γ => δ) => (α => β) => δ} {!!} t₁

    -- t₃ : {!!}
    -- t₃ = {!!}

    -- t₄ : {!!}
    -- t₄ = {!!}

    -- t₅ : {!!}
    -- t₅ = {!!}

    -- tₙ : {!!}
    -- tₙ = {!!}


syllogism-4-meta : Tautology (α => β => γ) → Tautology (γ => δ) → Tautology (α => β => δ)
syllogism-4-meta {α} {β} {γ} {δ} Tα=>β=>γ Tγ=>δ =
  MP Tα=>β=>γ (MP (MP (MP (MP Tγ=>δ (A₂ (γ => δ) β)) (A₃ β γ δ)) (A₂ ((β => γ) => β => δ) α)) (A₃ α (β => γ) (β => δ)))

-- BOT / NOT Eliminator

⊥-elim : Tautology (⊥ => α)
⊥-elim {α} = MP (MP (MP (MP (A₂ ⊥ ⊥) (A₃ ⊥ ⊥ ⊥)) (A₄ ⊥ ⊥)) (A₂ (⊥ => ⊥) (α => ⊥))) (A₄ α ⊥)

-- ⊥-elim : Tautology ((α => ⊥) => α => β)
-- ⊥-elim {α} {β} = MP (A₂ (α => ⊥) (β => ⊥))
--            (MP (MP (A₄ β α) (A₂ (((β => ⊥) => α => ⊥) => α => β) (α => ⊥)))
--             (A₃ (α => ⊥) ((β => ⊥) => α => ⊥) (α => β)))

-- both : Tautology ((α => β) => (¬ α => β) => β)
-- both = {!!}

double-¬-intro : Tautology (α => ¬ ¬ α)
double-¬-intro = mp

double-¬-elim : Tautology (¬ ¬ α => α)
double-¬-elim {α} = t₃
  where
    t₁ : Tautology ((α => ⊥) => ((α => ⊥) => ⊥) => ⊥)
    t₁ = mp

    t₂ : Tautology (((α => ⊥) => ((α => ⊥) => ⊥) => ⊥) => ((α => ⊥) => ⊥) => α)
    t₂ = A₄ α (¬ ¬ α)

    t₃ : Tautology (¬ ¬ α => α)
    t₃ = MP t₁ t₂

-- NOT Introduction

¬-intro : Tautology ((α => β) => ((α => ¬ β) => ¬ α))
-- ¬-intro {α} {β} = MP (A₂ (α => β) (α => β => ⊥))
--             (MP
--              (MP (MP (A₃ α β ⊥) (A₃ (α => β => ⊥) (α => β) (α => ⊥)))
--               (A₂ (((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥) (α => β)))
--              (A₃ (α => β) ((α => β => ⊥) => α => β) ((α => β => ⊥) => α => ⊥)))
¬-intro {α} {β} = t₉
  where
    t₁ : Tautology
           (((α => β) => ((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥) =>
            ((α => β) => (α => β => ⊥) => α => β) => (α => β) => (α => β => ⊥) => α => ⊥)
    t₁ = A₃ (α => β) ((α => β => ⊥) => α => β) ((α => β => ⊥) => α => ⊥)

    t₂ : Tautology
           ((((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥) =>
            (α => β) => ((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥)
    t₂ = A₂ (((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥) (α => β)

    t₃ : Tautology
           (((α => β => ⊥) => (α => β) => α => ⊥) =>
            ((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥)
    t₃ = A₃ (α => β => ⊥) (α => β) (α => ⊥)

    t₄ : Tautology ((α => β => ⊥) => (α => β) => α => ⊥)
    t₄ = A₃ α β ⊥

    t₅ : Tautology (((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥)
    t₅ = MP t₄ t₃

    t₆ : Tautology
           ((α => β) => ((α => β => ⊥) => α => β) => (α => β => ⊥) => α => ⊥)
    t₆ = MP t₅ t₂

    t₇ : Tautology
           (((α => β) => (α => β => ⊥) => α => β) =>
            (α => β) => (α => β => ⊥) => α => ⊥)
    t₇ = MP t₆ t₁

    t₈ : Tautology ((α => β) => (α => β => ⊥) => α => β)
    t₈ = A₂ (α => β) (α => β => ⊥)

    t₉ : Tautology ((α => β) => (α => β => ⊥) => α => ⊥)
    t₉ = MP t₈ t₇


-- ¬-elim : Tautology ((¬ α => β) => ((¬ α => ¬ β) => α))
-- ¬-elim {α} {β} = {!!}
  -- where
  --   -- t₁ : {!!}
  --   -- t₁ = {!!}

  --   -- t₂ : {!!}
  --   -- t₂ = {!!}

  --   t₃ : {!!}
  --   t₃ = {!¬-intro {¬ α} {β}!}

  --   -- t₄ : {!!}
  --   -- t₄ = {!!}

  --   -- t₅ : {!!}
  --   -- t₅ = {!!}

  --   -- tₙ : {!!}
  --   -- tₙ = {!!}

-- OR

-- ∨-commutative : Tautology (α ∨ β => β ∨ α)
-- ∨-commutative {α} {β} = {!!}

∨-left : Tautology (α => (α ∨ β))
-- ∨-left {α} {β} = reorder-meta ⊥-elim
∨-left {α} {β} = syllogism-4-meta (mp {α} {⊥}) ⊥-elim
  -- tₙ
  -- where
  --   t₁ : Tautology (((((α => ⊥) => β) => ⊥) => α => ⊥) => α => (α => ⊥) => β)
  --   t₁ = A₄ ((α => ⊥) => β) α

  --   t₂ : Tautology (((α => ⊥) => β) => α => (α => ⊥) => β)
  --   t₂ = A₂ ((α => ⊥) => β) α

  --   t₃ : Tautology (¬ (¬ α => β) => ¬ α)
  --   -- t₃ : Tautology ((((α => ⊥) => β) => ⊥) => α => ⊥)
  --   t₃ = {!!}

  --   tₙ : Tautology (α => (α => ⊥) => β)
  --   tₙ = MP t₃ t₁

∨-right : Tautology (β => (α ∨ β))
∨-right {β} {α} = A₂ β (α => ⊥)

-- ∨-elim : Tautology ((α => γ) => (β => γ) => (α ∨ β) => γ)
-- -- ∨-elim : Tautology ((α ∨ β) => (α => γ) => (β => γ) => γ)
-- ∨-elim = {!!}


-- AND

-- α => ⊥/¬ a

-- ∧-intro : Tautology (α => β => ¬(¬ α ∨ ¬ β))
∧-intro-meta : Tautology α → Tautology β → Tautology (α ∧ β)
-- ∧-intro-meta {α} {β} Tα Tβ =
--                    MP (MP Tα (A₂ α (((α => ⊥) => ⊥) => β => ⊥)))
--                    (MP (MP Tβ (reorder-meta (A₄ (α => ⊥) β)))
--                     (A₃ (((α => ⊥) => ⊥) => β => ⊥) α ⊥))
∧-intro-meta {α} {β} Tα Tβ = t₇
  where
    -- t₁ :
           -- (((((α => ⊥) => ⊥) => β => ⊥) => α => ⊥) =>
           --  ((((α => ⊥) => ⊥) => β => ⊥) => α) =>
           --  (((α => ⊥) => ⊥) => β => ⊥) => ⊥)
    -- t₁ = A₃ (((α => ⊥) => ⊥) => β => ⊥) α ⊥
    t₁ : Tautology (((¬ ¬ α => ¬ β) => ¬ α) => ((¬ ¬ α => ¬ β) => α) => ¬ (¬ ¬ α => ¬ β))
    t₁ = A₃ (¬ ¬ α => ¬ β) α ⊥

    t₂ : Tautology (β => (((α => ⊥) => ⊥) => β => ⊥) => α => ⊥)
    t₂ = reorder-meta (A₄ (α => ⊥) β)

    t₃ : Tautology (α => (((α => ⊥) => ⊥) => β => ⊥) => α)
    t₃ = A₂ α (((α => ⊥) => ⊥) => β => ⊥)

    t₄ : Tautology ((((α => ⊥) => ⊥) => β => ⊥) => α => ⊥)
    t₄ = MP Tβ t₂

    t₅ : Tautology (((((α => ⊥) => ⊥) => β => ⊥) => α) => (((α => ⊥) => ⊥) => β => ⊥) => ⊥)
    t₅ = MP t₄ t₁

    t₆ : Tautology ((((α => ⊥) => ⊥) => β => ⊥) => α)
    t₆ = MP Tα t₃

    t₇ : Tautology ((((α => ⊥) => ⊥) => β => ⊥) => ⊥)
    t₇ = MP t₆ t₅


∧-intro : Tautology (α => β => (α ∧ β))
∧-intro {α} {β} = t₇
  where
    tβ : Tautology (β => β)
    tβ = A₁ β

    t₁ : Tautology (β => ((¬ ¬ α => ¬ β) => ¬ α) => ((¬ ¬ α => ¬ β) => α) => ¬ (¬ ¬ α => ¬ β))
    t₁ = MP (A₃ (¬ ¬ α => ¬ β) α ⊥) (A₂ _ _)

    t₂ : Tautology (β => β => (¬ ¬ α => ¬ β) => ¬ α)
    t₂ = MP (reorder-meta (A₄ (¬ α) β)) (A₂ _ _)

    t₃'' : Tautology (β => α => (¬ ¬ α => ¬ β) => α)
    t₃'' = MP (A₂ α ((¬ (¬ α)) => ¬ β)) (A₂ _ _)

    t₄ : Tautology (β => (¬ ¬ α => ¬ β) => ¬ α)
    t₄ = MP tβ (MP t₂ (A₃ _ _ _))

    t₅'' : Tautology (β => ((¬ ¬ α => ¬ β) => α) => ¬ (¬ ¬ α => ¬ β))
    t₅'' = MP t₄ (MP t₁ (A₃ _ _ _))

    -- α =>

    tα : Tautology (α => β => α)
    tα = A₂ α β

    tβ' : Tautology (α => β => β)
    tβ' = MP tβ (A₂ _ _)

    t₃' : Tautology ((β => α) => β => (¬ ¬ α => ¬ β) => α)
    t₃' = MP t₃'' (A₃ _ _ _)

    t₃ : Tautology (α => (β => α) => β => (¬ ¬ α => ¬ β) => α)
    t₃ = MP t₃' (A₂ _ _)
    -- t₃ = MP
    --        (MP
    --         (MP (A₂ α (((α => ⊥) => ⊥) => β => ⊥))
    --          (A₂ (α => (((α => ⊥) => ⊥) => β => ⊥) => α) β))
    --         (A₃ β α ((((α => ⊥) => ⊥) => β => ⊥) => α)))
    --        (A₂ ((β => α) => β => (((α => ⊥) => ⊥) => β => ⊥) => α) α)

    t₅' : Tautology ((β => (((α => ⊥) => ⊥) => β => ⊥) => α) => β => (((α => ⊥) => ⊥) => β => ⊥) => ⊥)
    t₅' = MP t₅'' (A₃ _ _ _)

    t₅ : Tautology (α => (β => (¬ ¬ α => ¬ β) => α) => β => ¬ (¬ ¬ α => ¬ β))
    t₅ = MP t₅' (A₂ _ _)

    t₆ : Tautology (α => β => (¬ ¬ α => ¬ β) => α)
    t₆ = MP tα (MP t₃ (A₃ _ _ _))

    t₇ : Tautology (α => β => ¬ ((¬ (¬ α)) => ¬ β))
    t₇ = MP t₆ (MP t₅ (A₃ α (β => ((¬ ¬ α => ¬ β) => α)) (β => (¬ (¬ ¬ α => ¬ β)))))

-- ∧-left : Tautology ((α ∧ β) => α)
-- ∧-left = {!!}

-- ∧-right : Tautology ((α ∧ β) => β)
-- ∧-right = {!!}



-- test : Tautology ()
-- test = {!!}
  -- where
  --   t₁ : {!!}
  --   t₁ = {!!}

  --   t₂ : {!!}
  --   t₂ = {!!}

  --   t₃ : {!!}
  --   t₃ = {!!}

  --   t₄ : {!!}
  --   t₄ = {!!}

  --   t₅ : {!!}
  --   t₅ = {!!}

  --   tₙ : {!!}
  --   tₙ = {!!}


-- Random

test : Tautology (α => β => β => α)
test {α} {β} = insert-meta β (A₂ α β)
  -- MP
  --   (A₂ α β)
  --   (MP
  --     (MP
  --       (A₂ (β => α) β)
  --       (A₂ ((β => α) => β => β => α) α)
  --     )
  --     (A₃ α (β => α) (β => β => α))
  --   )