Theorem: LO.FirstOrder.compactness_aux (Logic/FirstOrder/Ultraproduct.lean)

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T ↔ ∀ (i : FinSubtheory T), Satisfiable ↑↑i
Tactic:
constructor
State after:
case mp
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T → ∀ (i : FinSubtheory T), Satisfiable ↑↑i

case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) → Satisfiable T

State before:
case mp
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T → ∀ (i : FinSubtheory T), Satisfiable ↑↑i
Tactic:
rintro h ⟨t, ht⟩
State after:
case mp.mk
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : Satisfiable T
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ Satisfiable ↑↑⟨t, ht⟩

State before:
case mp.mk
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : Satisfiable T
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ Satisfiable ↑↑⟨t, ht⟩
Tactic:
exact Semantics.Satisfiable.of_subset h ht
State after:
no goals

State before:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) → Satisfiable T
Tactic:
intro h
State after:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
⊢ Satisfiable T

State before:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
⊢ Satisfiable T
Tactic:
have : ∀ i : FinSubtheory T, ∃ (M : Type u) (_ : Nonempty M) (_ : Structure L M), M ⊧ₘ* (i.val : Theory L) :=
  by intro i; exact satisfiable_iff.mp (h i)
State after:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
this : ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
⊢ Satisfiable T

State before:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
this : ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
⊢ Satisfiable T
Tactic:
choose A si s hA using this
State after:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
⊢ Satisfiable T

State before:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
⊢ Satisfiable T
Tactic:
have : ∃ 𝓤 : Ultrafilter (FinSubtheory T), Set.image (Semiformula.domain A) T ⊆ 𝓤.sets := ultrafilter_exists A hA
State after:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : ∃ 𝓤, Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T

State before:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : ∃ 𝓤, Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T
Tactic:
rcases this with ⟨𝓤, h𝓤⟩
State after:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T

State before:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T
Tactic:
have : Structure.Uprod A 𝓤 ⊧ₘ* T := ⟨by intro σ hσ; exact models_Uprod.mpr (h𝓤 $ Set.mem_image_of_mem (Semiformula.domain A) hσ)⟩
State after:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
this : Structure.Uprod A 𝓤 ⊧ₘ* T
⊢ Satisfiable T

State before:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
this : Structure.Uprod A 𝓤 ⊧ₘ* T
⊢ Satisfiable T
Tactic:
exact satisfiable_intro (Structure.Uprod A 𝓤) this
State after:
no goals

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
⊢ ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
Tactic:
intro i
State after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
i : FinSubtheory T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
i : FinSubtheory T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
Tactic:
exact satisfiable_iff.mp (h i)
State after:
no goals

State before:
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ ∀ ⦃f : Sentence L⦄, f ∈ T → (Structure.UprodStruc A 𝓤).toStruc ⊧ f
Tactic:
intro σ hσ
State after:
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
σ : Sentence L
hσ : σ ∈ T
⊢ (Structure.UprodStruc A 𝓤).toStruc ⊧ σ

State before:
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
σ : Sentence L
hσ : σ ∈ T
⊢ (Structure.UprodStruc A 𝓤).toStruc ⊧ σ
Tactic:
exact models_Uprod.mpr (h𝓤 $ Set.mem_image_of_mem (Semiformula.domain A) hσ)
State after:
no goals