class LO.FirstOrder.Theory.Δ₁ {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) : Type

TODO: define predicate VariableFree and make mem_iff ∀ φ : Sentence, ℕ ⊧/![⌜φ⌝] ch.val ↔ φ ∈ T

• ch : 𝚫₁.Semisentence 1
• mem_iff (φ : Proposition L) : (Semiformula.Evalb ![⌜φ⌝]) ↑(ch T) ↔ ∃ σ ∈ T, φ = Rewriting.emb σ
• isDelta1 : Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn (ch T) 𝗜𝚺₁

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Δ₁ch {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚫₁.Semisentence 1

Equations

• T.Δ₁ch = LO.FirstOrder.Theory.Δ₁.ch T

class LO.FirstOrder.Theory.RE {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) : Prop

• re : REPred fun (x : Sentence L) => x ∈ T

class LO.FirstOrder.Theory.Primrec {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) : Prop

• primrec : PrimrecPred fun (x : Sentence L) => x ∈ T

instance LO.FirstOrder.Theory.instREOfPrimrec {L : Language} [L.Encodable] [L.Primcodable] {T : Theory L} [T.Primrec] : T.RE

theorem LO.FirstOrder.Theory.RE.add {L : Language} [L.Encodable] [L.Primcodable] {T U : Theory L} (hT : T.RE) (hU : U.RE) : (T ∪ U).RE

theorem LO.FirstOrder.Theory.RE.ofFinite {L : Language} [L.Encodable] [L.Primcodable] {T : Theory L} [L.DecidableEq] (hT : Set.Finite T) : T.RE

def LO.FirstOrder.Theory.Δ₁Class {V : Type u_1} [ORingStructure V] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Set V

Equations

• T.Δ₁Class = {φ : V | (LO.FirstOrder.Semiformula.Evalb ![φ]) ↑T.Δ₁ch}

instance LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Predicate fun (x : V) => x ∈ T.Δ₁Class via T.Δ₁ch

instance LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Predicate fun (x : V) => x ∈ T.Δ₁Class

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.proper {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : HierarchySymbol.Semiformula.ProperOn V T.Δ₁ch

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.mem_iff_s {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Proposition L} : ⌜φ⌝ ∈ T.Δ₁Class ↔ ∃ σ ∈ T, φ = Rewriting.emb σ

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.mem_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : ⌜φ⌝ ∈ T.Δ₁Class ↔ φ ∈ T

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.mem_iff' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : (Semiformula.Evalb ![⌜φ⌝]) ↑T.Δ₁ch ↔ φ ∈ T

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.mem_iff'_s {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Proposition L} : (Semiformula.Evalb ![⌜φ⌝]) ↑T.Δ₁ch ↔ ∃ σ ∈ T, φ = Rewriting.emb σ

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Δ₁Class.mem_iff'' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : ⌜φ⌝.val ∈ T.Δ₁Class ↔ φ ∈ T

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Δ₁.add {L : Language} [L.Encodable] [L.LORDefinable] {T U : Theory L} (dT : T.Δ₁) (dU : U.Δ₁) : (T ∪ U).Δ₁

Equations

• dT.add dU = { ch := T.Δ₁ch ⋎ U.Δ₁ch, mem_iff := ⋯, isDelta1 := ⋯ }

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Δ₁.ofEq {L : Language} [L.Encodable] [L.LORDefinable] {T U : Theory L} (dT : T.Δ₁) (h : T = U) : U.Δ₁

Equations

• dT.ofEq h = { ch := LO.FirstOrder.Theory.Δ₁.ch T, mem_iff := ⋯, isDelta1 := ⋯ }

@[instance_reducible]

instance LO.FirstOrder.Theory.Δ₁.empty {L : Language} [L.Encodable] [L.LORDefinable] : ∅.Δ₁

Equations

• LO.FirstOrder.Theory.Δ₁.empty = { ch := ⊥, mem_iff := ⋯, isDelta1 := LO.FirstOrder.Theory.Δ₁.empty._proof_3 }

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Δ₁.singleton {L : Language} [L.Encodable] [L.LORDefinable] (φ : Sentence L) : {φ}.Δ₁

Equations

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

@[simp]

theorem LO.FirstOrder.Theory.Δ₁.singleton_toTDef_ch_val {L : Language} [L.Encodable] [L.LORDefinable] (φ : Sentence L) : ↑{φ}.Δ₁ch = (“!!(Semiterm.bvar 0) = !!↑(Encodable.encode φ)”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Δ₁.ofList {L : Language} [L.Encodable] [L.LORDefinable] (l : List (Sentence L)) : Δ₁ {φ : Sentence L | φ ∈ l}

Equations

• LO.FirstOrder.Theory.Δ₁.ofList [] = LO.FirstOrder.Theory.Δ₁.empty.ofEq ⋯
• LO.FirstOrder.Theory.Δ₁.ofList (φ :: l_2) = ((LO.FirstOrder.Theory.Δ₁.singleton φ).add (LO.FirstOrder.Theory.Δ₁.ofList l_2)).ofEq ⋯

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Theory.Δ₁.ofFinite {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) (h : Set.Finite T) : T.Δ₁

Equations

• LO.FirstOrder.Theory.Δ₁.ofFinite T h = (LO.FirstOrder.Theory.Δ₁.ofList h.toFinset.toList).ofEq ⋯

@[instance_reducible]

instance LO.FirstOrder.Theory.Δ₁.instUnion {L : Language} [L.Encodable] [L.LORDefinable] {T U : Theory L} [T.Δ₁] [U.Δ₁] : (T ∪ U).Δ₁

Equations

• LO.FirstOrder.Theory.Δ₁.instUnion = inferInstance.add inferInstance

@[instance_reducible]

instance LO.FirstOrder.Theory.Δ₁.instSingletonSentence {L : Language} [L.Encodable] [L.LORDefinable] (φ : Sentence L) : {φ}.Δ₁

Equations

• LO.FirstOrder.Theory.Δ₁.instSingletonSentence φ = LO.FirstOrder.Theory.Δ₁.singleton φ

@[instance_reducible]

instance LO.FirstOrder.Theory.Δ₁.insert {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} {φ : Sentence L} [d : T.Δ₁] : (Insert.insert φ T).Δ₁

Equations

• LO.FirstOrder.Theory.Δ₁.insert = (d.add (LO.FirstOrder.Theory.Δ₁.singleton φ)).ofEq ⋯