Foundation.FirstOrder.Completeness.SubLanguage

source

def LO.FirstOrder.Language.subLanguage (L : Language) (pfunc : (k : ℕ) → L.Func k → Prop) (prel : (k : ℕ) → L.Rel k → Prop) :

Language

Equations

L.subLanguage pfunc prel = { Func := fun (k : ℕ) => Subtype (pfunc k), Rel := fun (k : ℕ) => Subtype (prel k) }

Instances For

source

def LO.FirstOrder.Language.ofSubLanguage (L : Language) {pf : (k : ℕ) → L.Func k → Prop} {pr : (k : ℕ) → L.Rel k → Prop} :

(L.subLanguage pf pr).Hom L

Equations

L.ofSubLanguage = { func := fun {k : ℕ} => Subtype.val, rel := fun {k : ℕ} => Subtype.val }

Instances For

source

@[simp]

theorem LO.FirstOrder.Language.ofSubLanguage_onFunc (L : Language) {pfunc✝ : (k : ℕ) → L.Func k → Prop} {prel✝ : (k : ℕ) → L.Rel k → Prop} {a✝ : ℕ} {φ : (L.subLanguage pfunc✝ prel✝).Func a✝} :

L.ofSubLanguage.func φ = ↑φ

source

@[simp]

theorem LO.FirstOrder.Language.ofSubLanguage_onRel (L : Language) {pfunc✝ : (k : ℕ) → L.Func k → Prop} {prel✝ : (k : ℕ) → L.Rel k → Prop} {a✝ : ℕ} {φ : (L.subLanguage pfunc✝ prel✝).Rel a✝} :

L.ofSubLanguage.rel φ = ↑φ

source

def LO.FirstOrder.Semiterm.lang {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} :

Semiterm L μ n → Finset ((k : ℕ) × L.Func k)

Equations

(LO.FirstOrder.Semiterm.bvar a).lang = ∅
(LO.FirstOrder.Semiterm.fvar a).lang = ∅
(LO.FirstOrder.Semiterm.func f v).lang = insert ⟨arity, f⟩ (Finset.univ.biUnion fun (i : Fin arity) => (v i).lang)

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiterm.lang_func {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L μ n) :

⟨k, f⟩ ∈ (func f v).lang

source

theorem LO.FirstOrder.Semiterm.lang_func_ss {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L μ n) (i : Fin k) :

(v i).lang ⊆ (func f v).lang

source

def LO.FirstOrder.Semiterm.toSubLanguage' {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} (pf : (k : ℕ) → L.Func k → Prop) (pr : (k : ℕ) → L.Rel k → Prop) (t : Semiterm L μ n) :

(∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ t.lang → pf k f) → Semiterm (L.subLanguage pf pr) μ n

Equations

LO.FirstOrder.Semiterm.toSubLanguage' pf pr (LO.FirstOrder.Semiterm.bvar x_2) x_3 = LO.FirstOrder.Semiterm.bvar x_2
LO.FirstOrder.Semiterm.toSubLanguage' pf pr (LO.FirstOrder.Semiterm.fvar x_2) x_3 = LO.FirstOrder.Semiterm.fvar x_2
LO.FirstOrder.Semiterm.toSubLanguage' pf pr (LO.FirstOrder.Semiterm.func f v) h = LO.FirstOrder.Semiterm.func ⟨f, ⋯⟩ fun (i : Fin k) => LO.FirstOrder.Semiterm.toSubLanguage' pf pr (v i) ⋯

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiterm.lMap_toSubLanguage' {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} (pf : (k : ℕ) → L.Func k → Prop) (pr : (k : ℕ) → L.Rel k → Prop) (t : Semiterm L μ n) (h : ∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ t.lang → pf k f) :

