D1

Arithmetization/ISigmaOne/Metamath/Formula/Typed.lean

@@ -80,10 +80,10 @@ lemma val_inj {p q : L.TSemiformula n} :
 
 @[simp] lemma neg_verum : ~(⊤ : L.TSemiformula n) = ⊥ := by ext; simp
 @[simp] lemma neg_falsum : ~(⊥ : L.TSemiformula n) = ⊤ := by ext; simp
-lemma neg_and (p q : L.TSemiformula n) : ~(p ⋏ q) = ~p ⋎ ~q := by ext; simp
-lemma neg_or (p q : L.TSemiformula n) : ~(p ⋎ q) = ~p ⋏ ~q := by ext; simp
-lemma neg_all (p : L.TSemiformula (n + 1)) : ~p.all = (~p).ex := by ext; simp
-lemma neg_ex (p : L.TSemiformula (n + 1)) : ~p.ex = (~p).all := by ext; simp
+@[simp] lemma neg_and (p q : L.TSemiformula n) : ~(p ⋏ q) = ~p ⋎ ~q := by ext; simp
+@[simp] lemma neg_or (p q : L.TSemiformula n) : ~(p ⋎ q) = ~p ⋏ ~q := by ext; simp
+@[simp] lemma neg_all (p : L.TSemiformula (n + 1)) : ~p.all = (~p).ex := by ext; simp
+@[simp] lemma neg_ex (p : L.TSemiformula (n + 1)) : ~p.ex = (~p).all := by ext; simp
 
 lemma imp_def (p q : L.TSemiformula n) : p ⟶ q = ~p ⋎ q := by ext; simp [imp]
 

Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean

@@ -1,5 +1,6 @@
 import Arithmetization.ISigmaOne.Metamath.Formula.Typed
 import Arithmetization.ISigmaOne.Metamath.Proof.Theory
+import Logic.Logic.HilbertStyle.Supplemental
 
 /-!
 
@@ -55,6 +56,8 @@ instance : Membership L.TFormula L.Sequent := ⟨(·.val ∈ ·.val)⟩
 
 instance : HasSubset L.Sequent := ⟨(·.val ⊆ ·.val)⟩
 
+scoped infixr:50 " ⫽ " => Insert.insert
+
 namespace Language.Sequent
 
 variable {Γ Δ : L.Sequent} {p q : L.TFormula}
@@ -79,6 +82,13 @@ lemma subset_iff : Γ ⊆ Δ ↔ Γ.val ⊆ Δ.val := iff_of_eq rfl
 
 @[simp] lemma mem_union_iff : p ∈ Γ ∪ Δ ↔ p ∈ Γ ∨ p ∈ Δ := by simp [mem_iff, Language.TSemiformula.val_inj]
 
+@[ext] lemma ext (h : ∀ x, x ∈ Γ ↔ x ∈ Δ) : Γ = Δ := by
+  rcases Γ with ⟨Γ, hΓ⟩; rcases Δ with ⟨Δ, hΔ⟩; simp
+  apply mem_ext; intro x
+  constructor
+  · intro hx; simpa using mem_iff.mp <| (h ⟨x, hΓ x hx⟩ |>.1 (by simp [mem_iff, hx]))
+  · intro hx; simpa using mem_iff.mp <| (h ⟨x, hΔ x hx⟩ |>.2 (by simp [mem_iff, hx]))
+
 end Language.Sequent
 
 def Language.Sequent.shift (s : L.Sequent) : L.Sequent := ⟨L.setShift s.val, by simp⟩
@@ -93,58 +103,191 @@ structure Language.Theory.TDerivation (T : L.Theory) (Γ : L.Sequent) where
   derivation : V
   derivationOf : L.DerivationOf derivation (antecedents ∪ Γ.val)
 
-scoped infix:45 " ⊢ₜ " => Language.Theory.TDerivation
+scoped infix:45 " ⊢¹ " => Language.Theory.TDerivation
+
+def Language.Theory.TProof (T : L.Theory) (p : L.TFormula) := T ⊢¹ insert p ∅
+
+instance : System L.TFormula L.Theory := ⟨Language.Theory.TProof⟩
 
