Supporting results for pointwise provable equality.

Derivability conditions of standard provability predicate

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instDiagonalizationISigmaOfNatNat : ProvabilityAbstraction.Diagonalization 𝐈Σ₁

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Theory.standardProvability {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : ProvabilityAbstraction.Provability 𝐈Σ₁ T

The standard Provability construction in FFL.FirstOrder.Theory.

Equations

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

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

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.provable_sigma_one_complete {T : ArithmeticTheory} [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] {σ : ArithmeticSentence} (hσ : Hierarchy Σ 1 σ) : 𝐈Σ₁ ⊢ σ ⇒ₗ Bootstrapping.provabilityPred T σ

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.provable_sound {T U : ArithmeticTheory} [Theory.Δ₁ T] [U.SoundOnHierarchy Σ 1] {σ : Sentence ℒₒᵣ} : U ⊢ Bootstrapping.provabilityPred T σ → T ⊢ σ

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instHBL3ISigmaOfNatNatStandardProvabilityOfWeakerThanSentenceORingArithmeticTheoryPeanoMinus {T : ArithmeticTheory} [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] : (Theory.standardProvability T).HBL3

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instHBLISigmaOfNatNatStandardProvabilityOfWeakerThanSentenceORingArithmeticTheoryPeanoMinus {T : ArithmeticTheory} [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] : (Theory.standardProvability T).HBL

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

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