Supporting results for pointwise provable equality.

Abstract incompleteness theorems and related results

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Language.ReferenceableBy (L : Language) (L₀ : Language) : Type (max u_1 u_2)

The Referenceable By construction in FFL.FirstOrder.Language.

Equations

• L.ReferenceableBy L₀ = PointwiseComposition.FFL.FirstOrder.Semiterm.Operator.GödelNumber L₀ (PointwiseComposition.FFL.FirstOrder.Sentence L)

structure PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] (T₀ : Theory L₀) (T : Theory L) : Type u_1

Data and laws for Provability in FFL.FirstOrder.ProvabilityAbstraction.

• prov : Semisentence L₀ 1

  The prov construction in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• bew_def {σ : Sentence L} : T ⊢ σ → T₀ ⊢ self.prov/[⌜σ⌝]

  Derivability condition D1

def PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.pr {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) (σ : Sentence L) : Sentence L₀

The pr construction in FFL.FirstOrder.ProvabilityAbstraction.Provability.

Equations

• ↑𝔅 σ = 𝔅.prov/[⌜σ⌝]

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.instCoeFunForallSentence {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} : CoeFun (Provability T₀ T) fun (x : Provability T₀ T) => Sentence L → Sentence L₀

Equations

• PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.instCoeFunForallSentence = { coe := PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.pr }

def PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.con {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) : Sentence L₀

The con construction in FFL.FirstOrder.ProvabilityAbstraction.Provability.

Equations

• 𝔅.con = ∼↑𝔅 ⊥

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.dia {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) (φ : Sentence L) : Sentence L₀

The dia construction in FFL.FirstOrder.ProvabilityAbstraction.Provability.

Equations

• 𝔅.dia φ = ∼↑𝔅 (∼φ)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.D1 {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ : Sentence L} : T ⊢ σ → T₀ ⊢ ↑𝔅 σ

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.HBL2 {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) : Prop

Data and laws for HBL2 in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• D2 {σ τ : Sentence L} : T₀ ⊢ ↑𝔅 (σ ⇒ₗ τ) ⇒ₗ ↑𝔅 σ ⇒ₗ ↑𝔅 τ

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.HBL3 {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) : Prop

Data and laws for HBL3 in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• D3 {σ : Sentence L} : T₀ ⊢ ↑𝔅 σ ⇒ₗ ↑𝔅 (↑𝔅 σ)

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.HBL {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) extends 𝔅.HBL2, 𝔅.HBL3 : Prop

Data and laws for HBL in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• D2 {σ τ : Sentence L} : T₀ ⊢ ↑𝔅 (σ ⇒ₗ τ) ⇒ₗ ↑𝔅 σ ⇒ₗ ↑𝔅 τ
• D3 {σ : Sentence L} : T₀ ⊢ ↑𝔅 σ ⇒ₗ ↑𝔅 (↑𝔅 σ)

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.Mono {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) : Prop

Data and laws for Mono in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• mono {σ τ : Sentence L} : T ⊢ σ ⇒ₗ τ → T₀ ⊢ ↑𝔅 σ ⇒ₗ ↑𝔅 τ

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.Ext {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) : Prop

Data and laws for Ext in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• ext {σ τ : Sentence L} : T ⊢ σ ⇔ₗ τ → T₀ ⊢ ↑𝔅 σ ⇔ₗ ↑𝔅 τ

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.Rosser {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) : Prop

Data and laws for Rosser in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• Ros {σ : Sentence L} : T ⊢ ∼σ → T₀ ⊢ ∼↑𝔅 σ

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.FormalizedCompleteOn {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) (σ : Sentence L) : Prop

Abstract version of formalized Γ-completeness for provability 𝔅.

example: [∀ σ ∈ Σ₁, 𝔅.FormalizedCompleteOn σ] for formalized Σ₁-completeness.

• formalized_complete_on : T₀ ⊢ σ ⇒ₗ ↑𝔅 σ

instance PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.instHBL3OfFormalizedCompleteOnPr {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) [∀ (σ : Sentence L), 𝔅.FormalizedCompleteOn (↑𝔅 σ)] : 𝔅.HBL3

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.Kreisel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) : Prop

NOTE: Named after [Vis21].

• KR {σ : Sentence L} : T ⊢ ↑𝔅 σ → T ⊢ σ

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.SoundOn {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) (M : outParam (Type u_1)) [Nonempty M] [Tarski.Structure L₀ M] : Prop

Data and laws for Sound On in FFL.FirstOrder.ProvabilityAbstraction.Provability.

• sound_on {σ : Sentence L} : M↓[L₀] ⊧ ↑𝔅 σ → T ⊢ σ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.syntactical_sound {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} (M : Type u_1) [Nonempty M] [Tarski.Structure L M] [𝔅.SoundOn M] [M↓[L] ⊧* T₀] {σ : Sentence L} : T₀ ⊢ ↑𝔅 σ → T ⊢ σ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.bew_distribute_imply {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.HBL2] (h : T₀ ⊢ ↑𝔅 (σ ⇒ₗ τ)) : T₀ ⊢ ↑𝔅 σ ⇒ₗ ↑𝔅 τ

instance PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.instMonoOfHBL2 {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} [𝔅.HBL2] : 𝔅.Mono

