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

Equations

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

def LO.FirstOrder.Language.ofSubLanguage (L : LO.FirstOrder.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 }

@[simp]

theorem LO.FirstOrder.Language.ofSubLanguage_onFunc (L : LO.FirstOrder.Language) : ∀ {pfunc : (k : ℕ) → L.Func k → Prop} {prel : (k : ℕ) → L.Rel k → Prop} {a : ℕ} {p : (L.subLanguage pfunc prel).Func a}, L.ofSubLanguage.func p = ↑p

@[simp]

theorem LO.FirstOrder.Language.ofSubLanguage_onRel (L : LO.FirstOrder.Language) : ∀ {pfunc : (k : ℕ) → L.Func k → Prop} {prel : (k : ℕ) → L.Rel k → Prop} {a : ℕ} {p : (L.subLanguage pfunc prel).Rel a}, L.ofSubLanguage.rel p = ↑p

def LO.FirstOrder.Semiterm.lang {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} : LO.FirstOrder.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)

@[simp]

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

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

def LO.FirstOrder.Semiterm.toSubLanguage' {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} (pf : (k : ℕ) → L.Func k → Prop) (pr : (k : ℕ) → L.Rel k → Prop) (t : LO.FirstOrder.Semiterm L μ n) : (∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ t.lang → pf k f) → LO.FirstOrder.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) ⋯

@[simp]

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

noncomputable def LO.FirstOrder.Semiformula.langFunc {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : ℕ} : LO.FirstOrder.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
• (p.and q).langFunc = p.langFunc ∪ q.langFunc
• (p.or q).langFunc = p.langFunc ∪ q.langFunc
• p.all.langFunc = p.langFunc
• p.ex.langFunc = p.langFunc

noncomputable def LO.FirstOrder.Semiformula.langRel {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : ℕ} : LO.FirstOrder.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⟩}
• (p.and q).langRel = p.langRel ∪ q.langRel
• (p.or q).langRel = p.langRel ∪ q.langRel
• p.all.langRel = p.langRel
• p.ex.langRel = p.langRel

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

def LO.FirstOrder.Semiformula.toSubLanguage' {L : LO.FirstOrder.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 : ℕ} (p : LO.FirstOrder.Semiformula L μ n) : (∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ p.langFunc → pf k f) → (∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ p.langRel → pr k r) → LO.FirstOrder.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 (p.and q) hf hr = LO.FirstOrder.Semiformula.toSubLanguage' pf pr p ⋯ ⋯ ⋏ LO.FirstOrder.Semiformula.toSubLanguage' pf pr q ⋯ ⋯
• LO.FirstOrder.Semiformula.toSubLanguage' pf pr (p.or q) hf hr = LO.FirstOrder.Semiformula.toSubLanguage' pf pr p ⋯ ⋯ ⋎ LO.FirstOrder.Semiformula.toSubLanguage' pf pr q ⋯ ⋯
• LO.FirstOrder.Semiformula.toSubLanguage' pf pr p.all hf hr = ∀' LO.FirstOrder.Semiformula.toSubLanguage' pf pr p hf hr
• LO.FirstOrder.Semiformula.toSubLanguage' pf pr p.ex hf hr = ∃' LO.FirstOrder.Semiformula.toSubLanguage' pf pr p hf hr

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_toSubLanguage' {L : LO.FirstOrder.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 : ℕ} (p : LO.FirstOrder.Semiformula L μ n) (hf : ∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ p.langFunc → pf k f) (hr : ∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ p.langRel → pr k r) : (LO.FirstOrder.Semiformula.lMap L.ofSubLanguage) (LO.FirstOrder.Semiformula.toSubLanguage' pf pr p hf hr) = p

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

Equations

• p.languageFuncIndexed k = p.langFunc.preimage (Sigma.mk k) ⋯

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

Equations

• p.languageRelIndexed k = p.langRel.preimage (Sigma.mk k) ⋯

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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