noncomputable def FFL.FirstOrder.ProvabilityAbstraction.Provability.height {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) : ℕ∞

Equations

• 𝔅.height = ENat.find fun (x : ℕ) => T ⊢ (↑𝔅)^[x] ⊥

@[simp]

theorem FFL.FirstOrder.ProvabilityAbstraction.neg_iterated_prov {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} {n : ℕ} (φ : Sentence L) : ∼(↑𝔅)^[n] φ = 𝔅.dia^[n] (∼φ)

theorem FFL.FirstOrder.ProvabilityAbstraction.boxBot_monotone {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} {n m : ℕ} [T₀ ⪯ T] [𝔅.HBL] : n ≤ m → T ⊢ (↑𝔅)^[n] ⊥ 🡒 (↑𝔅)^[m] ⊥

theorem FFL.FirstOrder.ProvabilityAbstraction.iIncon_unprovable_of_sigma1_sound {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} [𝔅.Kreisel] [Entailment.Consistent T] (n : ℕ) : T ⊬ (↑𝔅)^[n] ⊥

theorem FFL.FirstOrder.ProvabilityAbstraction.Provability.height_eq_top_iff {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} : 𝔅.height = ⊤ ↔ ∀ (n : ℕ), T ⊬ (↑𝔅)^[n] ⊥

theorem FFL.FirstOrder.ProvabilityAbstraction.Provability.height_le_of_boxBot {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} {n : ℕ} (h : T ⊢ (↑𝔅)^[n] ⊥) : 𝔅.height ≤ ↑n

theorem FFL.FirstOrder.ProvabilityAbstraction.Provability.height_lt_pos_of_boxBot {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} (hSound : ∀ {σ : Sentence L}, T₀ ⊢ ↑𝔅 σ → T ⊢ σ) {n : ℕ} (pos : 0 < n) (h : T₀ ⊢ (↑𝔅)^[n] ⊥) : 𝔅.height < ↑n

theorem FFL.FirstOrder.ProvabilityAbstraction.Provability.height_le_iff_boxBot {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} [T₀ ⪯ T] [𝔅.HBL] {n : ℕ} : 𝔅.height ≤ ↑n ↔ T ⊢ (↑𝔅)^[n] ⊥

theorem FFL.FirstOrder.ProvabilityAbstraction.Provability.height_eq_top_of_sound_and_consistent {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} [𝔅.Kreisel] [Entailment.Consistent T] : 𝔅.height = ⊤

theorem FFL.FirstOrder.ProvabilityAbstraction.Provability.height_eq_zero_of_inconsistent {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} (h : Entailment.Inconsistent T) : 𝔅.height = 0

@[reducible, inline]

noncomputable abbrev FFL.FirstOrder.ArithmeticTheory.height (T : ArithmeticTheory) [Theory.Δ₁ T] : ℕ∞

Equations

• T.height = (FFL.FirstOrder.Theory.standardProvability T).height

theorem FFL.FirstOrder.Arithmetic.height_eq_top_of_sigma1_sound (T : ArithmeticTheory) [Theory.Δ₁ T] [T.SoundOnHierarchy 𝚺 1] : T.height = ⊤

@[simp]

theorem FFL.FirstOrder.Arithmetic.ISigma1_height_eq_top : 𝗜𝚺₁.height = ⊤

@[simp]

theorem FFL.FirstOrder.Arithmetic.Peano_height_eq_top : 𝗣𝗔.height = ⊤