Finite sublanguage

def FFL.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) }

def FFL.FirstOrder.Language.unsub (L : Language) {pf : (k : ℕ) → L.Func k → Prop} {pr : (k : ℕ) → L.Rel k → Prop} : (L.sublanguage pf pr).Hom L

Equations

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

@[simp]

theorem FFL.FirstOrder.Language.unsub_onFunc (L : Language) {pFunc✝ : (k : ℕ) → L.Func k → Prop} {pRel✝ : (k : ℕ) → L.Rel k → Prop} {a✝ : ℕ} {φ : (L.sublanguage pFunc✝ pRel✝).Func a✝} : L.unsub.func φ = ↑φ

@[simp]

theorem FFL.FirstOrder.Language.unsub_onRel (L : Language) {pFunc✝ : (k : ℕ) → L.Func k → Prop} {pRel✝ : (k : ℕ) → L.Rel k → Prop} {a✝ : ℕ} {φ : (L.sublanguage pFunc✝ pRel✝).Rel a✝} : L.unsub.rel φ = ↑φ

def FFL.FirstOrder.Semiterm.symbols {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] {ξ : Type u_1} {n : ℕ} : Semiterm L ξ n → Finset ((k : ℕ) × L.Func k)

Equations

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

@[simp]

theorem FFL.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).symbols

theorem FFL.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).symbols ⊆ (func f v).symbols

def FFL.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.symbols → pf k f) → Semiterm (L.sublanguage pf pr) ξ n

Equations

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

@[simp]

theorem FFL.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.symbols → pf k f) : lMap L.unsub (toSublanguage pf pr t h) = t

