Supporting results for pointwise provable equality.

class PointwiseComposition.FFL.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

  The ch construction in FFL.FirstOrder.Theory.Δ₁.

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

@[reducible, inline]

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

The Δ₁ch construction in FFL.FirstOrder.Theory.

Equations

• T.Δ₁ch = PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.ch T

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

Data and laws for RE in FFL.FirstOrder.Theory.

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

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

Data and laws for Primrec in FFL.FirstOrder.Theory.

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

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

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

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

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

The Δ₁Class construction in FFL.FirstOrder.Theory.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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

theorem PointwiseComposition.FFL.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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.add {L : Language} [L.Encodable] [L.LORDefinable] {T U : Theory L} (dT : T.Δ₁) (dU : U.Δ₁) : (T ∪ U).Δ₁

The add construction in FFL.FirstOrder.Theory.Δ₁.

Equations

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

@[reducible, inline]

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

The of Eq construction in FFL.FirstOrder.Theory.Δ₁.

Equations

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

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

The singleton construction in FFL.FirstOrder.Theory.Δ₁.

Equations

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

@[simp]

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

@[reducible, inline]

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

The of List construction in FFL.FirstOrder.Theory.Δ₁.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.ofList [] = PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.empty.ofEq ⋯

@[reducible, inline]

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

The of Finite construction in FFL.FirstOrder.Theory.Δ₁.

Equations

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

@[instance_reducible]

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

Equations

• PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.instUnion = inferInstance.add inferInstance

@[instance_reducible]

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

Equations

• PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.instSingletonSentence φ = PointwiseComposition.FFL.FirstOrder.Theory.Δ₁.singleton φ

@[instance_reducible]

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

Equations

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