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 : Language} {I : Type u} (A : I → Type u) [s : (i : I) → Structure L (A i)] (𝓤 : Ultrafilter I) : Structure L (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 (Uprod A 𝓤)

@[simp]

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

@[simp]

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

theorem LO.FirstOrder.Semiterm.val_Uprod {n : ℕ} {L : Language} {μ : Type v} {I : Type u} (A : I → Type u) [s : (i : I) → Structure L (A i)] (𝓤 : Ultrafilter I) (e : Fin n → Structure.Uprod A 𝓤) (ε : μ → Structure.Uprod A 𝓤) (t : Semiterm L μ n) : valm (Structure.Uprod A 𝓤) e ε t = { val := fun (i : I) => 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 → Structure.Uprod A 𝓤} {z : 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 : Language} {μ : Type v} {I : Type u} {A : I → Type u} [s : (i : I) → Structure L (A i)] {𝓤 : Ultrafilter I} {e : Fin n → Structure.Uprod A 𝓤} {ε : μ → Structure.Uprod A 𝓤} [∀ (i : I), Nonempty (A i)] {φ : Semiformula L μ n} : (Evalm (Structure.Uprod A 𝓤) e ε) φ ↔ {i : I | (Eval (s i) (fun (x : Fin n) => (e x).val i) fun (x : μ) => (ε x).val i) φ} ∈ 𝓤

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

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

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

Equations

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

@[reducible, inline]

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

Equations

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

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

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

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

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

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