Consistency predicate

def LO.FirstOrder.Theory.Consistent (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Prop

Equations

• LO.FirstOrder.Theory.Consistent V T = ¬T.Provable ⌜⊥⌝

def LO.FirstOrder.Theory.ConsistentWith {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (φ : V) : Prop

Equations

• T.ConsistentWith φ = ¬T.Provable (LO.FirstOrder.Arithmetic.Bootstrapping.neg L φ)

theorem LO.FirstOrder.Theory.ConsistentWith.quote_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] {σ : Sentence L} : T.ConsistentWith ⌜σ⌝ ↔ ¬T.Provable ⌜∼σ⌝

noncomputable def LO.FirstOrder.Theory.consistent {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚷₁.Sentence

Equations

• T.consistent = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (∼T.provabilityPred ⊥) ⋯

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.consistent.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : V ⊧/![] ↑T.consistent ↔ Theory.Consistent V T

noncomputable def LO.FirstOrder.Theory.consistentWith {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚷₁.Semisentence 1

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.consistentWith.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚷₁-Predicate T.ConsistentWith via T.consistentWith

instance LO.FirstOrder.Arithmetic.Bootstrapping.consistentWith.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚷₁-Predicate T.ConsistentWith

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Theory.consistentWithPred {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : Sentence ℒₒᵣ

Equations

• T.consistentWithPred σ = ↑T.consistentWith/[⌜σ⌝]

noncomputable def LO.FirstOrder.Theory.consistentWithPred' {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : 𝚷₁.Sentence

Equations

• T.consistentWithPred' σ = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (↑T.consistentWith/[⌜σ⌝]) ⋯

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.consistentWithPred'_val {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : ↑(T.consistentWithPred' σ) = ↑(T.consistentWithPred' σ)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Con {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : ArithmeticTheory

Equations

• T.Con = {↑T.consistent}

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Incon {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : ArithmeticTheory

Equations

• T.Incon = {∼↑T.consistent}

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Con {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Theory.Δ₁ T.Con

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Con T = LO.FirstOrder.Theory.Δ₁.singleton ↑T.consistent

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Incon {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Theory.Δ₁ T.Incon

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Incon T = LO.FirstOrder.Theory.Δ₁.singleton (∼↑T.consistent)

def LO.FirstOrder.Arithmetic.Bootstrapping.consistent_eq (T : ArithmeticTheory) [Theory.Δ₁ T] : ↑(Theory.consistent T) = (Theory.standardProvability T).con

Equations

• ⋯ = ⋯

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.standard_consistent (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗥₀ ⪯ T] : Theory.Consistent ℕ T ↔ Entailment.Consistent T

instance LO.FirstOrder.Arithmetic.instModelsTheoryNatHAddArithmeticTheoryCon (T : ArithmeticTheory) [𝗜𝚺₁ ⪯ T] [Theory.Δ₁ T] [ℕ ⊧ₘ* T] : ℕ ⊧ₘ* T + Theory.Con T