import Mathlib.Data.Set.Basic

/-!
本文件形式化并证明：

  `Γ ⊢ α` 当且仅当 `Γ ∪ {¬α}` 不一致。

这里采用一个只含矛盾常元、否定和 `→` 的经典 Hilbert 系统。
矛盾常元用对象语言符号 `異議あり！` 表示。
一致性按题目定义为：`Consistent Γ` 当且仅当 `¬ Γ ⊢ 異議あり！`。
-/

namespace Consistency

/-- 命题公式。这里只保留本定理需要的联结词。 -/
inductive WFF : Type
  | p_atm : String → WFF
  | p_contra : WFF
  | p_not : WFF → WFF
  | p_imp : WFF → WFF → WFF

open WFF

infixr:60 " -> " => WFF.p_imp
notation "異議あり！" => WFF.p_contra

/-- 对象语言中的否定联结词。 -/
def not (α : WFF) : WFF := WFF.p_not α

/--
Hilbert 公理系统：

* `K`、`S` 是蕴含片段的标准 Hilbert 公理；
* `Ax10`、`Ax13`、`Ax14` 分别对应教材中的公理 1.22.10、
  1.22.13、1.22.14。
-/
inductive IsAxiom : WFF → Prop
  | K (α β : WFF) : IsAxiom (α -> (β -> α))
  | S (α β γ : WFF) :
      IsAxiom ((α -> (β -> γ)) -> ((α -> β) -> (α -> γ)))
  | Ax10 (α : WFF) : IsAxiom ((not α) -> (α -> 異議あり！))
  | Ax13 (α : WFF) : IsAxiom (((not α) -> 異議あり！) -> (not (not α)))
  | Ax14 (α : WFF) : IsAxiom ((not (not α)) -> α)

/-- `Γ |- φ` 表示公式 `φ` 可由前提集 `Γ` 推出。 -/
inductive Derivable (Γ : Set WFF) : WFF → Prop
  | hyp {φ : WFF} : φ ∈ Γ → Derivable Γ φ
  | axm {φ : WFF} : IsAxiom φ → Derivable Γ φ
  | mp  {φ ψ : WFF} : Derivable Γ φ → Derivable Γ (φ -> ψ) → Derivable Γ ψ

notation:50 Γ " |- " φ => Derivable Γ φ

/-- 一致性：`Γ` 不推出矛盾常元 `異議あり！`。 -/
def Consistent (Γ : Set WFF) : Prop := ¬ Γ |- 異議あり！

/-- 不一致：`Γ` 推出矛盾常元 `異議あり！`。 -/
def Inconsistent (Γ : Set WFF) : Prop := Γ |- 異議あり！

theorem lemma_1_24 {Γ : Set WFF} {α β : WFF} :
    (Γ |- α) → (Γ |- (α -> β)) → (Γ |- β) := by
  intro hα hαβ
  exact Derivable.mp hα hαβ

/--
`⊢` 对前提集的单调性作为已经成立的结论使用：
若 `Γ ⊢ φ`，则加入任意一组新前提后仍有 `Γ ∪ Δ ⊢ φ`。
-/
axiom monotonicity_union {Γ Δ : Set WFF} {φ : WFF} :
    (Γ |- φ) → (Γ ∪ Δ |- φ)

/-- 自反性：前提集中的公式可由该前提集推出。 -/
theorem derivable_self {Γ : Set WFF} {φ : WFF} (hφ : φ ∈ Γ) : Γ |- φ :=
  Derivable.hyp hφ

/--
演绎定理作为已经成立的结论使用：
`Γ ∪ {α} ⊢ β` 当且仅当 `Γ ⊢ α → β`。
-/
axiom deduction_theorem {Γ : Set WFF} {α β : WFF} :
    (((Γ ∪ ({α} : Set WFF)) |- β) ↔ (Γ |- (α -> β)))

/--
题目要求的形式：

`Γ ⊢ α` 当且仅当 `Γ ∪ {¬α}` 不一致。
-/
theorem derivable_iff_inconsistent_union_not {Γ : Set WFF} {α : WFF} :
    (Γ |- α) ↔ Inconsistent (Γ ∪ ({not α} : Set WFF)) := by
  unfold Inconsistent
  let Δ : Set WFF := Γ ∪ ({not α} : Set WFF)
  constructor
  case mp =>
    intro hα
    have hα' : Δ |- α :=
      monotonicity_union hα
    have hnot : Δ |- not α :=
      derivable_self (Or.inr rfl)
    have hAx10 : Δ |- ((not α) -> (α -> 異議あり！)) :=
      Derivable.axm (IsAxiom.Ax10 α)
    have hαToContra : Δ |- (α -> 異議あり！) :=
      lemma_1_24 hnot hAx10
    exact lemma_1_24 hα' hαToContra
  case mpr =>
    intro hContra
    have hNotToContra : Γ |- ((not α) -> 異議あり！) :=
      (deduction_theorem.mp hContra)
    have hAx13 : Γ |- (((not α) -> 異議あり！) -> (not (not α))) :=
      Derivable.axm (IsAxiom.Ax13 α)
    have hNegNeg : Γ |- not (not α) :=
      lemma_1_24 hNotToContra hAx13
    have hAx14 : Γ |- ((not (not α)) -> α) :=
      Derivable.axm (IsAxiom.Ax14 α)
    exact lemma_1_24 hNegNeg hAx14

/--
由“不一致”可立即得到“非一致”。这个小结论只是展开定义，
主定理不需要通过它来证明。
-/
theorem not_consistent_of_inconsistent {Γ : Set WFF} :
    Inconsistent Γ → ¬ Consistent Γ := by
  intro hContra hCon
  exact hCon hContra

end Consistency