SubLanguage

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[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 φ = ↑φ

@[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 φ = ↑φ

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

Imported declaration from the Incompleteness formalization.

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 : 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

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

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

Imported declaration from the Incompleteness formalization.

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 : 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

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)

Imported declaration from the Incompleteness formalization.

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

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)

Imported declaration from the Incompleteness formalization.

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

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

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

Imported declaration from the Incompleteness formalization.

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

@[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) = φ

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)

Imported declaration from the Incompleteness formalization.

Equations

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

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)

Imported declaration from the Incompleteness formalization.

Equations

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

@[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

Imported declaration from the Incompleteness formalization.

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

@[instance_reducible]

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) ⋯

@[instance_reducible]

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) ⋯

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[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) = φ

@[instance_reducible]

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

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

@[reducible]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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 ε) φ

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 ⊧ φ

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 ⊨ φ

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)