Rosser's provability predicate

def LO.FirstOrder.Theory.RosserProvable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (φ : V) : Prop

Equations

• T.RosserProvable φ = T.ProvabilityComparisonLE φ (LO.FirstOrder.Arithmetic.Bootstrapping.neg L φ)

noncomputable def LO.FirstOrder.Theory.rosserProvable {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚺₁.Semisentence 1

Equations

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

instance LO.FirstOrder.Theory.RosserProvable_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚺₁-Predicate T.RosserProvable via T.rosserProvable

instance LO.FirstOrder.Theory.rosserProvable_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚺₁-Predicate T.RosserProvable

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Theory.rosserPred {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : ArithmeticSentence

Equations

• T.rosserPred σ = ↑T.rosserProvable/[⌜σ⌝]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.rosser_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Proposition L} : T.RosserProvable ⌜φ⌝ ↔ T.ProvabilityComparisonLE ⌜φ⌝ ⌜∼φ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.rosser_quote₀ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : T.RosserProvable ⌜φ⌝ ↔ T.ProvabilityComparisonLE ⌜φ⌝ ⌜∼φ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.rosser_quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Proposition L} : T.RosserProvable ⌜φ⌝ ↔ ∃ (b : V), Proof T b ⌜φ⌝ ∧ ∀ b' < b, ¬Proof T b' ⌜∼φ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.rosser_quote_def₀ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : T.RosserProvable ⌜φ⌝ ↔ ∃ (b : V), Proof T b ⌜φ⌝ ∧ ∀ b' < b, ¬Proof T b' ⌜∼φ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.RosserProvable.to_provable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : T.RosserProvable φ → Provable T φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.provable_of_standard_proof {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {n : ℕ} {φ : Sentence L} : Proof T ↑n ⌜φ⌝ → T ⊢ φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.rosser_internalize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] [Entailment.Consistent T] {φ : Sentence L} : T ⊢ φ → T.RosserProvable ⌜φ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.rosser_internalize_sentence {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] [Entailment.Consistent T] {σ : Sentence L} : T ⊢ σ → T.RosserProvable ⌜σ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.not_rosserProvable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] [Entailment.Consistent T] {φ : Sentence L} : T ⊢ ∼φ → ¬T.RosserProvable ⌜φ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.not_rosserProvable_sentence {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] [Entailment.Consistent T] {σ : Sentence L} : T ⊢ ∼σ → ¬T.RosserProvable ⌜σ⌝

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

theorem LO.FirstOrder.Arithmetic.rosserProvable_rosser {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] [Entailment.Consistent T] {σ : Sentence L} : T ⊢ ∼σ → 𝗜𝚺₁ ⊢ ∼T.rosserPred σ

@[reducible, inline]

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

Equations

• T.rosserProvability = { prov := ↑T.rosserProvable, bew_def := ⋯ }

instance LO.FirstOrder.Arithmetic.instRosserISigmaOfNatNatRosserProvability {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] [Entailment.Consistent T] : T.rosserProvability.Rosser

theorem LO.FirstOrder.Arithmetic.rosserProvability_def {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] [Entailment.Consistent T] (σ : Sentence L) : ↑T.rosserProvability σ = T.rosserPred σ

instance LO.FirstOrder.Arithmetic.instSoundOnISigmaOfNatNatRosserProvability {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] [Entailment.Consistent T] : T.rosserProvability.SoundOn ℕ

theorem LO.FirstOrder.Arithmetic.incomplete_GR (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [Entailment.Consistent T] : Entailment.Incomplete T

Gödel-Rosser incompleteness theorem