instance PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.instExtOfHBL2 {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} [𝔅.HBL2] : 𝔅.Ext

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.bew_distribute_and {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.HBL2] : T₀ ⊢ ↑𝔅 (σ ⋏ τ) ⇒ₗ ↑𝔅 σ ⋏ ↑𝔅 τ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.bew_distribute_and' {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.HBL2] : T₀ ⊢ ↑𝔅 (σ ⋏ τ) → T₀ ⊢ ↑𝔅 σ ⋏ ↑𝔅 τ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.bew_collect_and {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.HBL2] : T₀ ⊢ ↑𝔅 σ ⋏ ↑𝔅 τ ⇒ₗ ↑𝔅 (σ ⋏ τ)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.dia_mono {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.Mono] (h : T ⊢ σ ⇒ₗ τ) : T₀ ⊢ 𝔅.dia σ ⇒ₗ 𝔅.dia τ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.mono' {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [T₀ ≼ T] {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.Mono] (h : T₀ ⊢ σ ⇒ₗ τ) : T₀ ⊢ ↑𝔅 σ ⇒ₗ ↑𝔅 τ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Provability.ext' {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [T₀ ≼ T] {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.Ext] (h : T₀ ⊢ σ ⇔ₗ τ) : T₀ ⊢ ↑𝔅 σ ⇔ₗ ↑𝔅 τ

class PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.Diagonalization {L : Language} [L.ReferenceableBy L] (T : Theory L) : Type u_1

Data and laws for Diagonalization in FFL.FirstOrder.ProvabilityAbstraction.

• fixedpoint : Semisentence L 1 → Sentence L

  The fixedpoint construction in FFL.FirstOrder.ProvabilityAbstraction.Diagonalization.

• diag (θ : Semisentence L 1) : T ⊢ fixedpoint T θ ⇔ₗ θ/[⌜fixedpoint T θ⌝]

def PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] (𝔅 : Provability T₀ T) : Sentence L

The gödel construction in FFL.FirstOrder.ProvabilityAbstraction.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.gödel_spec {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} : T₀ ⊢ gödel 𝔅 ⇔ₗ ∼↑𝔅 (gödel 𝔅)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.unprovable_gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [T₀ ≼ T] [Entailment.Consistent T] : T ⊬ gödel 𝔅

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.unrefutable_gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [T₀ ≼ T] [Entailment.Consistent T] [𝔅.Kreisel] : T ⊬ ∼gödel 𝔅

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.gödel_independent {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [T₀ ≼ T] [Entailment.Consistent T] [𝔅.Kreisel] : Entailment.Independent T (gödel 𝔅)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.first_incompleteness {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [T₀ ≼ T] [Entailment.Consistent T] [𝔅.Kreisel] : Entailment.Incomplete T

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.formalized_consistent_of_existance_unprovable {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} {𝔅 : Provability T₀ T} [𝔅.HBL] {σ : Sentence L} [L.DecidableEq] : T₀ ⊢ ∼↑𝔅 σ ⇒ₗ 𝔅.con

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.formalized_unprovable_gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [T₀ ≼ T] : T₀ ⊢ 𝔅.con ⇒ₗ ∼↑𝔅 (gödel 𝔅)

Formalized First Incompleteness Theorem

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.gödel_iff_con {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [L.DecidableEq] [T₀ ≼ T] : T₀ ⊢ gödel 𝔅 ⇔ₗ 𝔅.con

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.con_unprovable {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [L.DecidableEq] [T₀ ≼ T] [Entailment.Consistent T] : T ⊬ 𝔅.con

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.con_unrefutable {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [L.DecidableEq] [T₀ ≼ T] [Entailment.Consistent T] [𝔅.Kreisel] : T ⊬ ∼𝔅.con

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.con_independent {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [L.DecidableEq] [T₀ ≼ T] [Entailment.Consistent T] [𝔅.Kreisel] : Entailment.Independent T 𝔅.con

def PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.kreisel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] (𝔅 : Provability T₀ T) (σ : Sentence L) : Sentence L

The kreisel construction in FFL.FirstOrder.ProvabilityAbstraction.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.kreisel_spec {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} {σ : Sentence L} : T₀ ⊢ kreisel 𝔅 σ ⇔ₗ (↑𝔅 (kreisel 𝔅 σ) ⇒ₗ σ)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.löb_theorem {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} {σ : Sentence L} [𝔅.HBL] [T₀ ≼ T] (H : T ⊢ ↑𝔅 σ ⇒ₗ σ) : T ⊢ σ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.formalized_löb_theorem {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} {σ : Sentence L} [𝔅.HBL] [T₀ ≼ T] : T₀ ⊢ ↑𝔅 (↑𝔅 σ ⇒ₗ σ) ⇒ₗ ↑𝔅 σ

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.formalized_unprovable_not_con {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [L.DecidableEq] [T₀ ≼ T] [Entailment.Consistent T] [𝔅.Kreisel] : T ⊬ 𝔅.con ⇒ₗ ∼↑𝔅 (∼𝔅.con)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.formalized_unrefutable_gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [L.DecidableEq] [T₀ ≼ T] [Entailment.Consistent T] [𝔅.Kreisel] : T ⊬ 𝔅.con ⇒ₗ ∼↑𝔅 (∼gödel 𝔅)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.unrefutable_rosser {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] [T₀ ≼ T] [Entailment.Consistent T] {𝔅 : Provability T₀ T} [𝔅.Rosser] : T ⊬ ∼gödel 𝔅

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.rosser_independent {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] [T₀ ≼ T] [Entailment.Consistent T] {𝔅 : Provability T₀ T} [𝔅.Rosser] : Entailment.Independent T (gödel 𝔅)

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.rosser_first_incompleteness {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] [T₀ ≼ T] [Entailment.Consistent T] (𝔅 : Provability T₀ T) [𝔅.Rosser] : Entailment.Incomplete T

theorem PointwiseComposition.FFL.FirstOrder.ProvabilityAbstraction.kreisel_remark {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [T₀ ≼ T] {𝔅 : Provability T₀ T} [𝔅.Rosser] : T ⊢ 𝔅.con

If 𝔅 satisfies Rosser provability condition, then 𝔅.con is provable from T.