Supporting results for pointwise provable equality.

Rosser's provability predicate

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

The Rosser Provable construction in FFL.FirstOrder.Theory.

Equations

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

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

The rosser Provable construction in FFL.FirstOrder.Theory.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Theory.rosserPred {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : ArithmeticSentence

The rosser Pred construction in FFL.FirstOrder.Theory.

Equations

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.rosserProvable_D1 {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] [Entailment.Consistent T] {σ : Sentence L} : T ⊢ σ → 𝐈Σ₁ ⊢ T.rosserPred σ

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

The rosser Provability construction in FFL.FirstOrder.Theory.

Equations

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

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

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.incomplete_GR (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐈Σ₁ ≼ T] [Entailment.Consistent T] : Entailment.Incomplete T

Gödel-Rosser incompleteness theorem

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryTheoryISigmaOfNatNatCraigOfRE {T : ArithmeticTheory} [Theory.RE T] [𝐈Σ₁ ≼ T] : 𝐈Σ₁ ≼ Theory.craig T

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.incomplete_GR_of_RE (T : ArithmeticTheory) [Theory.RE T] [𝐈Σ₁ ≼ T] [Entailment.Consistent T] : Entailment.Incomplete T

Gödel-Rosser incompleteness theorem for r.e. theories

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.exists_true_but_unprovable_sentence_of_RE_of_consistent (T : ArithmeticTheory) [Theory.RE T] [𝐈Σ₁ ≼ T] [Entailment.Consistent T] : ∃ (δ : ArithmeticSentence), ℕ↓[ℒₒᵣ] ⊧ δ ∧ T ⊬ δ