Flypitch.LanguageExtension studies maps between first-order languages and how they act on terms, formulas, proofs, and structures. It also records the symbol-filtering and reflection constructions used later in the Henkin and completeness arguments.

def Flypitch.fol.Language.Lconstants (α : Type u) : Language

Equations

• Flypitch.fol.Language.Lconstants α = { functions := fun (n : ℕ) => match n with | 0 => α | n.succ => PEmpty.{?u.12 + 1}, relations := fun (x : ℕ) => PEmpty.{?u.12 + 1} }

def Flypitch.fol.Language.sum (L : Language) (L' : Language) : Language

Equations

• L.sum L' = { functions := fun (n : ℕ) => L.functions n ⊕ L'.functions n, relations := fun (n : ℕ) => L.relations n ⊕ L'.relations n }

def Flypitch.fol.Language.symbols (L : Language) : Type u_1

Equations

• L.symbols = ((l : ℕ) × L.functions l ⊕ (l : ℕ) × L.relations l)

def Flypitch.fol.symbols_in_term {L : Language} {l : ℕ} : preterm L l → Set L.symbols

Equations

• Flypitch.fol.symbols_in_term &a = ∅
• Flypitch.fol.symbols_in_term (Flypitch.fol.preterm.func f) = {Sum.inl ⟨x✝, f⟩}
• Flypitch.fol.symbols_in_term (t₁.app t₂) = Flypitch.fol.symbols_in_term t₁ ∪ Flypitch.fol.symbols_in_term t₂

def Flypitch.fol.symbols_in_formula {L : Language} {l : ℕ} : preformula L l → Set L.symbols

Equations

• Flypitch.fol.symbols_in_formula Flypitch.fol.preformula.falsum = ∅
• Flypitch.fol.symbols_in_formula (t₁ ≃ t₂) = Flypitch.fol.symbols_in_term t₁ ∪ Flypitch.fol.symbols_in_term t₂
• Flypitch.fol.symbols_in_formula (Flypitch.fol.preformula.rel R) = {Sum.inr ⟨x✝, R⟩}
• Flypitch.fol.symbols_in_formula (f.apprel t) = Flypitch.fol.symbols_in_formula f ∪ Flypitch.fol.symbols_in_term t
• Flypitch.fol.symbols_in_formula (f₁ ⟹ f₂) = Flypitch.fol.symbols_in_formula f₁ ∪ Flypitch.fol.symbols_in_formula f₂
• Flypitch.fol.symbols_in_formula (∀' f) = Flypitch.fol.symbols_in_formula f

@[simp]

theorem Flypitch.fol.symbols_in_term_lift_at {L : Language} (n m : ℕ) {l : ℕ} (t : preterm L l) : symbols_in_term (t ↑' n # m) = symbols_in_term t

@[simp]

theorem Flypitch.fol.symbols_in_term_lift {L : Language} (n : ℕ) {l : ℕ} (t : preterm L l) : symbols_in_term (t ↑ n) = symbols_in_term t

theorem Flypitch.fol.symbols_in_term_subst {L : Language} (s : term L) (n : ℕ) {l : ℕ} (t : preterm L l) : symbols_in_term (t[s // n]) ⊆ symbols_in_term t ∪ symbols_in_term s

theorem Flypitch.fol.symbols_in_formula_subst {L : Language} {l : ℕ} (f : preformula L l) (s : term L) (n : ℕ) : symbols_in_formula (subst_formula f s n) ⊆ symbols_in_formula f ∪ symbols_in_term s

structure Flypitch.fol.Lhom (L L' : Language) : Type u

• on_function {n : ℕ} : L.functions n → L'.functions n
• on_relation {n : ℕ} : L.relations n → L'.relations n

def Flypitch.fol.«term_→ᴸ_» : Lean.TrailingParserDescr

Equations

• Flypitch.fol.«term_→ᴸ_» = Lean.ParserDescr.trailingNode `Flypitch.fol.«term_→ᴸ_» 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᴸ ") (Lean.ParserDescr.cat `term 11))

def Flypitch.fol.Lhom.id (L : Language) : L →ᴸ L

Equations

• Flypitch.fol.Lhom.id L = { on_function := fun {n : ℕ} (x : L.functions n) => x, on_relation := fun {n : ℕ} (x : L.relations n) => x }

def Flypitch.fol.Lhom.sum_inl {L L' : Language} : L →ᴸ L.sum L'

Equations

• Flypitch.fol.Lhom.sum_inl = { on_function := fun {n : ℕ} (f : L.functions n) => Sum.inl f, on_relation := fun {n : ℕ} (R : L.relations n) => Sum.inl R }

def Flypitch.fol.Lhom.sum_inr {L L' : Language} : L' →ᴸ L.sum L'

Equations

• Flypitch.fol.Lhom.sum_inr = { on_function := fun {n : ℕ} (f : L'.functions n) => Sum.inr f, on_relation := fun {n : ℕ} (R : L'.relations n) => Sum.inr R }

@[reducible]

def Flypitch.fol.Lhom.comp {L₁ L₂ L₃ : Language} (g : L₂ →ᴸ L₃) (f : L₁ →ᴸ L₂) : L₁ →ᴸ L₃

Equations

• g.comp f = { on_function := fun {n : ℕ} (x : L₁.functions n) => g.on_function (f.on_function x), on_relation := fun {n : ℕ} (x : L₁.relations n) => g.on_relation (f.on_relation x) }

theorem Flypitch.fol.Lhom.Lhom_funext {L₁ L₂ : Language} {F G : L₁ →ᴸ L₂} (h_fun : ∀ (n : ℕ) (x : L₁.functions n), F.on_function x = G.on_function x) (h_rel : ∀ (n : ℕ) (x : L₁.relations n), F.on_relation x = G.on_relation x) : F = G

theorem Flypitch.fol.Lhom.ext {L₁ L₂ : Language} {F G : L₁ →ᴸ L₂} (h_fun : ∀ (n : ℕ) (x : L₁.functions n), F.on_function x = G.on_function x) (h_rel : ∀ (n : ℕ) (x : L₁.relations n), F.on_relation x = G.on_relation x) : F = G

theorem Flypitch.fol.Lhom.ext_iff {L₁ L₂ : Language} {F G : L₁ →ᴸ L₂} : F = G ↔ (∀ (n : ℕ) (x : L₁.functions n), F.on_function x = G.on_function x) ∧ ∀ (n : ℕ) (x : L₁.relations n), F.on_relation x = G.on_relation x

@[simp]

theorem Flypitch.fol.Lhom.id_is_left_identity {L₁ L₂ : Language} {F : L₁ →ᴸ L₂} : (Lhom.id L₂).comp F = F

@[simp]

theorem Flypitch.fol.Lhom.id_is_right_identity {L₁ L₂ : Language} {F : L₁ →ᴸ L₂} : F.comp (Lhom.id L₁) = F

@[simp]

theorem Flypitch.fol.Lhom.comp_assoc {L₁ L₂ L₃ L₀ : Language} (g : L₂ →ᴸ L₃) (f : L₁ →ᴸ L₂) (e : L₀ →ᴸ L₁) : (g.comp f).comp e = g.comp (f.comp e)

@[simp]

theorem Flypitch.fol.Lhom.comp_on_function {L₁ L₂ L₃ : Language} (g : L₂ →ᴸ L₃) (f : L₁ →ᴸ L₂) {n : ℕ} (x : L₁.functions n) : (g.comp f).on_function x = g.on_function (f.on_function x)

@[simp]

theorem Flypitch.fol.Lhom.comp_on_relation {L₁ L₂ L₃ : Language} (g : L₂ →ᴸ L₃) (f : L₁ →ᴸ L₂) {n : ℕ} (x : L₁.relations n) : (g.comp f).on_relation x = g.on_relation (f.on_relation x)

structure Flypitch.fol.Lhom.is_injective {L L' : Language} (ϕ : L →ᴸ L') : Prop

• on_function {n : ℕ} : Function.Injective ϕ.on_function
• on_relation {n : ℕ} : Function.Injective ϕ.on_relation

class Flypitch.fol.Lhom.has_decidable_range {L L' : Language} (ϕ : L →ᴸ L') : Type u

• on_function {n : ℕ} : DecidablePred (Set.range ϕ.on_function)
• on_relation {n : ℕ} : DecidablePred (Set.range ϕ.on_relation)

def Flypitch.fol.Lhom.on_symbol {L L' : Language} (ϕ : L →ᴸ L') : L.symbols → L'.symbols

Equations

• ϕ.on_symbol (Sum.inl ⟨l, f⟩) = Sum.inl ⟨l, ϕ.on_function f⟩
• ϕ.on_symbol (Sum.inr ⟨l, R⟩) = Sum.inr ⟨l, ϕ.on_relation R⟩

def Flypitch.fol.Lhom.on_term {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} : preterm L l → preterm L' l

Equations

• ϕ.on_term &a = &a
• ϕ.on_term (Flypitch.fol.preterm.func f) = Flypitch.fol.preterm.func (ϕ.on_function f)
• ϕ.on_term (t₁.app t₂) = (ϕ.on_term t₁).app (ϕ.on_term t₂)

@[simp]

theorem Flypitch.fol.Lhom.on_term_lift_at {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (t : preterm L l) (n m : ℕ) : ϕ.on_term (t ↑' n # m) = ϕ.on_term t ↑' n # m

@[simp]

theorem Flypitch.fol.Lhom.on_term_lift {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (n : ℕ) (t : preterm L l) : ϕ.on_term (t ↑ n) = ϕ.on_term t ↑ n

@[simp]

theorem Flypitch.fol.Lhom.on_term_subst {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (t : preterm L l) (s : term L) (n : ℕ) : ϕ.on_term (t[s // n]) = ϕ.on_term t[ϕ.on_term s // n]

@[simp]

theorem Flypitch.fol.Lhom.on_term_apps {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (t : preterm L l) (ts : dvector (term L) l) : ϕ.on_term (apps t ts) = apps (ϕ.on_term t) (dvector.map ϕ.on_term ts)

@[simp]

theorem Flypitch.fol.Lhom.on_term_comp {L L' L₂ : Language} (ψ : L' →ᴸ L₂) (ϕ : L →ᴸ L') {l : ℕ} (t : preterm L l) : (ψ.comp ϕ).on_term t = ψ.on_term (ϕ.on_term t)

@[simp]

theorem Flypitch.fol.Lhom.on_term_id {L : Language} {l : ℕ} (t : preterm L l) : (Lhom.id L).on_term t = t

theorem Flypitch.fol.Lhom.not_mem_symbols_in_term_on_term {L L' : Language} (ϕ : L →ᴸ L') {s : L'.symbols} (h : s ∉ Set.range ϕ.on_symbol) {l : ℕ} (t : preterm L l) : s ∉ symbols_in_term (ϕ.on_term t)

def Flypitch.fol.Lhom.on_formula {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} : preformula L l → preformula L' l

Equations

• ϕ.on_formula Flypitch.fol.preformula.falsum = ⊥
• ϕ.on_formula (t₁ ≃ t₂) = ϕ.on_term t₁ ≃ ϕ.on_term t₂
• ϕ.on_formula (Flypitch.fol.preformula.rel R) = Flypitch.fol.preformula.rel (ϕ.on_relation R)
• ϕ.on_formula (f.apprel t) = (ϕ.on_formula f).apprel (ϕ.on_term t)
• ϕ.on_formula (f₁ ⟹ f₂) = ϕ.on_formula f₁ ⟹ ϕ.on_formula f₂
• ϕ.on_formula (∀' f) = ∀' ϕ.on_formula f

@[simp]

theorem Flypitch.fol.Lhom.on_formula_lift_at {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (n m : ℕ) (f : preformula L l) : ϕ.on_formula (lift_formula_at f n m) = lift_formula_at (ϕ.on_formula f) n m

@[simp]

theorem Flypitch.fol.Lhom.on_formula_lift {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (n : ℕ) (f : preformula L l) : ϕ.on_formula (lift_formula f n) = lift_formula (ϕ.on_formula f) n

@[simp]

theorem Flypitch.fol.Lhom.on_formula_subst {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (f : preformula L l) (s : term L) (n : ℕ) : ϕ.on_formula (subst_formula f s n) = subst_formula (ϕ.on_formula f) (ϕ.on_term s) n

@[simp]

theorem Flypitch.fol.Lhom.on_formula_apps_rel {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (f : preformula L l) (ts : dvector (term L) l) : ϕ.on_formula (apps_rel f ts) = apps_rel (ϕ.on_formula f) (dvector.map ϕ.on_term ts)

@[simp]

theorem Flypitch.fol.Lhom.on_formula_comp {L L' L₂ : Language} (ψ : L' →ᴸ L₂) (ϕ : L →ᴸ L') {l : ℕ} (f : preformula L l) : (ψ.comp ϕ).on_formula f = ψ.on_formula (ϕ.on_formula f)

@[simp]

theorem Flypitch.fol.Lhom.on_formula_id {L : Language} {l : ℕ} (f : preformula L l) : (Lhom.id L).on_formula f = f

theorem Flypitch.fol.Lhom.not_mem_symbols_in_formula_on_formula {L L' : Language} (ϕ : L →ᴸ L') {s : L'.symbols} (h : s ∉ Set.range ϕ.on_symbol) {l : ℕ} (f : preformula L l) : s ∉ symbols_in_formula (ϕ.on_formula f)

theorem Flypitch.fol.Lhom.not_mem_function_in_formula_on_formula {L L' : Language} (ϕ : L →ᴸ L') {l' : ℕ} {f' : L'.functions l'} (h : f' ∉ Set.range ϕ.on_function) {l : ℕ} (f : preformula L l) : Sum.inl ⟨l', f'⟩ ∉ symbols_in_formula (ϕ.on_formula f)

theorem Flypitch.fol.Lhom.bounded_term_at_on_term {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} {t : preterm L l} {n : ℕ} : bounded_term_at t n → bounded_term_at (ϕ.on_term t) n

theorem Flypitch.fol.Lhom.bounded_formula_at_on_formula {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} {f : preformula L l} {n : ℕ} : bounded_formula_at f n → bounded_formula_at (ϕ.on_formula f) n

def Flypitch.fol.Lhom.on_bounded_term {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (t : bounded_preterm L n l) : bounded_preterm L' n l

Equations

• ϕ.on_bounded_term t = ⟨ϕ.on_term ↑t, ⋯⟩

@[simp]

theorem Flypitch.fol.Lhom.on_bounded_term_fst {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (t : bounded_preterm L n l) : (ϕ.on_bounded_term t).fst = ϕ.on_term t.fst

theorem Flypitch.fol.Lhom.on_bounded_term_comp {L L' L₂ : Language} (ψ : L' →ᴸ L₂) (ϕ : L →ᴸ L') {n l : ℕ} (t : bounded_preterm L n l) : (ψ.comp ϕ).on_bounded_term t = ψ.on_bounded_term (ϕ.on_bounded_term t)

theorem Flypitch.fol.Lhom.on_bounded_term_id {L : Language} {n l : ℕ} (t : bounded_preterm L n l) : (Lhom.id L).on_bounded_term t = t

def Flypitch.fol.Lhom.on_bounded_formula {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (f : bounded_preformula L n l) : bounded_preformula L' n l

Equations

• ϕ.on_bounded_formula f = ⟨ϕ.on_formula ↑f, ⋯⟩

@[simp]

theorem Flypitch.fol.Lhom.on_bounded_formula_fst {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (f : bounded_preformula L n l) : (ϕ.on_bounded_formula f).fst = ϕ.on_formula f.fst

theorem Flypitch.fol.Lhom.on_bounded_formula_comp {L L' L₂ : Language} (ψ : L' →ᴸ L₂) (ϕ : L →ᴸ L') {n l : ℕ} (f : bounded_preformula L n l) : (ψ.comp ϕ).on_bounded_formula f = ψ.on_bounded_formula (ϕ.on_bounded_formula f)

theorem Flypitch.fol.Lhom.on_bounded_formula_id {L : Language} {n l : ℕ} (f : bounded_preformula L n l) : (Lhom.id L).on_bounded_formula f = f

def Flypitch.fol.Lhom.on_closed_term {L L' : Language} (ϕ : L →ᴸ L') (t : closed_term L) : closed_term L'

Equations

• ϕ.on_closed_term t = ϕ.on_bounded_term t

def Flypitch.fol.Lhom.on_sentence {L L' : Language} (ϕ : L →ᴸ L') (f : sentence L) : sentence L'

Equations

• ϕ.on_sentence f = ⟨ϕ.on_formula ↑f, ⋯⟩

@[simp]

theorem Flypitch.fol.Lhom.on_sentence_fst {L L' : Language} (ϕ : L →ᴸ L') (f : sentence L) : ↑(ϕ.on_sentence f) = ϕ.on_formula ↑f

@[reducible]

def Flypitch.fol.Lhom.filter_symbols {L : Language} (p : L.symbols → Prop) : Language

Equations

• Flypitch.fol.Lhom.filter_symbols p = { functions := fun (l : ℕ) => { f : L.functions l // p (Sum.inl ⟨l, f⟩) }, relations := fun (l : ℕ) => { R : L.relations l // p (Sum.inr ⟨l, R⟩) } }

def Flypitch.fol.Lhom.filter_symbols_Lhom {L : Language} (p : L.symbols → Prop) : filter_symbols p →ᴸ L

Equations

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

theorem Flypitch.fol.Lhom.is_injective_filter_symbols_Lhom {L : Language} (p : L.symbols → Prop) : (filter_symbols_Lhom p).is_injective

def Flypitch.fol.Lhom.find_term_filter_symbols {L : Language} (p : L.symbols → Prop) {l : ℕ} (t : preterm L l) : symbols_in_term t ⊆ {s : L.symbols | p s} → (t' : preterm (filter_symbols p) l) ×' (filter_symbols_Lhom p).on_term t' = t

Equations

• One or more equations did not get rendered due to their size.
• Flypitch.fol.Lhom.find_term_filter_symbols p (&k) x_3 = ⟨&k, ⋯⟩
• Flypitch.fol.Lhom.find_term_filter_symbols p (Flypitch.fol.preterm.func f) h = ⟨Flypitch.fol.preterm.func ⟨f, ⋯⟩, ⋯⟩

def Flypitch.fol.Lhom.find_formula_filter_symbols {L : Language} (p : L.symbols → Prop) {l : ℕ} (f : preformula L l) : symbols_in_formula f ⊆ {s : L.symbols | p s} → (f' : preformula (filter_symbols p) l) ×' (filter_symbols_Lhom p).on_formula f' = f

Equations

• One or more equations did not get rendered due to their size.
• Flypitch.fol.Lhom.find_formula_filter_symbols p Flypitch.fol.preformula.falsum x_3 = ⟨⊥, ⋯⟩
• Flypitch.fol.Lhom.find_formula_filter_symbols p (Flypitch.fol.preformula.rel R) h = ⟨Flypitch.fol.preformula.rel ⟨R, ⋯⟩, ⋯⟩

noncomputable def Flypitch.fol.Lhom.on_prf {L L' : Language} (ϕ : L →ᴸ L') {Γ : Set (formula L)} {f : formula L} (h : Γ ⊢ f) : ϕ.on_formula '' Γ ⊢ ϕ.on_formula f

Equations

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

@[reducible]

def Flypitch.fol.Lhom.Theory_induced {L L' : Language} (ϕ : L →ᴸ L') (T : Theory L) : Theory L'

Equations

• ϕ.Theory_induced T = { carrier := ϕ.on_sentence '' T.carrier }

@[simp]

theorem Flypitch.fol.Lhom.Theory_induced_fst {L L' : Language} (ϕ : L →ᴸ L') (T : Theory L) : (ϕ.Theory_induced T).fst = ϕ.on_formula '' T.fst

noncomputable def Flypitch.fol.Lhom.on_sprf {L L' : Language} (ϕ : L →ᴸ L') {T : Theory L} {f : sentence L} (h : T ⊢ f) : ϕ.Theory_induced T ⊢ ϕ.on_sentence f

Equations

• ϕ.on_sprf h = ⋯.mpr (ϕ.on_prf h)

theorem Flypitch.fol.Lhom.on_term_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.is_injective) {l : ℕ} : Function.Injective ϕ.on_term

theorem Flypitch.fol.Lhom.on_formula_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.is_injective) {l : ℕ} : Function.Injective ϕ.on_formula

theorem Flypitch.fol.Lhom.on_bounded_term_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.is_injective) {n l : ℕ} : Function.Injective ϕ.on_bounded_term

theorem Flypitch.fol.Lhom.on_bounded_formula_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.is_injective) {n l : ℕ} : Function.Injective ϕ.on_bounded_formula

def Flypitch.fol.Lhom.reduct {L L' : Language} (ϕ : L →ᴸ L') (M : Structure L') : Structure L

Equations

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

@[simp]

theorem Flypitch.fol.Lhom.reduct_coe {L L' : Language} (ϕ : L →ᴸ L') (M : Structure L') : (ϕ.reduct M).carrier = M.carrier

@[simp]

theorem Flypitch.fol.Lhom.reduct_term_eq {L L' : Language} (ϕ : L →ᴸ L') {M : Structure L'} {l : ℕ} (v : ℕ → M.carrier) (t : preterm L l) (xs : dvector M.carrier l) : realize_term v (ϕ.on_term t) xs = realize_term v t xs

theorem Flypitch.fol.Lhom.reduct_formula_iff {L L' : Language} (ϕ : L →ᴸ L') {M : Structure L'} {l : ℕ} (v : ℕ → M.carrier) (f : preformula L l) (xs : dvector M.carrier l) : realize_formula v (ϕ.on_formula f) xs ↔ realize_formula v f xs

theorem Flypitch.fol.Lhom.reduct_realize_sentence {L L' : Language} (ϕ : L →ᴸ L') {M : Structure L'} {f : sentence L} : realize_sentence M (ϕ.on_sentence f) ↔ realize_sentence (ϕ.reduct M) f

theorem Flypitch.fol.Lhom.reduct_all_realize_sentence {L L' : Language} (ϕ : L →ᴸ L') {M : Structure L'} {T : Theory L} (h : all_realize_sentence M (ϕ.Theory_induced T)) : all_realize_sentence (ϕ.reduct M) T

theorem Flypitch.fol.Lhom.reduct_nonempty_of_nonempty {L L' : Language} (ϕ : L →ᴸ L') {M : Structure L'} (h : Nonempty M.carrier) : Nonempty (ϕ.reduct M).carrier

noncomputable def Flypitch.fol.Lhom.reflect_term {L L' : Language} (ϕ : L →ᴸ L') [hdec : ϕ.has_decidable_range] (t : term L') (m : ℕ) : term L

Equations

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

theorem Flypitch.fol.Lhom.reflect_term_apps_pos {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] {l : ℕ} {f : L'.functions l} (hf : f ∈ Set.range ϕ.on_function) (ts : dvector (term L') l) (m : ℕ) : ϕ.reflect_term (apps (preterm.func f) ts) m = apps (preterm.func (Classical.choose hf)) (dvector.map (fun (t : term L') => ϕ.reflect_term t m) ts)

theorem Flypitch.fol.Lhom.reflect_term_apps_neg {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] {l : ℕ} {f : L'.functions l} (hf : f ∉ Set.range ϕ.on_function) (ts : dvector (term L') l) (m : ℕ) : ϕ.reflect_term (apps (preterm.func f) ts) m = &m

theorem Flypitch.fol.Lhom.reflect_term_const_pos {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] {c : L'.constants} (hf : c ∈ Set.range ϕ.on_function) (m : ℕ) : ϕ.reflect_term (preterm.func c) m = preterm.func (Classical.choose hf)

theorem Flypitch.fol.Lhom.reflect_term_const_neg {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] {c : L'.constants} (hf : c ∉ Set.range ϕ.on_function) (m : ℕ) : ϕ.reflect_term (preterm.func c) m = &m

@[simp]

theorem Flypitch.fol.Lhom.reflect_term_var {L L' : Language} (ϕ : L →ᴸ L') [hdec : ϕ.has_decidable_range] (k m : ℕ) : ϕ.reflect_term (&k) m = &k ↑' 1 # m

@[simp]

theorem Flypitch.fol.Lhom.reflect_term_on_term {L L' : Language} (ϕ : L →ᴸ L') [hdec : ϕ.has_decidable_range] (hϕ : ϕ.is_injective) (t : term L) (m : ℕ) : ϕ.reflect_term (ϕ.on_term t) m = t ↑' 1 # m

theorem Flypitch.fol.Lhom.reflect_term_lift_at {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {n m m' : ℕ} (h : m ≤ m') (t : term L') : ϕ.reflect_term (t ↑' n # m) (m' + n) = ϕ.reflect_term t m' ↑' n # m

theorem Flypitch.fol.Lhom.reflect_term_lift {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {n m : ℕ} (t : term L') : ϕ.reflect_term (t ↑ n) (m + n) = ϕ.reflect_term t m ↑ n

noncomputable def Flypitch.fol.Lhom.reflect_formula {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (f : formula L') : ℕ → formula L

Equations

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

theorem Flypitch.fol.Lhom.reflect_formula_apps_rel_pos {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] {l : ℕ} {R : L'.relations l} (hR : R ∈ Set.range ϕ.on_relation) (ts : dvector (term L') l) (m : ℕ) : ϕ.reflect_formula (apps_rel (preformula.rel R) ts) m = apps_rel (preformula.rel (Classical.choose hR)) (dvector.map (fun (t : term L') => ϕ.reflect_term t m) ts)

theorem Flypitch.fol.Lhom.reflect_formula_apps_rel_neg {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] {l : ℕ} {R : L'.relations l} (hR : R ∉ Set.range ϕ.on_relation) (ts : dvector (term L') l) (m : ℕ) : ϕ.reflect_formula (apps_rel (preformula.rel R) ts) m = ⊥

@[simp]

theorem Flypitch.fol.Lhom.reflect_formula_equal {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (t₁ t₂ : term L') (m : ℕ) : ϕ.reflect_formula (t₁ ≃ t₂) m = ϕ.reflect_term t₁ m ≃ ϕ.reflect_term t₂ m

@[simp]

theorem Flypitch.fol.Lhom.reflect_formula_imp {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (f₁ f₂ : formula L') (m : ℕ) : ϕ.reflect_formula (f₁ ⟹ f₂) m = ϕ.reflect_formula f₁ m ⟹ ϕ.reflect_formula f₂ m

@[simp]

theorem Flypitch.fol.Lhom.reflect_formula_all {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (f : formula L') (m : ℕ) : ϕ.reflect_formula (∀' f) m = ∀' ϕ.reflect_formula f (m + 1)

@[simp]

theorem Flypitch.fol.Lhom.reflect_formula_on_formula {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) (m : ℕ) (f : formula L) : ϕ.reflect_formula (ϕ.on_formula f) m = lift_formula_at f 1 m

theorem Flypitch.fol.Lhom.reflect_formula_lift_at {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {n m m' : ℕ} (h : m ≤ m') (f : formula L') : ϕ.reflect_formula (lift_formula_at f n m) (m' + n) = lift_formula_at (ϕ.reflect_formula f m') n m

theorem Flypitch.fol.Lhom.reflect_formula_lift {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {n m : ℕ} (f : formula L') : ϕ.reflect_formula (lift_formula f n) (m + n) = lift_formula (ϕ.reflect_formula f m) n

@[simp]

theorem Flypitch.fol.Lhom.reflect_formula_lift1 {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) (f : formula L') (m : ℕ) : ϕ.reflect_formula (lift_formula1 f) (m + 1) = lift_formula1 (ϕ.reflect_formula f m)

theorem Flypitch.fol.Lhom.reflect_term_subst {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) (t s : term L') (n m : ℕ) : ϕ.reflect_term (t[s // n]) (m + n) = ϕ.reflect_term t (m + n + 1)[ϕ.reflect_term s m // n]

theorem Flypitch.fol.Lhom.reflect_formula_subst {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) (f : formula L') (t : term L') (n m : ℕ) : ϕ.reflect_formula (subst_formula f t n) (m + n) = subst_formula (ϕ.reflect_formula f (m + n + 1)) (ϕ.reflect_term t m) n

@[simp]

theorem Flypitch.fol.Lhom.reflect_formula_subst0 {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) (f : formula L') (t : term L') (m : ℕ) : ϕ.reflect_formula (subst_formula f t 0) m = subst_formula (ϕ.reflect_formula f (m + 1)) (ϕ.reflect_term t m) 0

noncomputable def Flypitch.fol.Lhom.reflect_prf_gen {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {Γ : Set (formula L')} {f : formula L'} (m : ℕ) (h : Γ ⊢ f) : (fun (g : formula L') => ϕ.reflect_formula g m) '' Γ ⊢ ϕ.reflect_formula f m

Equations

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

noncomputable def Flypitch.fol.Lhom.reflect_prf {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {Γ : Set (formula L)} {f : formula L} (h : ϕ.on_formula '' Γ ⊢ ϕ.on_formula f) : Γ ⊢ f

Equations

• ϕ.reflect_prf hϕ h = Flypitch.fol.reflect_prf_lift1 (cast ⋯ (ϕ.reflect_prf_gen hϕ 0 h))

noncomputable def Flypitch.fol.Lhom.reflect_sprf {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {T : Theory L} {f : sentence L} (h : ϕ.Theory_induced T ⊢ ϕ.on_sentence f) : T ⊢ f

Equations

• ϕ.reflect_sprf hϕ h = id (ϕ.reflect_prf hϕ (⋯.mp h))

theorem Flypitch.fol.Lhom.is_consistent_Theory_induced {L L' : Language} (ϕ : L →ᴸ L') [ϕ.has_decidable_range] (hϕ : ϕ.is_injective) {T : Theory L} (hT : is_consistent T) : is_consistent (ϕ.Theory_induced T)

def Flypitch.fol.Lhom.boundedFormulaSubstSentence {L : Language} (f : bounded_formula L 1) (t : closed_term L) : sentence L

A bounded formula instantiated at a closed term, repackaged as a sentence.

Equations

• Flypitch.fol.Lhom.boundedFormulaSubstSentence f t = ⟨Flypitch.fol.subst_formula (Flypitch.fol.bounded_preformula.fst f) (Flypitch.fol.bounded_preterm.fst t) 0, ⋯⟩

noncomputable def Flypitch.fol.Lhom.generalize_constant {L : Language} {Γ : Set (formula L)} (c : L.constants) (hΓ : Sum.inl ⟨0, c⟩ ∉ ⋃₀ (symbols_in_formula '' Γ)) {f : formula L} (hf : Sum.inl ⟨0, c⟩ ∉ symbols_in_formula f) (H : Γ ⊢ subst_formula f (preterm.func c) 0) : Γ ⊢ ∀' f

Generalize away a fresh constant appearing only as the witness in a derivation.

Equations

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

noncomputable def Flypitch.fol.Lhom.sgeneralize_constant {L : Language} {T : Theory L} (c : L.constants) (hΓ : Sum.inl ⟨0, c⟩ ∉ ⋃₀ (symbols_in_formula '' T.fst)) {f : bounded_formula L 1} (hf : Sum.inl ⟨0, c⟩ ∉ symbols_in_formula (bounded_preformula.fst f)) (H : T ⊢ boundedFormulaSubstSentence f (bd_const c)) : T ⊢ bd_all f

Sentence-level specialization of generalize_constant for bounded formulas.

Equations

• Flypitch.fol.Lhom.sgeneralize_constant c hΓ hf H = id (Flypitch.fol.Lhom.generalize_constant c hΓ hf (id H))