update Summary

Logic/Propositional/Basic.lean

@@ -1,3 +1,4 @@
 import Logic.Propositional.Basic.Formula
 import Logic.Propositional.Basic.Semantics
 import Logic.Propositional.Basic.Calculus
+import Logic.Propositional.Basic.Completeness

Logic/Propositional/Basic/Completeness.lean

@@ -44,15 +44,18 @@ theorem sound : ⊢¹ Δ → Semantics.Valid Δ.disj := by
 
 end Derivation
 
-instance : Sound (Formula α) := ⟨by
-  rintro T p ⟨Γ, hΓ, d⟩ v hT
+
+lemma soundness {T : Theory α} {p} : T ⊢ p → T ⊨ p := by
+  rintro ⟨Γ, hΓ, d⟩ v hT
   by_contra hv
   have : ∀ v, v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q := by
     simpa [Semantics.Valid, List.map_disj] using Derivation.sound (Tait.ofConsRight d)
   have : ∃ q ∈ Γ, ¬v ⊧ q := by simpa [hv] using this v
   rcases this with ⟨q, hqΓ, hq⟩
   have : v ⊧ q := hT (hΓ q hqΓ)
-  contradiction⟩
+  contradiction
+
+instance : Sound (Formula α) := ⟨soundness⟩
 
 section complete
 

Logic/Summary.lean

@@ -1,34 +1,56 @@
-import Logic.FirstOrder.Basic.Soundness
+
+import Logic.Propositional.Basic
 import Logic.FirstOrder.Hauptsatz
 import Logic.FirstOrder.Completeness.Completeness
 import Logic.FirstOrder.Incompleteness.FirstIncompleteness
 
-namespace LO.Summary.FirstOrder
+namespace LO.Summary
+
+namespace Propositional
+open LO.Propositional
+
+variable {α : Type*} {T : LO.Propositional.Theory α}
+
+/-- Soundness theorem -/
+noncomputable example {p : LO.Propositional.Formula α} :
+  T ⊢ p → T ⊨ p := soundness
+
+#print axioms soundness
+
+/-- Completeness theorem -/
+noncomputable example {p : LO.Propositional.Formula α} :
+  T ⊨ p → T ⊢ p := completeness
+
+#print axioms completeness
+
+end Propositional
+
+namespace FirstOrder
 
 open LO.FirstOrder
 
 variable {L : Language} {T : Theory L}
 
-/- Cut elimination for Tait-calculus -/
+/-- Cut elimination for Tait-calculus -/
 example [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)]
   {Δ : Sequent L} : ⊢¹ Δ → { d : ⊢¹ Δ // Derivation.CutFree d } := Derivation.hauptsatz
 
 #print axioms Derivation.hauptsatz
 
-/- Compactness theorem -/
+/-- Compactness theorem -/
 example (T : Theory L) :
     Semantics.SatisfiableTheory T ↔
     ∀ T' : Finset (Sentence L), ↑T' ⊆ T → Semantics.SatisfiableTheory (T' : Theory L) :=
   FirstOrder.compactness
 
 #print axioms FirstOrder.compactness
 
-/- Soundness theorem -/
+/-- Soundness theorem -/
 example {σ : Sentence L} : T ⊢ σ → T ⊨ σ := FirstOrder.soundness
 
 #print axioms FirstOrder.completeness
 
-/- Completeness theorem -/
+/-- Completeness theorem -/
 noncomputable example {σ : Sentence L} : T ⊨ σ → T ⊢ σ := FirstOrder.completeness
 
 #print axioms FirstOrder.completeness
@@ -38,16 +60,18 @@ open Arith FirstIncompleteness
 variable (T : Theory ℒₒᵣ) [DecidablePred T]
   [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [SigmaOneSound T] [Theory.Computable T]
 
-/- Gödel's first incompleteness theorem -/
+/-- Gödel's first incompleteness theorem -/
 example : ¬System.Complete T :=
   FirstOrder.Arith.first_incompleteness T
 
 #print axioms FirstOrder.Arith.first_incompleteness
 
-/- Undecidable sentence  -/
+/-- Undecidable sentence  -/
 example : T ⊬ undecidable T ∧ T ⊬ ~undecidable T :=
   FirstOrder.Arith.undecidable T
 
 #print axioms FirstOrder.Arith.undecidable
 
-end LO.Summary.FirstOrder
+end FirstOrder
+
+end LO.Summary