Foundation.FirstOrder.Bootstrapping.Syntax.Theory

source

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 (φ : SyntacticFormula L) : ℕ ⊧/![⌜φ⌝] ↑(ch T) ↔ ∃ σ ∈ T, φ = ↑σ
isDelta1 : Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn (ch T) 𝗜𝚺₁

Instances

source

@[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

Instances For

source

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 | V ⊧/![φ] ↑T.Δ₁ch}

Instances For

source

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

source

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

source

@[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

source

@[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.Δ₁] {φ : SyntacticFormula L} :

⌜φ⌝ ∈ T.Δ₁Class ↔ ∃ σ ∈ T, φ = ↑σ

source

@[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

source

@[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} :

V ⊧/![⌜φ⌝] ↑T.Δ₁ch ↔ φ ∈ T

source

@[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.Δ₁] {φ : SyntacticFormula L} :

V ⊧/![⌜φ⌝] ↑T.Δ₁ch ↔ ∃ σ ∈ T, φ = ↑σ

source

@[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

source

@[implicit_reducible]

instance 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 := ⋯ }

source

@[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 := ⋯ }

Instances For

source

@[implicit_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 }

source

@[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.

Instances For

source

@[simp]

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

↑{φ}.Δ₁ch = (“!!(Semiterm.bvar 0) = !!↑(Encodable.encode φ)”)

source

@[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 ⋯

Instances For

source

@[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 ⋯

Instances For

source

@[implicit_reducible]

instance LO.FirstOrder.Theory.Δ₁.instHAdd {L : Language} [L.Encodable] [L.LORDefinable] {T U : Theory L} [T.Δ₁] [U.Δ₁] :

(T + U).Δ₁

Equations

LO.FirstOrder.Theory.Δ₁.instHAdd = inferInstance.add inferInstance

source

@[implicit_reducible]

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

{φ}.Δ₁

Equations

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

source

@[implicit_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 ⋯