class SecondOrder.Language.HasStructure (L : Language) (M : Type u) : Type u

• interpFunc {n : ℕ} : L.Func n → Vec M n → M
• interpRel {n : ℕ} : L.Rel n → Vec M n → Prop

def SecondOrder.Language.interpTy (M : Type u) : Ty → Type u

Equations

• SecondOrder.Language.interpTy M SecondOrder.Ty.var = M
• SecondOrder.Language.interpTy M (SecondOrder.Ty.func n) = (Vec M n → M)
• SecondOrder.Language.interpTy M (SecondOrder.Ty.rel n) = (Vec M n → Prop)

def SecondOrder.Language.Assignment (M : Type u) (l : List Ty) : Type u

Equations

• SecondOrder.Language.Assignment M l = (⦃T : SecondOrder.Ty⦄ → l.Fin T → SecondOrder.Language.interpTy M T)

def SecondOrder.Language.Assignment.nil {M : Type u_1} : Assignment M []

def SecondOrder.Language.Assignment.«term[]ₐ» : Lean.ParserDescr

Equations

• SecondOrder.Language.Assignment.«term[]ₐ» = Lean.ParserDescr.node `SecondOrder.Language.Assignment.«term[]ₐ» 1024 (Lean.ParserDescr.symbol "[]ₐ")

def SecondOrder.Language.Assignment.cons {M : Type u_1} {T : Ty} {l : List Ty} (u : interpTy M T) (ρ : Assignment M l) : Assignment M (T :: l)

Equations

• (u ∷ₐ ρ) List.Fin.fz = u
• (u ∷ₐ ρ) x_3.fs = ρ x_3

def SecondOrder.Language.Assignment.«term_∷ₐ_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem SecondOrder.Language.Assignment.cons_zero {M✝ : Type u_1} {a✝ : Ty} {u : interpTy M✝ a✝} {l✝ : List Ty} {ρ : Assignment M✝ l✝} : (u ∷ₐ ρ) 0 = u

@[simp]

theorem SecondOrder.Language.Assignment.cons_one {M : Type u_1} {T : Ty} {l : List Ty} {a✝ : Ty} {u : interpTy M a✝} {ρ : Assignment M (T :: l)} : (u ∷ₐ ρ) 1 = ρ 0

@[simp]

theorem SecondOrder.Language.Assignment.cons_two {M : Type u_1} {T₁ T₂ : Ty} {l : List Ty} {a✝ : Ty} {u : interpTy M a✝} {ρ : Assignment M (T₁ :: T₂ :: l)} : (u ∷ₐ ρ) 2 = ρ 1

@[simp]

theorem SecondOrder.Language.Assignment.cons_three {M : Type u_1} {T₁ T₂ T₃ : Ty} {l : List Ty} {a✝ : Ty} {u : interpTy M a✝} {ρ : Assignment M (T₁ :: T₂ :: T₃ :: l)} : (u ∷ₐ ρ) 3 = ρ 2

@[simp]

theorem SecondOrder.Language.Assignment.cons_four {M : Type u_1} {T₁ T₂ T₃ T₄ : Ty} {l : List Ty} {a✝ : Ty} {u : interpTy M a✝} {ρ : Assignment M (T₁ :: T₂ :: T₃ :: T₄ :: l)} : (u ∷ₐ ρ) 4 = ρ 3

def SecondOrder.Language.interp {L : Language} {l : List Ty} (M : Type u) [L.HasStructure M] (ρ : Assignment M l) : L.Term l → M

Equations

• ⟦ #x_1 ⟧ₜ M, ρ = ρ x_1
• ⟦ f ⬝ᶠ v ⟧ₜ M, ρ = SecondOrder.Language.HasStructure.interpFunc f fun (i : Fin n) => ⟦ v i ⟧ₜ M, ρ
• ⟦ f ⬝ᶠᵛ v ⟧ₜ M, ρ = ρ f fun (i : Fin n) => ⟦ v i ⟧ₜ M, ρ

def SecondOrder.Language.«term⟦_⟧ₜ_,_» : Lean.ParserDescr

Equations

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

@[simp]

theorem SecondOrder.Language.interp_var {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {x : l.Fin Ty.var} : ⟦ #x ⟧ₜ M, ρ = ρ x

@[simp]

theorem SecondOrder.Language.interp_fconst {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {a✝ : ℕ} {f : L.Func a✝} {v : Fin a✝ → L.Term l} : ⟦ f ⬝ᶠ v ⟧ₜ M, ρ = HasStructure.interpFunc f fun (i : Fin a✝) => ⟦ v i ⟧ₜ M, ρ

@[simp]

theorem SecondOrder.Language.interp_fvar {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {a✝ : ℕ} {f : l.Fin (Ty.func a✝)} {v : Fin a✝ → L.Term l} : ⟦ f ⬝ᶠᵛ v ⟧ₜ M, ρ = ρ f fun (i : Fin a✝) => ⟦ v i ⟧ₜ M, ρ

def SecondOrder.Language.satisfy {L : Language} (M : Type u) [L.HasStructure M] {l : List Ty} : L.Formula l → Assignment M l → Prop

Equations

• (M ⊨[x✝] r ⬝ʳ v) = SecondOrder.Language.HasStructure.interpRel r fun (i : Fin n) => ⟦ v i ⟧ₜ M, x✝
• (M ⊨[x✝] r ⬝ʳᵛ v) = x✝ r fun (i : Fin n) => ⟦ v i ⟧ₜ M, x✝
• (M ⊨[x✝] t₁ ≐ t₂) = (⟦ t₁ ⟧ₜ M, x✝ = ⟦ t₂ ⟧ₜ M, x✝)
• (M ⊨[x✝] SecondOrder.Language.Formula.false) = False
• (M ⊨[x✝] p.imp q) = (M ⊨[x✝] p → M ⊨[x✝] q)
• (M ⊨[x✝] ∀' p) = ∀ (u : M), M ⊨[u ∷ₐ x✝] p
• (M ⊨[x✝] ∀ᶠ[n]p) = ∀ (f : Vec M n → M), M ⊨[f ∷ₐ x✝] p
• (M ⊨[x✝] ∀ʳ[n]p) = ∀ (r : Vec M n → Prop), M ⊨[r ∷ₐ x✝] p

def SecondOrder.Language.«term_⊨[_]_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem SecondOrder.Language.satisfy_rconst {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {a✝ : ℕ} {r : L.Rel a✝} {v : Fin a✝ → L.Term l} : M ⊨[ρ] r ⬝ʳ v ↔ HasStructure.interpRel r fun (i : Fin a✝) => ⟦ v i ⟧ₜ M, ρ

@[simp]

theorem SecondOrder.Language.satisfy_rvar {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {a✝ : ℕ} {r : l.Fin (Ty.rel a✝)} {v : Fin a✝ → L.Term l} : M ⊨[ρ] r ⬝ʳᵛ v ↔ ρ r fun (i : Fin a✝) => ⟦ v i ⟧ₜ M, ρ

@[simp]

theorem SecondOrder.Language.satisfy_eq {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {t₁ t₂ : L.Term l} : M ⊨[ρ] t₁ ≐ t₂ ↔ ⟦ t₁ ⟧ₜ M, ρ = ⟦ t₂ ⟧ₜ M, ρ

@[simp]

theorem SecondOrder.Language.satisfy_false {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} : ¬M ⊨[ρ] ⊥

@[simp]

theorem SecondOrder.Language.satisfy_imp {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {p q : L.Formula l} : M ⊨[ρ] p ⇒ q ↔ M ⊨[ρ] p → M ⊨[ρ] q

@[simp]

theorem SecondOrder.Language.satisfy_true {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} : M ⊨[ρ] ⊤

@[simp]

theorem SecondOrder.Language.satisfy_neg {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {p : L.Formula l} : M ⊨[ρ] ~ p ↔ ¬M ⊨[ρ] p

@[simp]

theorem SecondOrder.Language.satisfy_and {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {p q : L.Formula l} : M ⊨[ρ] p ⩑ q ↔ M ⊨[ρ] p ∧ M ⊨[ρ] q

@[simp]

theorem SecondOrder.Language.satisfy_or {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {p q : L.Formula l} : M ⊨[ρ] p ⩒ q ↔ M ⊨[ρ] p ∨ M ⊨[ρ] q

@[simp]

theorem SecondOrder.Language.satisfy_iff {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {p q : L.Formula l} : M ⊨[ρ] p ⇔ q ↔ (M ⊨[ρ] p ↔ M ⊨[ρ] q)

@[simp]

theorem SecondOrder.Language.satisfy_all {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {p : L.Formula (Ty.var :: l)} : M ⊨[ρ] ∀' p ↔ ∀ (u : M), M ⊨[u ∷ₐ ρ] p

@[simp]

theorem SecondOrder.Language.satisfy_allf {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {n : ℕ} {p : L.Formula (Ty.func n :: l)} : M ⊨[ρ] ∀ᶠ[n]p ↔ ∀ (f : Vec M n → M), M ⊨[f ∷ₐ ρ] p

@[simp]

theorem SecondOrder.Language.satisfy_allr {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {n : ℕ} {p : L.Formula (Ty.rel n :: l)} : M ⊨[ρ] ∀ʳ[n]p ↔ ∀ (r : Vec M n → Prop), M ⊨[r ∷ₐ ρ] p

@[simp]

theorem SecondOrder.Language.satisfy_ex {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {p : L.Formula (Ty.var :: l)} : M ⊨[ρ] ∃' p ↔ ∃ (u : M), M ⊨[u ∷ₐ ρ] p

@[simp]

theorem SecondOrder.Language.satisfy_exf {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {n : ℕ} {p : L.Formula (Ty.func n :: l)} : M ⊨[ρ] ∃ᶠ[n]p ↔ ∃ (f : Vec M n → M), M ⊨[f ∷ₐ ρ] p

@[simp]

theorem SecondOrder.Language.satisfy_exr {L : Language} {M : Type u} [L.HasStructure M] {l : List Ty} {ρ : Assignment M l} {n : ℕ} {p : L.Formula (Ty.rel n :: l)} : M ⊨[ρ] ∃ʳ[n]p ↔ ∃ (r : Vec M n → Prop), M ⊨[r ∷ₐ ρ] p

@[reducible, inline]

abbrev SecondOrder.Language.satisfys {L : Language} (M : Type u) [L.HasStructure M] (p : L.Sentence) : Prop

Equations

• (M ⊨ₛ p) = (M ⊨[[]ₐ] p)

def SecondOrder.Language.«term_⊨ₛ_» : Lean.TrailingParserDescr

Equations

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

structure SecondOrder.Language.Structure (L : Language) : Type (u + 1)

• Dom : Type u
• interpFunc {n : ℕ} : L.Func n → Vec self.Dom n → self.Dom
• interpRel {n : ℕ} : L.Rel n → Vec self.Dom n → Prop

instance SecondOrder.Language.Structure.instCoeSortType {L : Language} : CoeSort L.Structure (Type u)

Equations

• SecondOrder.Language.Structure.instCoeSortType = { coe := fun (x : L.Structure) => x.Dom }

instance SecondOrder.Language.Structure.instHasStructureDom {L : Language} {M : L.Structure} : L.HasStructure M.Dom

Equations

• SecondOrder.Language.Structure.instHasStructureDom = { interpFunc := fun {n : ℕ} => M.interpFunc, interpRel := fun {n : ℕ} => M.interpRel }

@[reducible]

def SecondOrder.Language.Structure.of {L : Language} (M : Type u) [L.HasStructure M] : L.Structure

Equations

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

structure SecondOrder.Language.Structure.Embedding {L : Language} (M : L.Structure) (N : L.Structure) extends M.Dom ↪ N.Dom : Type (max u_1 u_2)

• toFun : M.Dom → N.Dom
• inj' : Injective self.toFun
• on_func {n : ℕ} (f : L.Func n) (v : Vec M.Dom n) : self.toEmbedding (HasStructure.interpFunc f v) = HasStructure.interpFunc f (⇑self.toEmbedding ∘ v)
• on_rel {n : ℕ} (r : L.Rel n) (v : Vec M.Dom n) : HasStructure.interpRel r v ↔ HasStructure.interpRel r (⇑self.toEmbedding ∘ v)

def SecondOrder.Language.Structure.«term_↪ᴹ_» : Lean.TrailingParserDescr

Equations

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

instance SecondOrder.Language.Structure.Embedding.instCoeFunForallDom {L : Language} {M : L.Structure} {N : L.Structure} : CoeFun (M ↪ᴹ N) fun (x : M ↪ᴹ N) => M.Dom → N.Dom

Equations

• SecondOrder.Language.Structure.Embedding.instCoeFunForallDom = { coe := fun (x : M ↪ᴹ N) => ⇑x.toEmbedding }

def SecondOrder.Language.Structure.Embedding.refl {L : Language} {M : L.Structure} : M ↪ᴹ M

Equations

• SecondOrder.Language.Structure.Embedding.refl = { toEmbedding := Function.Embedding.refl M.Dom, on_func := ⋯, on_rel := ⋯ }

def SecondOrder.Language.Structure.Embedding.trans {L : Language} {M : L.Structure} {N : L.Structure} {𝓢 : L.Structure} (e₁ : M ↪ᴹ N) (e₂ : N ↪ᴹ 𝓢) : M ↪ᴹ 𝓢

Equations

• e₁.trans e₂ = { toEmbedding := e₁.trans e₂.toEmbedding, on_func := ⋯, on_rel := ⋯ }

structure SecondOrder.Language.Structure.Isomorphism {L : Language} (M : L.Structure) (N : L.Structure) extends M.Dom ≃ N.Dom : Type (max u_1 u_2)

• toFun : M.Dom → N.Dom
• invFun : N.Dom → M.Dom
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• on_func {n : ℕ} (f : L.Func n) (v : Vec M.Dom n) : self.toEquiv (HasStructure.interpFunc f v) = HasStructure.interpFunc f (⇑self.toEquiv ∘ v)
• on_rel {n : ℕ} (r : L.Rel n) (v : Vec M.Dom n) : HasStructure.interpRel r v ↔ HasStructure.interpRel r (⇑self.toEquiv ∘ v)

def SecondOrder.Language.Structure.«term_≃ᴹ_» : Lean.TrailingParserDescr

Equations

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

instance SecondOrder.Language.Structure.Isomorphism.instCoeFunForallDom {L : Language} {M : L.Structure} {N : L.Structure} : CoeFun (M ≃ᴹ N) fun (x : M ≃ᴹ N) => M.Dom → N.Dom

Equations

• SecondOrder.Language.Structure.Isomorphism.instCoeFunForallDom = { coe := fun (x : M ≃ᴹ N) => ⇑x.toEquiv }

def SecondOrder.Language.Structure.Isomorphism.refl {L : Language} {M : L.Structure} : M ≃ᴹ M

Equations

• SecondOrder.Language.Structure.Isomorphism.refl = { toEquiv := Equiv.refl M.Dom, on_func := ⋯, on_rel := ⋯ }

def SecondOrder.Language.Structure.Isomorphism.symm {L : Language} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) : N ≃ᴹ M

Equations

• i.symm = { toEquiv := i.symm, on_func := ⋯, on_rel := ⋯ }

def SecondOrder.Language.Structure.Isomorphism.trans {L : Language} {M : L.Structure} {N : L.Structure} {𝓢 : L.Structure} (i₁ : M ≃ᴹ N) (i₂ : N ≃ᴹ 𝓢) : M ≃ᴹ 𝓢

Equations

• i₁.trans i₂ = { toEquiv := i₁.trans i₂.toEquiv, on_func := ⋯, on_rel := ⋯ }

def SecondOrder.Language.Structure.Isomorphism.toEmbedding {L : Language} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) : M ↪ᴹ N

Equations

• i.toEmbedding = { toEmbedding := i.toEmbedding, on_func := ⋯, on_rel := ⋯ }

def SecondOrder.Language.Structure.Isomorphism.onTy {L : Language} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) {T : Ty} : interpTy M.Dom T → interpTy N.Dom T

Equations

• i.onTy x_2 = i.toEquiv x_2
• i.onTy f = fun (v : Vec N.Dom a) => i.toEquiv (f (⇑i.symm.toEquiv ∘ v))
• i.onTy r = fun (v : Vec N.Dom a) => r (⇑i.symm.toEquiv ∘ v)

def SecondOrder.Language.Structure.Isomorphism.onAssignment {L : Language} {l : List Ty} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) : Assignment M.Dom l → Assignment N.Dom l

Equations

• i.onAssignment ρ x = i.onTy (ρ x)

theorem SecondOrder.Language.Structure.Isomorphism.on_term {L : Language} {l : List Ty} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) (t : L.Term l) (ρ : Assignment M.Dom l) : i.toEquiv (⟦ t ⟧ₜ M.Dom, ρ) = ⟦ t ⟧ₜ N.Dom, i.onAssignment ρ

theorem SecondOrder.Language.Structure.Isomorphism.on_formula {L : Language} {l : List Ty} {M : L.Structure} {N : L.Structure} (i : M ≃ᴹ N) (p : L.Formula l) (ρ : Assignment M.Dom l) : M.Dom ⊨[ρ] p ↔ N.Dom ⊨[i.onAssignment ρ] p

class SecondOrder.Language.Theory.IsModel {L : Language} (T : L.Theory) (M : Type u) [L.HasStructure M] : Prop

• satisfy_theory (p : L.Sentence) : p ∈ T → M ⊨ₛ p

structure SecondOrder.Language.Theory.Model {L : Language} (T : L.Theory) extends L.Structure : Type (u_1 + 1)

• Dom : Type u_1
• interpFunc {n : ℕ} : L.Func n → Vec self.Dom n → self.Dom
• interpRel {n : ℕ} : L.Rel n → Vec self.Dom n → Prop
• satisfy_theory (p : L.Sentence) : p ∈ T → self.Dom ⊨ₛ p

instance SecondOrder.Language.Theory.Model.instCoeOutStructure {L : Language} {T : L.Theory} : CoeOut T.Model L.Structure

Equations

• SecondOrder.Language.Theory.Model.instCoeOutStructure = { coe := fun (x : T.Model) => x.toStructure }

instance SecondOrder.Language.Theory.Model.instCoeSortType {L : Language} {T : L.Theory} : CoeSort T.Model (Type u)

Equations

• SecondOrder.Language.Theory.Model.instCoeSortType = { coe := fun (x : T.Model) => x.Dom }

instance SecondOrder.Language.Theory.Model.instIsModelDom {L : Language} {T : L.Theory} {M : T.Model} : T.IsModel M.Dom

@[reducible]

def SecondOrder.Language.Theory.Model.of {L : Language} {T : L.Theory} (M : Type u) [L.HasStructure M] [T.IsModel M] : T.Model

Equations

• SecondOrder.Language.Theory.Model.of M = { toStructure := SecondOrder.Language.Structure.of M, satisfy_theory := ⋯ }

def SecondOrder.Language.Theory.Categorical {L : Language} (T : L.Theory) : Prop

Equations

• T.Categorical = ∀ (M : T.Model) (N : T.Model), Nonempty (M.toStructure ≃ᴹ N.toStructure)