structure LO.FirstOrder.Structure.Uprod {I : Type u} (A : I → Type u) (𝓤 : Ultrafilter I) : Type u

• val : (i : I) → A i

instance LO.FirstOrder.Structure.UprodStruc {L : LO.FirstOrder.Language} {I : Type u} (A : I → Type u) [s : (i : I) → LO.FirstOrder.Structure L (A i)] (𝓤 : Ultrafilter I) : LO.FirstOrder.Structure L (LO.FirstOrder.Structure.Uprod A 𝓤)

Equations

• One or more equations did not get rendered due to their size.

instance LO.FirstOrder.Structure.instNonemptyUprod {I : Type u} (A : I → Type u) (𝓤 : Ultrafilter I) [Nonempty I] [∀ (i : I), Nonempty (A i)] : Nonempty (LO.FirstOrder.Structure.Uprod A 𝓤)

Equations

• ⋯ = ⋯

@[simp]

theorem LO.FirstOrder.Structure.func_Uprod {L : LO.FirstOrder.Language} {I : Type u} (A : I → Type u) [s : (i : I) → LO.FirstOrder.Structure L (A i)] (𝓤 : Ultrafilter I) {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Structure.Uprod A 𝓤) : LO.FirstOrder.Structure.func f v = { val := fun (i : I) => LO.FirstOrder.Structure.func f fun (x : Fin k) => (v x).val i }

@[simp]

theorem LO.FirstOrder.Structure.rel_Uprod {L : LO.FirstOrder.Language} {I : Type u} (A : I → Type u) [s : (i : I) → LO.FirstOrder.Structure L (A i)] (𝓤 : Ultrafilter I) {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Structure.Uprod A 𝓤) : LO.FirstOrder.Structure.rel r v ↔ {i : I | LO.FirstOrder.Structure.rel r fun (x : Fin k) => (v x).val i} ∈ 𝓤

theorem LO.FirstOrder.Semiterm.val_Uprod {n : ℕ} {L : LO.FirstOrder.Language} {μ : Type v} {I : Type u} (A : I → Type u) [s : (i : I) → LO.FirstOrder.Structure L (A i)] (𝓤 : Ultrafilter I) (e : Fin n → LO.FirstOrder.Structure.Uprod A 𝓤) (ε : μ → LO.FirstOrder.Structure.Uprod A 𝓤) (t : LO.FirstOrder.Semiterm L μ n) : LO.FirstOrder.Semiterm.valm (LO.FirstOrder.Structure.Uprod A 𝓤) e ε t = { val := fun (i : I) => LO.FirstOrder.Semiterm.val (s i) (fun (x : Fin n) => (e x).val i) (fun (x : μ) => (ε x).val i) t }

theorem LO.FirstOrder.Semiformula.val_vecCons_val_eq {n : ℕ} {I : Type u} {A : I → Type u} {𝓤 : Ultrafilter I} {e : Fin n → LO.FirstOrder.Structure.Uprod A 𝓤} {z : LO.FirstOrder.Structure.Uprod A 𝓤} {i : I} : (z.val i :> fun (x : Fin n) => (e x).val i) = fun (x : Fin n.succ) => ((z :> e) x).val i

theorem LO.FirstOrder.Semiformula.eval_Uprod {n : ℕ} {L : LO.FirstOrder.Language} {μ : Type v} {I : Type u} {A : I → Type u} [∀ (i : I), Nonempty (A i)] [s : (i : I) → LO.FirstOrder.Structure L (A i)] {𝓤 : Ultrafilter I} {e : Fin n → LO.FirstOrder.Structure.Uprod A 𝓤} {ε : μ → LO.FirstOrder.Structure.Uprod A 𝓤} {p : LO.FirstOrder.Semiformula L μ n} : (LO.FirstOrder.Semiformula.Evalm (LO.FirstOrder.Structure.Uprod A 𝓤) e ε) p ↔ {i : I | (LO.FirstOrder.Semiformula.Eval (s i) (fun (x : Fin n) => (e x).val i) fun (x : μ) => (ε x).val i) p} ∈ 𝓤

theorem LO.FirstOrder.Semiformula.val_Uprod {L : LO.FirstOrder.Language} {μ : Type v} {I : Type u} {A : I → Type u} [∀ (i : I), Nonempty (A i)] [s : (i : I) → LO.FirstOrder.Structure L (A i)] {𝓤 : Ultrafilter I} {ε : μ → LO.FirstOrder.Structure.Uprod A 𝓤} {p : LO.FirstOrder.Formula L μ} : (LO.FirstOrder.Semiformula.Evalfm (LO.FirstOrder.Structure.Uprod A 𝓤) ε) p ↔ {i : I | (LO.FirstOrder.Semiformula.Evalf (s i) fun (x : μ) => (ε x).val i) p} ∈ 𝓤

theorem LO.FirstOrder.models_Uprod {L : LO.FirstOrder.Language} {I : Type u} {A : I → Type u} [s : (i : I) → LO.FirstOrder.Structure L (A i)] {𝓤 : Ultrafilter I} [Nonempty I] [∀ (i : I), Nonempty (A i)] {p : LO.FirstOrder.SyntacticFormula L} : LO.FirstOrder.Structure.Uprod A 𝓤 ⊧ₘ p ↔ {i : I | A i ⊧ₘ p} ∈ 𝓤

def LO.FirstOrder.Semiformula.domain {L : LO.FirstOrder.Language} {I : Type u} (A : I → Type u) [∀ (i : I), Nonempty (A i)] [s : (i : I) → LO.FirstOrder.Structure L (A i)] (p : LO.FirstOrder.SyntacticFormula L) : Set I

Equations

• LO.FirstOrder.Semiformula.domain A p = {i : I | A i ⊧ₘ p}

@[reducible, inline]

abbrev LO.FirstOrder.FinSubtheory {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) : Type u

Equations

• LO.FirstOrder.FinSubtheory T = { t : Finset (LO.FirstOrder.SyntacticFormula L) // ↑t ⊆ T }

instance LO.FirstOrder.instNonemptyFinSubtheory {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : Nonempty (LO.FirstOrder.FinSubtheory T)

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.ultrafilter_exists {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (A : LO.FirstOrder.FinSubtheory T → Type u) [s : (i : LO.FirstOrder.FinSubtheory T) → LO.FirstOrder.Structure L (A i)] [∀ (t : LO.FirstOrder.FinSubtheory T), Nonempty (A t)] (H : ∀ (i : LO.FirstOrder.FinSubtheory T), A i ⊧ₘ* ↑↑i) : ∃ (𝓤 : Ultrafilter (LO.FirstOrder.FinSubtheory T)), LO.FirstOrder.Semiformula.domain A '' T ⊆ (↑𝓤).sets

theorem LO.FirstOrder.compactness_aux {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : LO.FirstOrder.Satisfiable T ↔ ∀ (i : LO.FirstOrder.FinSubtheory T), LO.FirstOrder.Satisfiable ↑↑i

theorem LO.FirstOrder.compact {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : LO.FirstOrder.Satisfiable T ↔ ∀ (u : Finset (LO.FirstOrder.SyntacticFormula L)), ↑u ⊆ T → LO.FirstOrder.Satisfiable ↑u

instance LO.FirstOrder.instCompactSmallStrucSyntacticFormula {L : LO.FirstOrder.Language} : LO.Compact (LO.FirstOrder.SmallStruc L)

Equations

• ⋯ = ⋯