Derivability conditions of standard provability predicate

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Arithmetic.instDiagonalizationISigmaOfNatNat : ProvabilityAbstraction.Diagonalization 𝗜𝚺₁

Equations

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

theorem FFL.FirstOrder.Arithmetic.provable_D1 {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {σ : Sentence L} : T ⊢ σ → 𝗜𝚺₁ ⊢ Bootstrapping.provabilityPred T σ

The derivability condition D1.

theorem FFL.FirstOrder.Arithmetic.provable_D2 {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {σ π : Sentence L} : 𝗜𝚺₁ ⊢ Bootstrapping.provabilityPred T (σ 🡒 π) 🡒 Bootstrapping.provabilityPred T σ 🡒 Bootstrapping.provabilityPred T π

The derivability condition D2.

@[reducible, inline]

noncomputable abbrev FFL.FirstOrder.Theory.standardProvability {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : ProvabilityAbstraction.Provability 𝗜𝚺₁ T

Equations

• T.standardProvability = { prov := ↑(FFL.FirstOrder.Arithmetic.Bootstrapping.provable T), bew_def := ⋯ }

instance FFL.FirstOrder.Arithmetic.instHBL2ISigmaOfNatNatStandardProvability {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : T.standardProvability.HBL2

theorem FFL.FirstOrder.Arithmetic.standardProvability_def {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (σ : Sentence L) : ↑T.standardProvability σ = Bootstrapping.provabilityPred T σ

instance FFL.FirstOrder.Arithmetic.instSoundOnISigmaOfNatNatStandardProvability {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : T.standardProvability.SoundOn ℕ

theorem FFL.FirstOrder.Arithmetic.provable_sigma_one_complete {T : ArithmeticTheory} [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] {σ : ArithmeticSentence} (hσ : ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1 σ) : 𝗜𝚺₁ ⊢ σ 🡒 Bootstrapping.provabilityPred T σ

theorem FFL.FirstOrder.Arithmetic.provable_D3 {T : ArithmeticTheory} [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] {σ : ArithmeticSentence} : 𝗜𝚺₁ ⊢ Bootstrapping.provabilityPred T σ 🡒 Bootstrapping.provabilityPred T (Bootstrapping.provabilityPred T σ)

The derivability condition D3.

theorem FFL.FirstOrder.Arithmetic.provable_D2_context {T U : ArithmeticTheory} [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ U] {Γ : List ArithmeticSentence} {σ π : Sentence ℒₒᵣ} (hσπ : Γ ⊢[U] Bootstrapping.provabilityPred T (σ 🡒 π)) (hσ : Γ ⊢[U] Bootstrapping.provabilityPred T σ) : Γ ⊢[U] Bootstrapping.provabilityPred T π

theorem FFL.FirstOrder.Arithmetic.provable_D3_context {T U : ArithmeticTheory} [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] [𝗜𝚺₁ ⪯ U] {Γ : List ArithmeticSentence} {σ : Sentence ℒₒᵣ} (hσπ : Γ ⊢[U] Bootstrapping.provabilityPred T σ) : Γ ⊢[U] Bootstrapping.provabilityPred T (Bootstrapping.provabilityPred T σ)

theorem FFL.FirstOrder.Arithmetic.provable_sound {T U : ArithmeticTheory} [Theory.Δ₁ T] [U.SoundOnHierarchy 𝚺 1] {σ : Sentence ℒₒᵣ} : U ⊢ Bootstrapping.provabilityPred T σ → T ⊢ σ

theorem FFL.FirstOrder.Arithmetic.provable_complete {T U : ArithmeticTheory} [Theory.Δ₁ T] [U.SoundOnHierarchy 𝚺 1] [𝗜𝚺₁ ⪯ U] {σ : Sentence ℒₒᵣ} : T ⊢ σ ↔ U ⊢ Bootstrapping.provabilityPred T σ

instance FFL.FirstOrder.Arithmetic.instHBL3ISigmaOfNatNatStandardProvabilityOfWeakerThanSentenceORingArithmeticTheoryPeanoMinus {T : ArithmeticTheory} [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] : (Theory.standardProvability T).HBL3

instance FFL.FirstOrder.Arithmetic.instHBLISigmaOfNatNatStandardProvabilityOfWeakerThanSentenceORingArithmeticTheoryPeanoMinus {T : ArithmeticTheory} [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] : (Theory.standardProvability T).HBL

instance FFL.FirstOrder.Arithmetic.instKreiselISigmaOfNatNatStandardProvabilityOfSoundOnHierarchySigmaPolarity {T : ArithmeticTheory} [Theory.Δ₁ T] [T.SoundOnHierarchy 𝚺 1] : (Theory.standardProvability T).Kreisel

theorem FFL.FirstOrder.Arithmetic.models_standardProvability_iff {T : ArithmeticTheory} [Theory.Δ₁ T] {σ : Sentence ℒₒᵣ} : ℕ↓[ℒₒᵣ] ⊧ ↑(Theory.standardProvability T) σ ↔ T ⊢ σ

theorem FFL.FirstOrder.Arithmetic.soundOnHierarchy_iff_models_reflection {T : ArithmeticTheory} [Theory.Δ₁ T] : T.SoundOnHierarchy 𝚺 1 ↔ ∀ (σ : Semiformula ℒₒᵣ Empty 0), ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1 σ → ℕ↓[ℒₒᵣ] ⊧ ↑(Theory.standardProvability T) σ 🡒 σ

theorem FFL.FirstOrder.Arithmetic.provable_sigma_one_complete_of_E {T : ArithmeticTheory} [Theory.Δ₁ T] {σ π : Semiformula ℒₒᵣ Empty 0} [𝗜𝚺₁ ⪯ T] (hσ : ℬ[<, ℒₒᵣ].Hierarchy 𝚺 1 σ) (hσπ : 𝗜𝚺₁ ⊢ σ 🡘 π) : 𝗜𝚺₁ ⊢ π 🡒 Bootstrapping.provabilityPred T π

If π is equivalent to some 𝚺ᴬ₁ sentence σ, then π 🡒 □π is provable in T (note: not 𝗜𝚺₁, compare provable_sigma_one_complete)

theorem FFL.FirstOrder.Arithmetic.provable_standardProvability_imp_of_Δ₁Class_subset {T U : ArithmeticTheory} [Theory.Δ₁ T] [Theory.Δ₁ U] (h : ∀ (V : Type) [inst : ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁], ∀ p ∈ Theory.Δ₁Class T, p ∈ Theory.Δ₁Class U) (σ : ArithmeticSentence) : 𝗜𝚺₁ ⊢ ↑(Theory.standardProvability T) σ 🡒 ↑(Theory.standardProvability U) σ

theorem FFL.FirstOrder.Arithmetic.InductionOnPrenexHierarchy.provable_standardProvability_imp_Peano {Γ : Polarity} (m : ℕ) (σ : ArithmeticSentence) : 𝗜𝚺₁ ⊢ ↑(Theory.standardProvability (𝗜𝗡𝗗 Γ m)) σ 🡒 ↑(Theory.standardProvability 𝗣𝗔) σ

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.provable_standardProvability_imp_of_le {Γ : Polarity} {m n : ℕ} (h : m ≤ n) (σ : ArithmeticSentence) : 𝗜𝚺₁ ⊢ ↑(Theory.standardProvability (𝗜𝗡𝗗⁺ Γ m)) σ 🡒 ↑(Theory.standardProvability (𝗜𝗡𝗗⁺ Γ n)) σ

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.provable_standardProvability_imp_Peano {Γ : Polarity} (m : ℕ) (σ : ArithmeticSentence) : 𝗜𝚺₁ ⊢ ↑(Theory.standardProvability (𝗜𝗡𝗗⁺ Γ m)) σ 🡒 ↑(Theory.standardProvability 𝗣𝗔) σ

theorem FFL.FirstOrder.Arithmetic.exists_true_but_unprovable_sentence_of_incomplete {T : ArithmeticTheory} (h : Entailment.Incomplete T) : ∃ (δ : ArithmeticSentence), ℕ↓[ℒₒᵣ] ⊧ δ ∧ T ⊬ δ