Documentation

Foundation.FirstOrder.Completeness.SubLanguage

def LO.FirstOrder.Language.subLanguage (L : Language) (pfunc : (k : ) → L.Func kProp) (prel : (k : ) → L.Rel kProp) :
Equations
  • L.subLanguage pfunc prel = { Func := fun (k : ) => Subtype (pfunc k), Rel := fun (k : ) => Subtype (prel k) }
Instances For
def LO.FirstOrder.Language.ofSubLanguage (L : Language) {pf : (k : ) → L.Func kProp} {pr : (k : ) → L.Rel kProp} :
(L.subLanguage pf pr).Hom L
Equations
@[simp]
theorem LO.FirstOrder.Language.ofSubLanguage_onFunc (L : Language) {pfunc✝ : (k : ) → L.Func kProp} {prel✝ : (k : ) → L.Rel kProp} {a✝ : } {φ : (L.subLanguage pfunc✝ prel✝).Func a✝} :
L.ofSubLanguage.func φ = φ
@[simp]
theorem LO.FirstOrder.Language.ofSubLanguage_onRel (L : Language) {pfunc✝ : (k : ) → L.Func kProp} {prel✝ : (k : ) → L.Rel kProp} {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 μ nFinset ((k : ) × L.Func k)
Equations
@[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 kSemiterm 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 kSemiterm 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 kProp) (pr : (k : ) → L.Rel kProp) (t : Semiterm L μ n) :
(∀ (k : ) (f : L.Func k), k, f t.langpf k f)Semiterm (L.subLanguage pf pr) μ n
Equations
@[simp]
theorem LO.FirstOrder.Semiterm.lMap_toSubLanguage' {L : Language} [(k : ) → DecidableEq (L.Func k)] {μ : Type u_1} {n : } (pf : (k : ) → L.Func kProp) (pr : (k : ) → L.Rel kProp) (t : Semiterm L μ n) (h : ∀ (k : ) (f : L.Func k), k, f t.langpf 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 μ nFinset ((k : ) × L.Func k)
Equations
noncomputable def LO.FirstOrder.Semiformula.langRel {L : Language} [(k : ) → DecidableEq (L.Rel k)] {μ : Type u_1} {n : } :
Semiformula L μ nFinset ((k : ) × L.Rel k)
Equations
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 kSemiterm 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 kProp) (pr : (k : ) → L.Rel kProp) {n : } (φ : Semiformula L μ n) :
(∀ (k : ) (f : L.Func k), k, f φ.langFuncpf k f)(∀ (k : ) (r : L.Rel k), k, r φ.langRelpr k r)Semiformula (L.subLanguage pf pr) μ n
Equations
@[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 kProp) (pr : (k : ) → L.Rel kProp) {n : } (φ : Semiformula L μ n) (hf : ∀ (k : ) (f : L.Func k), k, f φ.langFuncpf k f) (hr : ∀ (k : ) (r : L.Rel k), k, r φ.langRelpr 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)
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)
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)) :
Equations
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
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
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 : φ Γ) :
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 LO.FirstOrder.Structure.subLanguageStructure {L : Language} {pf : (k : ) → L.Func kProp} {pr : (k : ) → L.Rel kProp} {M : Type w} (s : Structure L M) :
Structure (L.subLanguage pf pr) M
Equations
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.
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 kM) :
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 kM) :
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 nM) (ε : μ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 nM) (ε : μ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₁} :
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) :