MathematicalLogic.FirstOrder.Completeness.Language

source

theorem directed_of_vec {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [IsDirected α r] {n : ℕ} [h : Nonempty α] (v : Vec α n) :

∃ (a : α), ∀ (i : Fin n), r (v i) a

source

theorem directed_of_three {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [IsDirected α r] (x y z : α) :

∃ (a : α), r x a ∧ r y a ∧ r z a

source

structure FirstOrder.Language.Hom (L₁ L₂ : Language) :

Type

onFunc {n : ℕ} : L₁.Func n → L₂.Func n
onRel {n : ℕ} : L₁.Rel n → L₂.Rel n

Instances For

source

def FirstOrder.Language.«term_→ᴸ_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

theorem FirstOrder.Language.Hom.ext {L₁ L₂ : Language} {φ ψ : L₁ →ᴸ L₂} (h₁ : ∀ (n : ℕ) (f : L₁.Func n), φ.onFunc f = ψ.onFunc f) (h₂ : ∀ (n : ℕ) (r : L₁.Rel n), φ.onRel r = ψ.onRel r) :

φ = ψ

source

theorem FirstOrder.Language.Hom.ext_iff {L₁ L₂ : Language} {φ ψ : L₁ →ᴸ L₂} :

φ = ψ ↔ (∀ (n : ℕ) (f : L₁.Func n), φ.onFunc f = ψ.onFunc f) ∧ ∀ (n : ℕ) (r : L₁.Rel n), φ.onRel r = ψ.onRel r

source

def FirstOrder.Language.Hom.id {L : Language} :

L →ᴸ L

Equations

FirstOrder.Language.Hom.id = { onFunc := fun {n : ℕ} (f : L.Func n) => f, onRel := fun {n : ℕ} (r : L.Rel n) => r }

Instances For

source

@[simp]

theorem FirstOrder.Language.Hom.id_onFunc {L : Language} {n✝ : ℕ} (f : L.Func n✝) :

id.onFunc f = f

source

@[simp]

theorem FirstOrder.Language.Hom.id_onRel {L : Language} {n✝ : ℕ} (r : L.Rel n✝) :

id.onRel r = r

source

def FirstOrder.Language.Hom.comp {L₁ L₂ L₃ : Language} (φ₂ : L₂ →ᴸ L₃) (φ₁ : L₁ →ᴸ L₂) :

L₁ →ᴸ L₃

Equations

φ₂ ∘ᴸ φ₁ = { onFunc := fun {n : ℕ} (f : L₁.Func n) => φ₂.onFunc (φ₁.onFunc f), onRel := fun {n : ℕ} (r : L₁.Rel n) => φ₂.onRel (φ₁.onRel r) }

Instances For

source

@[simp]

theorem FirstOrder.Language.Hom.comp_onRel {L₁ L₂ L₃ : Language} (φ₂ : L₂ →ᴸ L₃) (φ₁ : L₁ →ᴸ L₂) {n✝ : ℕ} (r : L₁.Rel n✝) :

(φ₂ ∘ᴸ φ₁).onRel r = φ₂.onRel (φ₁.onRel r)

source

@[simp]

theorem FirstOrder.Language.Hom.comp_onFunc {L₁ L₂ L₃ : Language} (φ₂ : L₂ →ᴸ L₃) (φ₁ : L₁ →ᴸ L₂) {n✝ : ℕ} (f : L₁.Func n✝) :

(φ₂ ∘ᴸ φ₁).onFunc f = φ₂.onFunc (φ₁.onFunc f)

source

def FirstOrder.Language.Hom.«term_∘ᴸ_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

theorem FirstOrder.Language.Hom.comp_id {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} :

φ ∘ᴸ id = φ

source

theorem FirstOrder.Language.Hom.id_comp {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} :

id ∘ᴸ φ = φ

source

theorem FirstOrder.Language.Hom.comp_assoc {L₁✝ L₂✝ : Language} {φ₃ : L₁✝ →ᴸ L₂✝} {L₁✝¹ : Language} {φ₂ : L₁✝¹ →ᴸ L₁✝} {L₁✝² : Language} {φ₁ : L₁✝² →ᴸ L₁✝¹} :

φ₃ ∘ᴸ φ₂ ∘ᴸ φ₁ = φ₃ ∘ᴸ (φ₂ ∘ᴸ φ₁)

source

def FirstOrder.Language.Hom.onTerm {L₁ L₂ : Language} {n : ℕ} (φ : L₁ →ᴸ L₂) :

L₁.Term n → L₂.Term n

Equations

φ.onTerm #x_1 = #x_1
φ.onTerm (f ⬝ᶠ v) = φ.onFunc f ⬝ᶠ fun (i : Fin m) => φ.onTerm (v i)

Instances For

source

theorem FirstOrder.Language.Hom.id_onTerm {L✝ : Language} {n✝ : ℕ} {t : L✝.Term n✝} :

id.onTerm t = t

source

theorem FirstOrder.Language.Hom.comp_onTerm {L₁✝ L₂✝ : Language} {φ₂ : L₁✝ →ᴸ L₂✝} {L₁✝¹ : Language} {φ₁ : L₁✝¹ →ᴸ L₁✝} {n✝ : ℕ} {t : L₁✝¹.Term n✝} :

(φ₂ ∘ᴸ φ₁).onTerm t = φ₂.onTerm (φ₁.onTerm t)

source

theorem FirstOrder.Language.Hom.onTerm_subst {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {n✝ : ℕ} {t : L₁.Term n✝} {m✝ : ℕ} {σ : L₁.Subst n✝ m✝} :

φ.onTerm t[σ]ₜ = (φ.onTerm t)[φ.onTerm ∘ σ]ₜ

source

theorem FirstOrder.Language.Hom.onTerm_shift {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {n✝ : ℕ} {t : L₁.Term n✝} :

φ.onTerm ↑ₜt = ↑ₜ(φ.onTerm t)

source

def FirstOrder.Language.Hom.onFormula {L₁ L₂ : Language} {n : ℕ} (φ : L₁ →ᴸ L₂) :

L₁.Formula n → L₂.Formula n

Equations

φ.onFormula (r ⬝ʳ v) = φ.onRel r ⬝ʳ fun (i : Fin m) => φ.onTerm (v i)
φ.onFormula (t₁ ≐ t₂) = φ.onTerm t₁ ≐ φ.onTerm t₂
φ.onFormula FirstOrder.Language.Formula.false = ⊥
φ.onFormula (p.imp q) = φ.onFormula p ⇒ φ.onFormula q
φ.onFormula (∀' p) = ∀' φ.onFormula p

Instances For

source

theorem FirstOrder.Language.Hom.onFormula_neg {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {a✝ : ℕ} {p : L₁.Formula a✝} :

φ.onFormula (~ p) = ~ φ.onFormula p

source

theorem FirstOrder.Language.Hom.onFormula_and {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {a✝ : ℕ} {p q : L₁.Formula a✝} :

φ.onFormula (p ⩑ q) = φ.onFormula p ⩑ φ.onFormula q

source

theorem FirstOrder.Language.Hom.onFormula_andN {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {n m : ℕ} {v : Vec (L₁.Formula n) m} :

φ.onFormula (⋀ (i : Fin m), v i) = ⋀ (i : Fin m), φ.onFormula (v i)

source

theorem FirstOrder.Language.Hom.id_onFormula {L✝ : Language} {a✝ : ℕ} {p : L✝.Formula a✝} :

id.onFormula p = p

source

theorem FirstOrder.Language.Hom.comp_onFormula {L₁✝ L₂✝ : Language} {φ₂ : L₁✝ →ᴸ L₂✝} {L₁✝¹ : Language} {φ₁ : L₁✝¹ →ᴸ L₁✝} {a✝ : ℕ} {p : L₁✝¹.Formula a✝} :

(φ₂ ∘ᴸ φ₁).onFormula p = φ₂.onFormula (φ₁.onFormula p)

source

theorem FirstOrder.Language.Hom.onFormula_subst {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {n m : ℕ} {p : L₁.Formula n} {σ : L₁.Subst n m} :

φ.onFormula p[σ]ₚ = (φ.onFormula p)[φ.onTerm ∘ σ]ₚ

source

theorem FirstOrder.Language.Hom.onFormula_shift {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {a✝ : ℕ} {p : L₁.Formula a✝} :

φ.onFormula ↑ₚp = ↑ₚ(φ.onFormula p)

source

theorem FirstOrder.Language.Hom.onFormula_subst_single {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {a✝ : ℕ} {p : L₁.Formula (a✝ + 1)} {t : L₁.Term a✝} :

φ.onFormula p[↦ₛ t]ₚ = (φ.onFormula p)[↦ₛ φ.onTerm t]ₚ

source

theorem FirstOrder.Language.Hom.on_axiom {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {a✝ : ℕ} {p : L₁.Formula a✝} :

p ∈ L₁.Axiom → φ.onFormula p ∈ L₂.Axiom

source

theorem FirstOrder.Language.Hom.on_proof {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {n✝ : ℕ} {Γ : L₁.FormulaSet n✝} {p : L₁.Formula n✝} :

Γ ⊢ p → φ.onFormula '' Γ ⊢ φ.onFormula p

source

def FirstOrder.Language.Hom.reduct {L₁ L₂ : Language} (φ : L₁ →ᴸ L₂) (M : L₂.Structure) :

L₁.Structure

Equations

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

Instances For

source

@[simp]

theorem FirstOrder.Language.Hom.reduct_interpFunc {L₁ L₂ : Language} (φ : L₁ →ᴸ L₂) (M : L₂.Structure) {m✝ : ℕ} (f : L₁.Func m✝) (v : Vec M.Dom m✝) :

(φ.reduct M).interpFunc f v = M.interpFunc (φ.onFunc f) v

source

@[simp]

theorem FirstOrder.Language.Hom.reduct_Dom {L₁ L₂ : Language} (φ : L₁ →ᴸ L₂) (M : L₂.Structure) :

(φ.reduct M).Dom = M.Dom

source

@[simp]

theorem FirstOrder.Language.Hom.reduct_interpRel {L₁ L₂ : Language} (φ : L₁ →ᴸ L₂) (M : L₂.Structure) {m✝ : ℕ} (r : L₁.Rel m✝) (v : Vec M.Dom m✝) :

(φ.reduct M).interpRel r v = M.interpRel (φ.onRel r) v

source

theorem FirstOrder.Language.Hom.interp_onTerm {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {M : L₂.Structure} {n✝ : ℕ} {t : L₁.Term n✝} {ρ : Vec M.Dom n✝} :

⟦φ.onTerm t⟧ₜ M.Dom, ρ = ⟦t⟧ₜ (φ.reduct M).Dom, ρ

source

theorem FirstOrder.Language.Hom.satisfy_onFormula {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {M : L₂.Structure} {a✝ : ℕ} {p : L₁.Formula a✝} {ρ : Vec M.Dom a✝} :

M.Dom ⊨[ρ] φ.onFormula p ↔ (φ.reduct M).Dom ⊨[ρ] p

source

theorem FirstOrder.Language.Hom.on_satisfiable {L₁ L₂ : Language} {φ : L₁ →ᴸ L₂} {a✝ : ℕ} {Γ : Set (L₁.Formula a✝)} :

Satisfiable.{u} (φ.onFormula '' Γ) → Satisfiable.{u} Γ

source

structure FirstOrder.Language.DirectedSystem {ι : Type} [Preorder ι] (L : ι → Language) :

Type

hom (i j : ι) : i ≤ j → L i →ᴸ L j
hom_id {i : ι} (h : i ≤ i) : self.hom i i h = Hom.id
hom_comp {i j k : ι} (h₁ : i ≤ j) (h₂ : j ≤ k) (h₃ : i ≤ k) : self.hom j k h₂ ∘ᴸ self.hom i j h₁ = self.hom i k h₃

Instances For

source

def FirstOrder.Language.DirectedSystem.setoidFunc {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} (φ : DirectedSystem L) (n : ℕ) :

Setoid ((i : ι) × (L i).Func n)

Equations

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

Instances For

source

def FirstOrder.Language.DirectedSystem.setoidRel {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} (φ : DirectedSystem L) (n : ℕ) :

Setoid ((i : ι) × (L i).Rel n)

Equations

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

Instances For

source

def FirstOrder.Language.DirectedSystem.directLimit {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} (φ : DirectedSystem L) :

Language

Equations

φ.directLimit = { Func := fun (n : ℕ) => Quotient (φ.setoidFunc n), Rel := fun (n : ℕ) => Quotient (φ.setoidRel n) }

Instances For

source

def FirstOrder.Language.DirectedSystem.homLimit {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} (φ : DirectedSystem L) (i : ι) :

L i →ᴸ φ.directLimit

Equations

φ.homLimit i = { onFunc := fun {n : ℕ} (f : (L i).Func n) => ⟦⟨i, f⟩⟧, onRel := fun {n : ℕ} (r : (L i).Rel n) => ⟦⟨i, r⟩⟧ }

Instances For

source

theorem FirstOrder.Language.DirectedSystem.homLimit_comp_hom {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {i j : ι} {h : i ≤ j} :

φ.homLimit j ∘ᴸ φ.hom i j h = φ.homLimit i

source

theorem FirstOrder.Language.DirectedSystem.term_hom_eq_of_homLimit_eq {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {i : ι} {n : ℕ} {j : ι} [Nonempty ι] (t₁ : (L i).Term n) (t₂ : (L j).Term n) (h : (φ.homLimit i).onTerm t₁ = (φ.homLimit j).onTerm t₂) :

∃ (k : ι) (h₁ : i ≤ k) (h₂ : j ≤ k), (φ.hom i k h₁).onTerm t₁ = (φ.hom j k h₂).onTerm t₂

source

theorem FirstOrder.Language.DirectedSystem.formula_hom_eq_of_homLimit_eq {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {i : ι} {n : ℕ} {j : ι} [Nonempty ι] (p : (L i).Formula n) (q : (L j).Formula n) (h : (φ.homLimit i).onFormula p = (φ.homLimit j).onFormula q) :

∃ (k : ι) (h₁ : i ≤ k) (h₂ : j ≤ k), (φ.hom i k h₁).onFormula p = (φ.hom j k h₂).onFormula q

source

theorem FirstOrder.Language.DirectedSystem.term_of_homLimit {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {n : ℕ} [h : Nonempty ι] (t : φ.directLimit.Term n) :

∃ (i : ι) (t' : (L i).Term n), t = (φ.homLimit i).onTerm t'

source

theorem FirstOrder.Language.DirectedSystem.formula_of_homLimit {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {n : ℕ} [h : Nonempty ι] (p : φ.directLimit.Formula n) :

∃ (i : ι) (q : (L i).Formula n), p = (φ.homLimit i).onFormula q

source

theorem FirstOrder.Language.DirectedSystem.axiom_of_homLimit {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {a✝ : ℕ} {p : φ.directLimit.Formula a✝} [Nonempty ι] (h : p ∈ φ.directLimit.Axiom) :

∃ (i : ι) (q : (L i).Formula a✝), p = (φ.homLimit i).onFormula q ∧ q ∈ (L i).Axiom

source

theorem FirstOrder.Language.DirectedSystem.proof_of_homLimit {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {n✝ : ℕ} {Γ : φ.directLimit.FormulaSet n✝} {p : φ.directLimit.Formula n✝} [Nonempty ι] (h : Γ ⊢ p) :

∃ (i : ι) (Δ : Set ((L i).Formula n✝)) (q : (L i).Formula n✝), (φ.homLimit i).onFormula '' Δ ⊆ Γ ∧ p = (φ.homLimit i).onFormula q ∧ Δ.Finite ∧ Δ ⊢ q

source

theorem FirstOrder.Language.DirectedSystem.subset_of_monotone_union {ι : Type} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {L : ι → Language} {φ : DirectedSystem L} {n : ℕ} {i : ι} [Nonempty ι] {Γ : (i : ι) → (L i).FormulaSet n} {Δ : (L i).FormulaSet n} (h₁ : ∀ (i j : ι) (h : i ≤ j), (φ.hom i j h).onFormula '' Γ i ⊆ Γ j) (h₂ : (φ.homLimit i).onFormula '' Δ ⊆ ⋃ (i : ι), (φ.homLimit i).onFormula '' Γ i) (h : Set.Finite Δ) :

∃ (j : ι) (h : i ≤ j), (φ.hom i j h).onFormula '' Δ ⊆ Γ j

source

def FirstOrder.Language.DirectedSystem.ofChain (L : ℕ → Language) (φ : (i : ℕ) → L i →ᴸ L (i + 1)) :

DirectedSystem L

Equations

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

Instances For

source

theorem FirstOrder.Language.DirectedSystem.ofChain_hom_succ {i : ℕ} {h : i ≤ i.succ} {L : ℕ → Language} {φ : (i : ℕ) → L i →ᴸ L (i + 1)} :

(ofChain L φ).hom i i.succ h = φ i

source

theorem FirstOrder.Language.DirectedSystem.monotone_chain {n : ℕ} {L : ℕ → Language} {φ : (i : ℕ) → L i →ᴸ L (i + 1)} {Γ : (i : ℕ) → (L i).FormulaSet n} (h₁ : ∀ (i : ℕ), (φ i).onFormula '' Γ i ⊆ Γ (i + 1)) (i j : ℕ) (h : i ≤ j) :

((ofChain L φ).hom i j h).onFormula '' Γ i ⊆ Γ j