Theory HC

subsection‹Hilbert Calculus›
theory HC
imports Formulas
begin

text‹We can define Hilbert Calculus as the modus ponens closure over a set of axioms:›
inductive HC :: "'a formula  set ⇒ 'a formula ⇒ bool" (infix "⊢⇩H" 30) for Γ :: "'a formula set" where
Ax: "F ∈ Γ ⟹ Γ ⊢⇩H F" |
MP: "Γ ⊢⇩H F ⟹ Γ ⊢⇩H F ❙→ G ⟹ Γ ⊢⇩H G"
text‹.›

context begin

text‹The problem with that is defining the axioms. Normally, we just write that @{term "F ❙→ (G ❙→ F)"} is an axiom, 
  and mean that anything can be substituted for @{term F} and @{term G}.
Now, we can't just write down a set ‹{F ❙→ (G ❙→ F), \dots›.
Instead, defining it as an inductive set with no induction is a good idea.
›
(* Note to self: Don't try to formulate these as a definition. Possible, but painful to use. *)
inductive_set AX0 where
"F ❙→ (G ❙→ F) ∈ AX0" |
"(F ❙→ (G ❙→ H)) ❙→ ((F ❙→ G) ❙→ (F ❙→ H)) ∈ AX0"
inductive_set AX10 where
"F ∈ AX0 ⟹ F ∈ AX10" |
"F ❙→ (F ❙∨ G) ∈ AX10" |
"G ❙→ (F ❙∨ G) ∈ AX10" |
"(F ❙→ H) ❙→ ((G ❙→ H) ❙→ ((F ❙∨ G) ❙→ H)) ∈ AX10" |
"(F ❙∧ G) ❙→ F ∈ AX10" | 
"(F ❙∧ G) ❙→ G ∈ AX10" |
"F ❙→ (G ❙→ (F ❙∧ G)) ∈ AX10" |
"(F ❙→ ⊥) ❙→ ❙¬F ∈ AX10" |
"❙¬F ❙→ (F ❙→ ⊥) ∈ AX10" |
"(❙¬F ❙→ ⊥) ❙→ F ∈ AX10"
lemmas HC_intros[intro!] = 
  AX0.intros[THEN HC.intros(1)]
  AX0.intros[THEN AX10.intros(1), THEN HC.intros(1)]
  AX10.intros(2-)[THEN HC.intros(1)]

text‹The first four axioms, as originally formulated by Hilbert~\<^cite>‹"hilbert1928grundlagen"›.›
inductive_set AXH where
  "(F ❙→ (G ❙→ F)) ∈ AXH" |
  "(F ❙→ (F ❙→ G)) ❙→ (F ❙→ G) ∈ AXH" |
  "(F ❙→ (G ❙→ H)) ❙→ (G ❙→ (F ❙→ H)) ∈ AXH" |
  "(G ❙→ H) ❙→ ((F ❙→ G) ❙→ (F ❙→ H)) ∈ AXH"

lemma HC_mono: "S ⊢⇩H F ⟹ S ⊆ T ⟹ T ⊢⇩H F"
  by(induction rule: HC.induct) (auto intro: HC.intros)
lemma AX010: "AX0 ⊆ AX10"
  apply(rule)
  apply(cases rule: AX0.cases, assumption)
   apply(auto intro: AX10.intros)
done
lemma AX100[simp]: "AX0 ∪ AX10 = AX10" using AX010 by blast

text‹Hilbert's first four axioms and @{const AX0} are syntactically quite different.
  Derivability does not change:›
lemma hilbert_folgeaxiome_as_strong_as_AX0: "AX0 ∪ Γ ⊢⇩H F ⟷ AXH ∪ Γ ⊢⇩H F"
proof -
  have 0:
  "AX0 ⊢⇩H (F ❙→ (F ❙→ G)) ❙→ (F ❙→ G)"
  "AX0 ⊢⇩H (F ❙→ (G ❙→ H)) ❙→ (G ❙→ (F ❙→ H))"
  "AX0 ⊢⇩H (G ❙→ H) ❙→ ((F ❙→ G) ❙→ (F ❙→ H))" 
    for F G H using HC_intros(1,2) MP by metis+
  have H:
    "AXH ⊢⇩H (F ❙→ (G ❙→ H)) ❙→ ((F ❙→ G) ❙→ (F ❙→ H))"
    for F G H
  proof -
    note AXH.intros[THEN HC.Ax]
    thus ?thesis using MP by metis (* 4s *)
  qed
  note * = H 0
  note * = *[THEN HC_mono, OF Un_upper1]
  show ?thesis (is "?Z ⟷ ?H") (* HC, where nothing is automatic (except for after this, nearly everything in this file is) *)
  proof
    assume ?Z thus ?H proof induction
      case MP thus ?case using HC.MP by blast
    next
      case (Ax F) thus ?case proof
        assume "F ∈ AX0" thus ?thesis by induction (simp_all add: AXH.intros(1) HC.Ax *)
      next
        assume "F ∈ Γ" thus ?case using HC.Ax[of F] by simp
      qed
    qed
  next
    assume ?H thus ?Z proof induction
      case MP thus ?case using HC.MP by blast
    next
      case (Ax F) thus ?case proof
        assume "F ∈ AXH" thus ?thesis by induction (simp_all add: AX0.intros(1) HC.Ax *)
      next
        assume "F ∈ Γ" thus ?case using HC.Ax[of F] by simp
      qed
    qed
  qed
qed

lemma "AX0 ⊢⇩H F ❙→ F" by (meson HC_intros(1,2) HC.MP)
(* Can you do that again, but slowly? *)
lemma imp_self: "AX0 ⊢⇩H F ❙→ F" proof -
  let ?d = "λf. AX0 ⊢⇩H f"
  note MP
  moreover have "?d (F ❙→ (G ❙→ F))" for G using HC_intros(1)[where G=G and F=F] .
  moreover {
    note MP
    moreover have "?d (F ❙→ ((G ❙→ F) ❙→ F))" for G using HC_intros(1)[where G="G ❙→ F" and F=F] .
    moreover have "?d ((F ❙→ ((G ❙→ F) ❙→ F)) ❙→ ((F ❙→ (G ❙→ F)) ❙→ (F ❙→ F)))" for G using HC_intros(2)[where G="G ❙→ F" and F=F and H=F] .
    ultimately have "?d ((F ❙→ (G ❙→ F)) ❙→ (F ❙→ F))" for G . }
  ultimately show "?d (F ❙→ F)" .
qed

(* You'd get the idea for this theorem just when writing the HCND proof. It's really quite natural. *)
theorem Deduction_theorem: "AX0 ∪ insert F Γ ⊢⇩H G ⟹ AX0 ∪ Γ ⊢⇩H F ❙→ G"
proof(induction rule: HC.induct)
  case (Ax G)
  show ?case proof cases
    assume "F = G"
    from imp_self have "AX0 ⊢⇩H G ❙→ G" .
    with HC_mono show ?case unfolding ‹F = G› using sup_ge1 .
  next
    assume "F ≠ G"
    note HC.MP
    moreover {
      from ‹F ≠ G› ‹G ∈ AX0 ∪ insert F Γ› have "G ∈ AX0 ∪ Γ" by simp
      with HC.Ax have "AX0 ∪ Γ ⊢⇩H G" .
    }
    moreover from HC_mono[OF HC_intros(1) sup_ge1] have "AX0 ∪ Γ ⊢⇩H G ❙→ (F ❙→ G)" .
    ultimately show ?case .
  qed
next
  case (MP G H)
  have "AX0 ∪ Γ ⊢⇩H (F ❙→ (G ❙→ H)) ❙→ ((F ❙→ G) ❙→ (F ❙→ H))" using HC_mono by blast
  with HC.MP ‹AX0 ∪ Γ ⊢⇩H F ❙→ (G ❙→ H)› have "AX0 ∪ Γ ⊢⇩H (F ❙→ G) ❙→ (F ❙→ H)" .
  with HC.MP ‹AX0 ∪ Γ ⊢⇩H F ❙→ G› show "AX0 ∪ Γ ⊢⇩H F ❙→ H" .
qed


end

end