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

• val (i : I) : A i

@[implicit_reducible]

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) : val e ε t = { val := fun (i : I) => val (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} : (Eval e ε) φ ↔ {i : I | (Eval (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 ξ} : (Evalf ε) φ ↔ {i : I | (Evalf 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)] {φ : Sentence L} : (Structure.Uprod A 𝓤)↓[L] ⊧ φ ↔ {i : I | (A i)↓[L] ⊧ φ} ∈ 𝓤

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

Equations

• LO.FirstOrder.Sentence.domain A φ = {i : I | (A i)↓[L] ⊧ φ}

@[reducible, inline]

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

Equations

• LO.FirstOrder.FinSubtheory T = { t : Finset (LO.FirstOrder.Sentence 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)↓[L] ⊧* ↑↑i) : ∃ (𝓤 : Ultrafilter (FinSubtheory T)), Sentence.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 (Sentence L)), ↑u ⊆ T → Satisfiable ↑u

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