-def Language.Theory.Derivable.toTDerivation {T : L.Theory} (Γ : L.Sequent) (h : T.Derivable Γ.val) : T ⊢ₜ Γ := by
+def Language.Theory.Derivable.toTDerivation {T : L.Theory} (Γ : L.Sequent) (h : T.Derivable Γ.val) : T ⊢¹ Γ := by
   choose a ha using h; choose d hd using ha.2
   exact ⟨a, ha.1, d, hd⟩
 
-def Language.Theory.TDerivation.toDerivable {T : L.Theory} {Γ : L.Sequent} (d : T ⊢ₜ Γ) : T.Derivable Γ.val :=
+def Language.Theory.TDerivation.toDerivable {T : L.Theory} {Γ : L.Sequent} (d : T ⊢¹ Γ) : T.Derivable Γ.val :=
   ⟨d.antecedents, d.antecedents_fvFree, d.derivation, d.derivationOf⟩
 
+def Language.Theory.TDerivation.toTProof {T : L.Theory} {p} (d : T ⊢¹ insert p ∅) : T ⊢ p := d
+
+def Language.Theory.TProof.toTDerivation {T : L.Theory} {p} (d : T ⊢ p) : T ⊢¹ insert p ∅ := d
+
 namespace Language.Theory.TDerivation
 
