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.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.exists_true_but_unprovable_sentence_of_incomplete {T : ArithmeticTheory} (h : Entailment.Incomplete T) : ∃ (δ : ArithmeticSentence), ℕ↓[ℒₒᵣ] ⊧ δ ∧ T ⊬ δ