theorem
LO.FirstOrder.ModelsTheory.of_provably_subtheory
{L : LO.FirstOrder.Language}
(M : Type w)
[Nonempty M]
[LO.FirstOrder.Structure L M]
(T : LO.FirstOrder.Theory L)
(U : LO.FirstOrder.Theory L)
:
theorem
LO.FirstOrder.ModelsTheory.of_provably_subtheory'
{L : LO.FirstOrder.Language}
(M : Type w)
[Nonempty M]
[LO.FirstOrder.Structure L M]
(T : LO.FirstOrder.Theory L)
(U : LO.FirstOrder.Theory L)
[T ≼ U]
[M ⊧ₘ* U]
:
M ⊧ₘ* T
theorem
LO.FirstOrder.ModelsTheory.of_add_left
{L : LO.FirstOrder.Language}
(M : Type w)
[Nonempty M]
[LO.FirstOrder.Structure L M]
(T : LO.FirstOrder.Theory L)
(U : LO.FirstOrder.Theory L)
[M ⊧ₘ* T + U]
:
M ⊧ₘ* T
theorem
LO.FirstOrder.ModelsTheory.of_add_right
{L : LO.FirstOrder.Language}
(M : Type w)
[Nonempty M]
[LO.FirstOrder.Structure L M]
(T : LO.FirstOrder.Theory L)
(U : LO.FirstOrder.Theory L)
[M ⊧ₘ* T + U]
:
M ⊧ₘ* U
theorem
LO.FirstOrder.ModelsTheory.of_add_left_left
{L : LO.FirstOrder.Language}
(M : Type w)
[Nonempty M]
[LO.FirstOrder.Structure L M]
(T : LO.FirstOrder.Theory L)
(U : LO.FirstOrder.Theory L)
(V : LO.FirstOrder.Theory L)
[M ⊧ₘ* T + U + V]
:
M ⊧ₘ* T
theorem
LO.FirstOrder.ModelsTheory.of_add_left_right
{L : LO.FirstOrder.Language}
(M : Type w)
[Nonempty M]
[LO.FirstOrder.Structure L M]
(T : LO.FirstOrder.Theory L)
(U : LO.FirstOrder.Theory L)
(V : LO.FirstOrder.Theory L)
[M ⊧ₘ* T + U + V]
:
M ⊧ₘ* U
theorem
LO.FirstOrder.EQ.provOf
{L : LO.FirstOrder.Language}
[L.Eq]
{T : LO.FirstOrder.Theory L}
[𝐄𝐐 ≼ T]
(p : LO.FirstOrder.SyntacticFormula L)
(H : ∀ (M : Type (max u w)) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M]
[inst_2 : LO.FirstOrder.Structure.Eq L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ p)
:
T ⊨ p