def
LO.FirstOrder.Language.subLanguage
(L : LO.FirstOrder.Language)
(pfunc : (k : ℕ) → L.Func k → Prop)
(prel : (k : ℕ) → L.Rel k → Prop)
:
Equations
Instances For
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
Instances For
@[simp]
@[simp]
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)
Instances For
@[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) ⋯
Instances For
@[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
Instances For
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
Instances For
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
Instances For
@[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)
Instances For
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)
Instances For
@[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))
:
Equations
Instances For
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 ∈ Γ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
: