feat(FirstOrder): ProvableWithEq

FormalMathematicsLab · Apr 7, 2024 · 584dadc · 584dadc
1 parent 4c8fbc9
commit 584dadc
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/Logic/FirstOrder/Basic/Eq.lean b/Logic/FirstOrder/Basic/Eq.lean
@@ -64,6 +64,14 @@ abbrev ConsequenceWithEq (T : Theory L) (σ : Sentence L) : Prop := T⁼ ⊨ σ
 
 infix:55 " ⊨₌ " => ConsequenceWithEq
 
+abbrev ProofWithEq (T : Theory L) (σ : Sentence L) : Type _ := T⁼ ⊢ σ
+
+abbrev ProvableWithEq (T : Theory L) (σ : Sentence L) : Prop := T⁼ ⊢! σ
+
+infix:45 " ⊢₌ " => ProofWithEq
+
+infix:45 " ⊢₌! " => ProvableWithEq
+
 namespace Structure
 
 namespace Eq

diff --git a/Logic/FirstOrder/Completeness/Lemmata.lean b/Logic/FirstOrder/Completeness/Lemmata.lean
@@ -21,4 +21,6 @@ lemma of_add_left_right [M ⊧ₘ* T + U + V] : M ⊧ₘ* U := @of_add_right _ M
 
 end ModelsTheory
 
+theorem completeness_iff_with_eq {L : Language} [L.Eq] {T : Theory L} {σ : Sentence L} : T ⊨₌ σ ↔ T ⊢₌! σ := completeness_iff
+
 end LO.FirstOrder