Derivability conditions of standard provability predicate

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

Equations

• LO.FirstOrder.Arithmetic.instDiagonalizationISigmaOfNatNat = { fixedpoint := LO.FirstOrder.Arithmetic.fixedpoint, diag := LO.FirstOrder.Arithmetic.instDiagonalizationISigmaOfNatNat._proof_1 }

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

The derivability condition D1.

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

The derivability condition D2.

@[reducible, inline]

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

Equations

• T.standardProvability = { prov := ↑T.provable, prov_def := ⋯ }

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

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

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

theorem LO.FirstOrder.Arithmetic.provable_sigma_one_complete {T : Theory ℒₒᵣ} [T.Δ₁] [𝗣𝗔⁻ ⪯ T] {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) : 𝗜𝚺₁ ⊢ σ ➝ T.provabilityPred σ

theorem LO.FirstOrder.Arithmetic.provable_D3 {T : Theory ℒₒᵣ} [T.Δ₁] [𝗣𝗔⁻ ⪯ T] {σ : Sentence ℒₒᵣ} : 𝗜𝚺₁ ⊢ T.provabilityPred σ ➝ T.provabilityPred (T.provabilityPred σ)

The derivability condition D3.

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

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

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

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

instance LO.FirstOrder.Arithmetic.instHBL3ISigmaOfNatNatStandardProvabilityOfWeakerThanSentenceORingArithmeticTheoryTheoryPeanoMinus {T : Theory ℒₒᵣ} [T.Δ₁] [𝗣𝗔⁻ ⪯ T] : T.standardProvability.HBL3

instance LO.FirstOrder.Arithmetic.instHBLISigmaOfNatNatStandardProvabilityOfWeakerThanSentenceORingArithmeticTheoryTheoryPeanoMinus {T : Theory ℒₒᵣ} [T.Δ₁] [𝗣𝗔⁻ ⪯ T] : T.standardProvability.HBL

instance LO.FirstOrder.Arithmetic.instKreiselISigmaOfNatNatStandardProvabilityOfSoundOnHierarchySigmaPolarity {T : Theory ℒₒᵣ} [T.Δ₁] {σ : Sentence ℒₒᵣ} [ArithmeticTheory.SoundOnHierarchy T 𝚺 1] : T.standardProvability.Kreisel σ

theorem LO.FirstOrder.Arithmetic.provable_sigma_one_complete_of_E {T : Theory ℒₒᵣ} [T.Δ₁] {σ π : Semiformula ℒₒᵣ Empty 0} [𝗜𝚺₁ ⪯ T] (hσ : Hierarchy 𝚺 1 σ) (hσπ : T ⊢ σ ⭤ π) : T ⊢ π ➝ T.provabilityPred π

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