-variable {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {Γ Δ : L.Sequent} {p q : L.TFormula}
+variable {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {Γ Δ : L.Sequent} {p q p₀ p₁ p₂ p₃ p₄ : L.TFormula}
+
+def byAxm (p) (h : p.val ∈ T) (hΓ : p ∈ Γ) : T ⊢¹ Γ :=
+  Language.Theory.Derivable.toTDerivation _
+    <| Language.Theory.Derivable.by_axm (by simp) h hΓ
 
-def em (p) (h : p ∈ Γ) (hn : ~p ∈ Γ) : T ⊢ₜ Γ :=
+def em (p) (h : p ∈ Γ := by simp) (hn : ~p ∈ Γ := by simp) : T ⊢¹ Γ :=
   Language.Theory.Derivable.toTDerivation _
     <| Language.Theory.Derivable.em (by simp) p.val (Language.Sequent.mem_iff.mp h) (by simpa using Language.Sequent.mem_iff.mp hn)
 
-def verum (h : ⊤ ∈ Γ) : T ⊢ₜ Γ :=
+def verum (h : ⊤ ∈ Γ := by simp) : T ⊢¹ Γ :=
   Language.Theory.Derivable.toTDerivation _
     <| Language.Theory.Derivable.verum (by simp) (by simpa using Language.Sequent.mem_iff.mp h)
 
-def and (dp : T ⊢ₜ insert p Γ) (dq : T ⊢ₜ insert q Γ) : T ⊢ₜ insert (p ⋏ q) Γ :=
+def and (dp : T ⊢¹ insert p Γ) (dq : T ⊢¹ insert q Γ) : T ⊢¹ insert (p ⋏ q) Γ :=
   Language.Theory.Derivable.toTDerivation _
     <| by simpa using Language.Theory.Derivable.and (by simpa using dp.toDerivable) (by simpa using dq.toDerivable)
 
-def or_m (dpq : T ⊢ₜ insert p (insert q Γ)) : T ⊢ₜ insert (p ⋎ q) Γ :=
+def or (dpq : T ⊢¹ insert p (insert q Γ)) : T ⊢¹ insert (p ⋎ q) Γ :=
   Language.Theory.Derivable.toTDerivation _ <| by simpa using Language.Theory.Derivable.or (by simpa using dpq.toDerivable)
 
-def all_m {p : L.TSemiformula (0 + 1)} (dp : T ⊢ₜ insert p.free Γ.shift) : T ⊢ₜ insert p.all Γ :=
+def all {p : L.TSemiformula (0 + 1)} (dp : T ⊢¹ insert p.free Γ.shift) : T ⊢¹ insert p.all Γ :=
   Language.Theory.Derivable.toTDerivation _ <| by
     simpa using Language.Theory.Derivable.all (by simpa using p.prop) (by simpa using dp.toDerivable)
 
-def ex_m {p : L.TSemiformula (0 + 1)} (t : L.TTerm) (dp : T ⊢ₜ insert (p.substs₁ t) Γ) : T ⊢ₜ insert p.ex Γ :=
+def ex {p : L.TSemiformula (0 + 1)} (t : L.TTerm) (dp : T ⊢¹ insert (p.substs₁ t) Γ) : T ⊢¹ insert p.ex Γ :=
   Language.Theory.Derivable.toTDerivation _ <| by
     simpa using Language.Theory.Derivable.ex (by simpa using p.prop) t.prop (by simpa using dp.toDerivable)
 
-def wk (d : T ⊢ₜ Δ) (h : Δ ⊆ Γ) : T ⊢ₜ Γ :=
+def wk (d : T ⊢¹ Δ) (h : Δ ⊆ Γ) : T ⊢¹ Γ :=
   Language.Theory.Derivable.toTDerivation _ <| by
     simpa using Language.Theory.Derivable.wk (by simp) (Language.Sequent.subset_iff.mp h) (by simpa using d.toDerivable)
 
-def cut (d₁ : T ⊢ₜ insert p Γ) (d₂ : T ⊢ₜ insert (~p) Γ) : T ⊢ₜ Γ :=
+def cut (d₁ : T ⊢¹ insert p Γ) (d₂ : T ⊢¹ insert (~p) Γ) : T ⊢¹ Γ :=
   Language.Theory.Derivable.toTDerivation _ <| by
     simpa using Language.Theory.Derivable.cut p.val (by simpa using d₁.toDerivable) (by simpa using d₂.toDerivable)
 
-def cut' (d₁ : T ⊢ₜ insert p Γ) (d₂ : T ⊢ₜ insert (~p) Δ) : T ⊢ₜ Γ ∪ Δ :=
+def cut' (d₁ : T ⊢¹ insert p Γ) (d₂ : T ⊢¹ insert (~p) Δ) : T ⊢¹ Γ ∪ Δ :=
   cut (p := p) (d₁.wk (by intro x; simp; tauto)) (d₂.wk (by intro x; simp; tauto))
 
-def conj (ps : L.TSemiformulaVec 0) (ds : ∀ i, (hi : i < len ps.val) → T ⊢ₜ insert (ps.nth i hi) Γ) : T ⊢ₜ insert ps.conj Γ := by
+def conj (ps : L.TSemiformulaVec 0) (ds : ∀ i, (hi : i < len ps.val) → T ⊢¹ insert (ps.nth i hi) Γ) : T ⊢¹ insert ps.conj Γ := by
   have : ∀ i < len ps.val, T.Derivable (insert (ps.val.[i]) Γ.val) := by intro i hi; simpa using (ds i hi).toDerivable
   have : T.Derivable (insert (^⋀ ps.val) Γ.val) := Language.Theory.Derivable.conj ps.val (by simp) this
   exact Language.Theory.Derivable.toTDerivation _ (by simpa using this)
 
+def modusPonens (dpq : T ⊢¹ insert (p ⟶ q) Γ) (dp : T ⊢¹ insert p Γ) : T ⊢¹ insert q Γ := by
+  let d : T ⊢¹ insert (p ⟶ q) (insert q Γ) := dpq.wk (insert_subset_insert_of_subset _ <| by simp)
+  let b : T ⊢¹ insert (~(p ⟶ q)) (insert q Γ) := by
+    simp only [TSemiformula.imp_def, TSemiformula.neg_or, TSemiformula.neg_neg]
+    exact and (dp.wk (insert_subset_insert_of_subset _ <| by simp))
+      (em q (by simp) (by simp))
+  exact cut d b
+
+def ofEq (d : T ⊢¹ Γ) (h : Γ = Δ) : T ⊢¹ Δ := h ▸ d
+
+def rotate₁ (d : T ⊢¹ p₀ ⫽ p₁ ⫽ Γ) : T ⊢¹ p₁ ⫽ p₀ ⫽ Γ :=
+  ofEq d (by ext x; simp; tauto)
+
+def rotate₂ (d : T ⊢¹ p₀ ⫽ p₁ ⫽ p₂ ⫽ Γ) : T ⊢¹ p₂ ⫽ p₁ ⫽ p₀ ⫽ Γ :=
+  ofEq d (by ext x; simp; tauto)
+
+def rotate₃ (d : T ⊢¹ p₀ ⫽ p₁ ⫽ p₂ ⫽ p₃ ⫽ Γ) : T ⊢¹ p₃ ⫽ p₁ ⫽ p₂ ⫽ p₀ ⫽ Γ :=
+  ofEq d (by ext x; simp; tauto)
+
 end Language.Theory.TDerivation
 
+namespace Language.Theory.TProof
+
+variable {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {p q : L.TFormula}
+
+/-- Condition D1 -/
+def modusPonens (d : T ⊢ p ⟶ q) (b : T ⊢ p) : T ⊢ q := TDerivation.modusPonens d b
+
+instance : System.ModusPonens T := ⟨modusPonens⟩
+
+instance : System.NegationEquiv T where
+  neg_equiv p := by
+    simp [Axioms.NegEquiv, LO.LogicalConnective.iff, TSemiformula.imp_def]
+    apply TDerivation.and
+    · apply TDerivation.or
+      apply TDerivation.rotate₁
+      apply TDerivation.or
+      exact TDerivation.em p
+    · apply TDerivation.or
+      apply TDerivation.and
+      · exact TDerivation.em p
+      · exact TDerivation.verum
+
+instance : System.Minimal T where
+  verum := TDerivation.toTProof <| TDerivation.verum
+  imply₁ (p q) := by
+    simp only [Axioms.Imply₁, TSemiformula.imp_def]
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    exact TDerivation.em p
+  imply₂ (p q r) := by
+    simp only [Axioms.Imply₂, TSemiformula.imp_def, TSemiformula.neg_or, TSemiformula.neg_neg]
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    apply TDerivation.rotate₂
+    apply TDerivation.and
+    · exact TDerivation.em p
+    · apply TDerivation.rotate₃
+      apply TDerivation.and
+      · exact TDerivation.em p
+      · apply TDerivation.and
+        · exact TDerivation.em q
+        · exact TDerivation.em r
+  and₁ (p q) := by
+    simp only [Axioms.AndElim₁, TSemiformula.imp_def, TSemiformula.neg_and]
+    apply TDerivation.or
+    apply TDerivation.or
+    exact TDerivation.em p
+  and₂ (p q) := by
+    simp only [Axioms.AndElim₂, TSemiformula.imp_def, TSemiformula.neg_and]
+    apply TDerivation.or
+    apply TDerivation.or
+    exact TDerivation.em q
+  and₃ (p q) := by
+    simp only [Axioms.AndInst, TSemiformula.imp_def]
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.and
+    · exact TDerivation.em p
+    · exact TDerivation.em q
+  or₁ (p q) := by
+    simp only [Axioms.OrInst₁, TSemiformula.imp_def]
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    exact TDerivation.em p
+  or₂ (p q) := by
+    simp [Axioms.OrInst₂, TSemiformula.imp_def]
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    exact TDerivation.em q
+  or₃ (p q r) := by
+    simp [Axioms.OrElim, TSemiformula.imp_def]
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    apply TDerivation.rotate₁
+    apply TDerivation.or
+    apply TDerivation.and
+    · apply TDerivation.rotate₃
+      apply TDerivation.and
+      · exact TDerivation.em p
+      · exact TDerivation.em r
+    · apply TDerivation.rotate₂
+      apply TDerivation.and
+      · exact TDerivation.em q
+      · exact TDerivation.em r
+
+instance : System.Classical T where
+  dne p := by
+    simp [Axioms.DNE, TSemiformula.imp_def]
+    apply TDerivation.or
+    exact TDerivation.em p
+
+end Language.Theory.TProof
+
 end typed_derivation