lMap L.ofSubLanguage (toSubLanguage' pf pr t h) = t

source

noncomputable def LO.FirstOrder.Semiformula.langFunc {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} :

Semiformula L μ n → Finset ((k : ℕ) × L.Func k)

Equations

LO.FirstOrder.Semiformula.verum.langFunc = ∅
LO.FirstOrder.Semiformula.falsum.langFunc = ∅
(LO.FirstOrder.Semiformula.rel a v).langFunc = Finset.univ.biUnion fun (i : Fin arity) => (v i).lang
(LO.FirstOrder.Semiformula.nrel a v).langFunc = Finset.univ.biUnion fun (i : Fin arity) => (v i).lang
(φ.and ψ).langFunc = φ.langFunc ∪ ψ.langFunc
(φ.or ψ).langFunc = φ.langFunc ∪ ψ.langFunc
φ.all.langFunc = φ.langFunc
φ.ex.langFunc = φ.langFunc

Instances For

source

noncomputable def LO.FirstOrder.Semiformula.langRel {L : Language} [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} :

Semiformula L μ n → Finset ((k : ℕ) × L.Rel k)

Equations

LO.FirstOrder.Semiformula.verum.langRel = ∅
LO.FirstOrder.Semiformula.falsum.langRel = ∅
(LO.FirstOrder.Semiformula.rel a v).langRel = {⟨arity, a⟩}
(LO.FirstOrder.Semiformula.nrel a v).langRel = {⟨arity, a⟩}
(φ.and ψ).langRel = φ.langRel ∪ ψ.langRel
(φ.or ψ).langRel = φ.langRel ∪ ψ.langRel
φ.all.langRel = φ.langRel
φ.ex.langRel = φ.langRel

Instances For

source

theorem LO.FirstOrder.Semiformula.langFunc_rel_ss {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L μ n) (i : Fin k) :

(v i).lang ⊆ (rel r v).langFunc

source

def LO.FirstOrder.Semiformula.toSubLanguage' {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} (pf : (k : ℕ) → L.Func k → Prop) (pr : (k : ℕ) → L.Rel k → Prop) {n : ℕ} (φ : Semiformula L μ n) :

(∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ φ.langFunc → pf k f) → (∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ φ.langRel → pr k r) → Semiformula (L.subLanguage pf pr) μ n

Equations

One or more equations did not get rendered due to their size.
LO.FirstOrder.Semiformula.toSubLanguage' pf pr LO.FirstOrder.Semiformula.verum x_5 x_6 = ⊤
LO.FirstOrder.Semiformula.toSubLanguage' pf pr LO.FirstOrder.Semiformula.falsum x_5 x_6 = ⊥
LO.FirstOrder.Semiformula.toSubLanguage' pf pr (φ.and ψ) hf hr = LO.FirstOrder.Semiformula.toSubLanguage' pf pr φ ⋯ ⋯ ⋏ LO.FirstOrder.Semiformula.toSubLanguage' pf pr ψ ⋯ ⋯
LO.FirstOrder.Semiformula.toSubLanguage' pf pr (φ.or ψ) hf hr = LO.FirstOrder.Semiformula.toSubLanguage' pf pr φ ⋯ ⋯ ⋎ LO.FirstOrder.Semiformula.toSubLanguage' pf pr ψ ⋯ ⋯
LO.FirstOrder.Semiformula.toSubLanguage' pf pr φ.all hf hr = ∀' LO.FirstOrder.Semiformula.toSubLanguage' pf pr φ hf hr
LO.FirstOrder.Semiformula.toSubLanguage' pf pr φ.ex hf hr = ∃' LO.FirstOrder.Semiformula.toSubLanguage' pf pr φ hf hr

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_toSubLanguage' {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} (pf : (k : ℕ) → L.Func k → Prop) (pr : (k : ℕ) → L.Rel k → Prop) {n : ℕ} (φ : Semiformula L μ n) (hf : ∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ φ.langFunc → pf k f) (hr : ∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ φ.langRel → pr k r) :

(lMap L.ofSubLanguage) (toSubLanguage' pf pr φ hf hr) = φ

source

noncomputable def LO.FirstOrder.Semiformula.languageFuncIndexed {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} (φ : Semiformula L μ n) (k : ℕ) :

Finset (L.Func k)

Equations

φ.languageFuncIndexed k = φ.langFunc.preimage (Sigma.mk k) ⋯

Instances For

source

noncomputable def LO.FirstOrder.Semiformula.languageRelIndexed {L : Language} [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} (φ : Semiformula L μ n) (k : ℕ) :

Finset (L.Rel k)

Equations

φ.languageRelIndexed k = φ.langRel.preimage (Sigma.mk k) ⋯

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.languageFinset {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} (Γ : Finset (Semiformula L μ n)) :

Language

Equations

LO.FirstOrder.Semiformula.languageFinset Γ = L.subLanguage (fun (k : ℕ) (f : L.Func k) => ∃ φ ∈ Γ, ⟨k, f⟩ ∈ φ.langFunc) fun (k : ℕ) (r : L.Rel k) => ∃ φ ∈ Γ, ⟨k, r⟩ ∈ φ.langRel

Instances For

source

noncomputable instance LO.FirstOrder.Semiformula.instFintypeFuncLanguageFinset {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} (Γ : Finset (Semiformula L μ n)) (k : ℕ) :

Fintype ((languageFinset Γ).Func k)

Equations

LO.FirstOrder.Semiformula.instFintypeFuncLanguageFinset Γ k = Fintype.subtype (Γ.biUnion fun (x : LO.FirstOrder.Semiformula L μ n) => x.languageFuncIndexed k) ⋯

source

noncomputable instance LO.FirstOrder.Semiformula.instFintypeRelLanguageFinset {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} (Γ : Finset (Semiformula L μ n)) (k : ℕ) :

Fintype ((languageFinset Γ).Rel k)

Equations

LO.FirstOrder.Semiformula.instFintypeRelLanguageFinset Γ k = Fintype.subtype (Γ.biUnion fun (x : LO.FirstOrder.Semiformula L μ n) => x.languageRelIndexed k) ⋯

source

def LO.FirstOrder.Semiformula.toSubLanguageFinsetSelf {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} {Γ : Finset (Semiformula L μ n)} {φ : Semiformula L μ n} (h : φ ∈ Γ) :

Semiformula (languageFinset Γ) μ n

Equations

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

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_toSubLanguageFinsetSelf {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} {Γ : Finset (Semiformula L μ n)} {φ : Semiformula L μ n} (h : φ ∈ Γ) :

(lMap L.ofSubLanguage) (toSubLanguageFinsetSelf h) = φ

source

instance LO.FirstOrder.Structure.subLanguageStructure {L : Language} {pf : (k : ℕ) → L.Func k → Prop} {pr : (k : ℕ) → L.Rel k → Prop} {M : Type w} (s : Structure L M) :

Structure (L.subLanguage pf pr) M

Equations

s.subLanguageStructure = LO.FirstOrder.Structure.lMap L.ofSubLanguage s

source

noncomputable def LO.FirstOrder.Structure.extendStructure {L₁ L₂ : Language} (Φ : L₁.Hom L₂) {M : Type w} [Nonempty M] (s : Structure L₁ M) :

Structure L₂ M

Equations

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

Instances For

source

theorem LO.FirstOrder.Structure.extendStructure.func {L₁ L₂ : Language} {M : Type u} [Nonempty M] (s₁ : Structure L₁ M) (Φ : L₁.Hom L₂) {k : ℕ} (injf : Function.Injective Φ.func) (f₁ : L₁.Func k) (v : Fin k → M) :

func (Φ.func f₁) v = func f₁ v

source

theorem LO.FirstOrder.Structure.extendStructure.rel {L₁ L₂ : Language} {M : Type u} [Nonempty M] (s₁ : Structure L₁ M) (Φ : L₁.Hom L₂) {k : ℕ} (injr : Function.Injective Φ.rel) (r₁ : L₁.Rel k) (v : Fin k → M) :

rel (Φ.rel r₁) v ↔ rel r₁ v

source

theorem LO.FirstOrder.Structure.extendStructure.val_lMap {L₁ L₂ : Language} {M : Type u} [Nonempty M] (s₁ : Structure L₁ M) {μ : Type u_1} (Φ : L₁.Hom L₂) (injf : ∀ (k : ℕ), Function.Injective Φ.func) {n : ℕ} (e : Fin n → M) (ε : μ → M) (t : Semiterm L₁ μ n) :

Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ t) = Semiterm.val s₁ e ε t

source

theorem LO.FirstOrder.Structure.extendStructure.eval_lMap {L₁ L₂ : Language} {M : Type u} [Nonempty M] (s₁ : Structure L₁ M) {μ : Type u_1} (Φ : L₁.Hom L₂) (injf : ∀ (k : ℕ), Function.Injective Φ.func) (injr : ∀ (k : ℕ), Function.Injective Φ.rel) {n : ℕ} (e : Fin n → M) (ε : μ → M) {φ : Semiformula L₁ μ n} :

(Semiformula.Eval (extendStructure Φ s₁) e ε) ((Semiformula.lMap Φ) φ) ↔ (Semiformula.Eval s₁ e ε) φ

source

theorem LO.FirstOrder.Structure.extendStructure.models_lMap {L₁ L₂ : Language} {M : Type u} [Nonempty M] (s₁ : Structure L₁ M) (Φ : L₁.Hom L₂) (injf : ∀ (k : ℕ), Function.Injective Φ.func) (injr : ∀ (k : ℕ), Function.Injective Φ.rel) (φ : SyntacticFormula L₁) :

(extendStructure Φ s₁).toStruc ⊧ (Semiformula.lMap Φ) φ ↔ s₁.toStruc ⊧ φ

source

theorem LO.FirstOrder.lMap_models_lMap_iff {L₁ L₂ : Language} (Φ : L₁.Hom L₂) (injf : ∀ (k : ℕ), Function.Injective Φ.func) (injr : ∀ (k : ℕ), Function.Injective Φ.rel) {T : Theory L₁} {φ : SyntacticFormula L₁} :

Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) φ ↔ T ⊨ φ

source

theorem LO.FirstOrder.satisfiable_lMap {L₁ L₂ : Language} (Φ : L₁.Hom L₂) (injf : ∀ (k : ℕ), Function.Injective Φ.func) (injr : ∀ (k : ℕ), Function.Injective Φ.rel) {T : Theory L₁} (s : Satisfiable T) :

Satisfiable (⇑(Semiformula.lMap Φ) '' T)