noncomputable def FFL.FirstOrder.Semiformula.functionSymbols {L : Language} [L.DecidableEq] {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → Finset ((k : ℕ) × L.Func k)

Equations

• (FFL.FirstOrder.Semiformula.rel a v).functionSymbols = Finset.univ.biUnion fun (i : Fin arity) => (v i).symbols
• (FFL.FirstOrder.Semiformula.nrel a v).functionSymbols = Finset.univ.biUnion fun (i : Fin arity) => (v i).symbols
• FFL.FirstOrder.Semiformula.verum.functionSymbols = ∅
• FFL.FirstOrder.Semiformula.falsum.functionSymbols = ∅
• (φ.and ψ).functionSymbols = φ.functionSymbols ∪ ψ.functionSymbols
• (φ.or ψ).functionSymbols = φ.functionSymbols ∪ ψ.functionSymbols
• φ.all.functionSymbols = φ.functionSymbols
• φ.exs.functionSymbols = φ.functionSymbols

noncomputable def FFL.FirstOrder.Semiformula.relationSymbols {L : Language} [L.DecidableEq] {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → Finset ((k : ℕ) × L.Rel k)

Equations

• (FFL.FirstOrder.Semiformula.rel a v).relationSymbols = {⟨arity, a⟩}
• (FFL.FirstOrder.Semiformula.nrel a v).relationSymbols = {⟨arity, a⟩}
• FFL.FirstOrder.Semiformula.verum.relationSymbols = ∅
• FFL.FirstOrder.Semiformula.falsum.relationSymbols = ∅
• (φ.and ψ).relationSymbols = φ.relationSymbols ∪ ψ.relationSymbols
• (φ.or ψ).relationSymbols = φ.relationSymbols ∪ ψ.relationSymbols
• φ.all.relationSymbols = φ.relationSymbols
• φ.exs.relationSymbols = φ.relationSymbols

theorem FFL.FirstOrder.Semiformula.functionSymbols_rel_ss {L : Language} [L.DecidableEq] {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) (i : Fin k) : (v i).symbols ⊆ (rel r v).functionSymbols

def FFL.FirstOrder.Semiformula.toSublanguage {L : Language} [L.DecidableEq] {ξ : 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⟩ ∈ φ.functionSymbols → pf k f) → (∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ φ.relationSymbols → pr k r) → Semiformula (L.sublanguage pf pr) ξ n

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.Semiformula.toSublanguage pf pr FFL.FirstOrder.Semiformula.verum x_3 x_4 = ⊤
• FFL.FirstOrder.Semiformula.toSublanguage pf pr FFL.FirstOrder.Semiformula.falsum x_3 x_4 = ⊥
• FFL.FirstOrder.Semiformula.toSublanguage pf pr (φ.and ψ) hf hr = FFL.FirstOrder.Semiformula.toSublanguage pf pr φ ⋯ ⋯ ⋏ FFL.FirstOrder.Semiformula.toSublanguage pf pr ψ ⋯ ⋯
• FFL.FirstOrder.Semiformula.toSublanguage pf pr (φ.or ψ) hf hr = FFL.FirstOrder.Semiformula.toSublanguage pf pr φ ⋯ ⋯ ⋎ FFL.FirstOrder.Semiformula.toSublanguage pf pr ψ ⋯ ⋯
• FFL.FirstOrder.Semiformula.toSublanguage pf pr φ.all hf hr = ∀¹ FFL.FirstOrder.Semiformula.toSublanguage pf pr φ hf hr
• FFL.FirstOrder.Semiformula.toSublanguage pf pr φ.exs hf hr = ∃¹ FFL.FirstOrder.Semiformula.toSublanguage pf pr φ hf hr

@[simp]

theorem FFL.FirstOrder.Semiformula.lMap_toSublanguage {L : Language} [L.DecidableEq] {ξ : 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⟩ ∈ φ.functionSymbols → pf k f) (hr : ∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ φ.relationSymbols → pr k r) : (lMap L.unsub) (toSublanguage pf pr φ hf hr) = φ

@[reducible, inline]

abbrev FFL.FirstOrder.Semiformula.sublanguage {ξ : Type u_1} {n : ℕ} {L : Language} [L.DecidableEq] (φ : Semiformula L ξ n) : Language

A language consists of the function and relation symbols appearing in a given finite set of formulas.

Equations

• φ.sublanguage = L.sublanguage (fun (k : ℕ) (f : L.Func k) => ⟨k, f⟩ ∈ φ.functionSymbols) fun (k : ℕ) (r : L.Rel k) => ⟨k, r⟩ ∈ φ.relationSymbols

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Semiformula.instFintypeFuncSublanguage {ξ : Type u_1} {n : ℕ} {L : Language} [L.DecidableEq] (φ : Semiformula L ξ n) (k : ℕ) : Fintype (φ.sublanguage.Func k)

Equations

• φ.instFintypeFuncSublanguage k = Fintype.subtype (φ.functionSymbols.preimage (fun (x : L.Func k) => ⟨k, x⟩) ⋯) ⋯

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Semiformula.instFintypeRelSublanguage {ξ : Type u_1} {n : ℕ} {L : Language} [L.DecidableEq] (φ : Semiformula L ξ n) (k : ℕ) : Fintype (φ.sublanguage.Rel k)

Equations

• φ.instFintypeRelSublanguage k = Fintype.subtype (φ.relationSymbols.preimage (fun (x : L.Rel k) => ⟨k, x⟩) ⋯) ⋯

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Semiformula.instEncodableSublanguage {ξ : Type u_1} {n : ℕ} {L : Language} [L.DecidableEq] (φ : Semiformula L ξ n) : φ.sublanguage.Encodable

Equations

• φ.instEncodableSublanguage = { func := fun (x : ℕ) => Fintype.toEncodable (φ.sublanguage.Func x), rel := fun (x : ℕ) => Fintype.toEncodable (φ.sublanguage.Rel x) }

def FFL.FirstOrder.Semiformula.toSubLanguageSelf {ξ : Type u_1} {n : ℕ} {L : Language} [L.DecidableEq] (φ : Semiformula L ξ n) : Semiformula φ.sublanguage ξ n

Equations

• φ.toSubLanguageSelf = FFL.FirstOrder.Semiformula.toSublanguage (fun (k : ℕ) (f : L.Func k) => ⟨k, f⟩ ∈ φ.functionSymbols) (fun (k : ℕ) (r : L.Rel k) => ⟨k, r⟩ ∈ φ.relationSymbols) φ ⋯ ⋯

@[simp]

theorem FFL.FirstOrder.Semiformula.lMap_toSubLanguage {ξ : Type u_1} {n : ℕ} {L : Language} [L.DecidableEq] {φ : Semiformula L ξ n} : (lMap L.unsub) φ.toSubLanguageSelf = φ

Tarski.Structure induced by an injective language homomorphism

class FFL.FirstOrder.Language.Hom.Injective {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) : Prop

• func (k : ℕ) : Function.Injective Φ.func
• rel (k : ℕ) : Function.Injective Φ.rel

instance FFL.FirstOrder.Language.unsub_injective {L : Language} (pf : (k : ℕ) → L.Func k → Prop) (pr : (k : ℕ) → L.Rel k → Prop) : L.unsub.Injective

@[reducible, inline]

noncomputable abbrev FFL.FirstOrder.Tarski.Structure.extendStructure {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) {M : Type u_1} [Nonempty M] (s : Structure L₁ M) : Structure L₂ M

Equations

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

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

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

theorem FFL.FirstOrder.Tarski.Structure.extendStructure.val_lMap {L₁ : Language} {M : Type u_1} [Nonempty M] (s₁ : Structure L₁ M) {L₂ : Language} {n : ℕ} {ξ : Type u_3} (Φ : L₁.Hom L₂) [Φ.Injective] (bv : Fin n → M) (fv : ξ → M) (t : Semiterm L₁ ξ n) : Semiterm.val bv fv (Semiterm.lMap Φ t) = Semiterm.val bv fv t

theorem FFL.FirstOrder.Tarski.Structure.extendStructure.eval_lMap {L₁ : Language} {M : Type u_1} [Nonempty M] (s₁ : Structure L₁ M) {L₂ : Language} {n : ℕ} {ξ : Type u_3} (Φ : L₁.Hom L₂) [Φ.Injective] (bv : Fin n → M) (fv : ξ → M) {φ : Semiformula L₁ ξ n} : (Semiformula.Eval bv fv) ((Semiformula.lMap Φ) φ) ↔ (Semiformula.Eval bv fv) φ

theorem FFL.FirstOrder.Tarski.Structure.extendStructure.models_lMap {L₁ : Language} {M : Type u_1} [Nonempty M] (s₁ : Structure L₁ M) {L₂ : Language} (Φ : L₁.Hom L₂) [Φ.Injective] (φ : Sentence L₁) : (extendStructure Φ s₁).toStruc ⊧ (Semiformula.lMap Φ) φ ↔ s₁.toStruc ⊧ φ

theorem FFL.FirstOrder.lMap_models_lMap_iff {L₁ L₂ : Language} (Φ : L₁.Hom L₂) [Φ.Injective] {T : Theory L₁} {φ : Sentence L₁} : Consequence (Theory.lMap Φ T) ((Semiformula.lMap Φ) φ) ↔ Consequence T φ

theorem FFL.FirstOrder.satisfiable_lMap {L₁ L₂ : Language} (Φ : L₁.Hom L₂) [Φ.Injective] {T : Theory L₁} (s : Satisfiable T) : Satisfiable (Theory.lMap Φ T)