Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Basic

@[reducible, inline]

abbrev LO.FirstOrder.Language.ReferenceableBy (L : Language) (L₀ : Language) :

Type (max u_1 u_2)

Equations

L.ReferenceableBy L₀ = LO.FirstOrder.Semiterm.Operator.GödelNumber L₀ (LO.FirstOrder.Sentence L)

Instances For

structure LO.FirstOrder.ProvabilityAbstraction.Provability {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] (T₀ : Theory L₀) (T : Theory L) :

Type u_1

prov : Semisentence L₀ 1
bew_def {σ : Sentence L} : T ⊢ σ → T₀ ⊢ self.prov/[⌜σ⌝]
Derivability condition D1

Instances For

source

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

Sentence L₀

Equations

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

Instances For

source

@[implicit_reducible]

instance LO.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

LO.FirstOrder.ProvabilityAbstraction.Provability.instCoeFunForallSentence = { coe := LO.FirstOrder.ProvabilityAbstraction.Provability.pr }

source

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

Sentence L₀

Equations

𝔅.con = ∼↑𝔅 ⊥

Instances For

source

@[reducible, inline]

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

Sentence L₀

Equations

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

Instances For

source

theorem LO.FirstOrder.ProvabilityAbstraction.Provability.D1 {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ : Sentence L} :

T ⊢ σ → T₀ ⊢ ↑𝔅 σ

source

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

Prop

D2 {σ τ : Sentence L} : T₀ ⊢ ↑𝔅 (σ 🡒 τ) 🡒 ↑𝔅 σ 🡒 ↑𝔅 τ

Instances

source

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

Prop

D3 {σ : Sentence L} : T₀ ⊢ ↑𝔅 σ 🡒 ↑𝔅 (↑𝔅 σ)

Instances

source

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

Prop

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

Instances

source

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

Prop

mono {σ τ : Sentence L} : T ⊢ σ 🡒 τ → T₀ ⊢ ↑𝔅 σ 🡒 ↑𝔅 τ

Instances

source

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

Prop

ext {σ τ : Sentence L} : T ⊢ σ 🡘 τ → T₀ ⊢ ↑𝔅 σ 🡘 ↑𝔅 τ

Instances

source

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

Prop

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

Instances

source

class LO.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₀ ⊢ σ 🡒 ↑𝔅 σ

Instances

source

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

𝔅.HBL3

source

class LO.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 ⊢ σ

Instances

source

class LO.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] [Structure L₀ M] :

Prop

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

Instances

source

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

T₀ ⊢ ↑𝔅 σ → T ⊢ σ

source

theorem LO.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₀ ⊢ ↑𝔅 σ 🡒 ↑𝔅 τ

source

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

𝔅.Mono

source

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

𝔅.Ext

source

theorem LO.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] [L₀.DecidableEq] :

T₀ ⊢ ↑𝔅 (σ ⋏ τ) 🡒 ↑𝔅 σ ⋏ ↑𝔅 τ

source

theorem LO.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] [L₀.DecidableEq] :

T₀ ⊢ ↑𝔅 (σ ⋏ τ) → T₀ ⊢ ↑𝔅 σ ⋏ ↑𝔅 τ

source

theorem LO.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] [L₀.DecidableEq] [L.DecidableEq] :

T₀ ⊢ ↑𝔅 σ ⋏ ↑𝔅 τ 🡒 ↑𝔅 (σ ⋏ τ)

source

theorem LO.FirstOrder.ProvabilityAbstraction.Provability.dia_mono {L₀ : Language} {L : Language} [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} {𝔅 : Provability T₀ T} {σ τ : Sentence L} [L₀.DecidableEq] [L.DecidableEq] [𝔅.Mono] (h : T ⊢ σ 🡒 τ) :

T₀ ⊢ 𝔅.dia σ 🡒 𝔅.dia τ

source

theorem LO.FirstOrder.ProvabilityAbstraction.Provability.mono' {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [T₀ ⪯ T] {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.Mono] (h : T₀ ⊢ σ 🡒 τ) :

T₀ ⊢ ↑𝔅 σ 🡒 ↑𝔅 τ

source

theorem LO.FirstOrder.ProvabilityAbstraction.Provability.ext' {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [T₀ ⪯ T] {𝔅 : Provability T₀ T} {σ τ : Sentence L} [𝔅.Ext] (h : T₀ ⊢ σ 🡘 τ) :

T₀ ⊢ ↑𝔅 σ 🡘 ↑𝔅 τ

source

class LO.FirstOrder.ProvabilityAbstraction.Diagonalization {L : Language} [L.ReferenceableBy L] (T : Theory L) :

Type u_1

fixedpoint : Semisentence L 1 → Sentence L
diag (θ : Semisentence L 1) : T ⊢ fixedpoint T θ 🡘 θ/[⌜fixedpoint T θ⌝]

Instances

source

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

Sentence L

Equations

LO.FirstOrder.ProvabilityAbstraction.gödel 𝔅 = LO.FirstOrder.ProvabilityAbstraction.Diagonalization.fixedpoint T₀ (∼𝔅.prov/[LO.FirstOrder.Semiterm.bvar 0])

Instances For

source

theorem LO.FirstOrder.ProvabilityAbstraction.gödel_spec {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} :

T₀ ⊢ gödel 𝔅 🡘 ∼↑𝔅 (gödel 𝔅)

source

theorem LO.FirstOrder.ProvabilityAbstraction.unprovable_gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [L.DecidableEq] [T₀ ⪯ T] [Entailment.Consistent T] :

T ⊬ gödel 𝔅

source

theorem LO.FirstOrder.ProvabilityAbstraction.unrefutable_gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [L.DecidableEq] [T₀ ⪯ T] [Entailment.Consistent T] [𝔅.Kreisel] :

T ⊬ ∼gödel 𝔅

source

theorem LO.FirstOrder.ProvabilityAbstraction.gödel_independent {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [L.DecidableEq] [T₀ ⪯ T] [Entailment.Consistent T] [𝔅.Kreisel] :

Entailment.Independent T (gödel 𝔅)

source

theorem LO.FirstOrder.ProvabilityAbstraction.first_incompleteness {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [L.DecidableEq] [T₀ ⪯ T] [Entailment.Consistent T] [𝔅.Kreisel] :

Entailment.Incomplete T

source

theorem LO.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

source

theorem LO.FirstOrder.ProvabilityAbstraction.formalized_unprovable_gödel {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} [𝔅.HBL] [L.DecidableEq] [T₀ ⪯ T] :

T₀ ⊢ 𝔅.con 🡒 ∼↑𝔅 (gödel 𝔅)

Formalized First Incompleteness Theorem

source

theorem LO.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

source

theorem LO.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

source

theorem LO.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

source

theorem LO.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

source

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

Sentence L

Equations

LO.FirstOrder.ProvabilityAbstraction.kreisel 𝔅 σ = LO.FirstOrder.ProvabilityAbstraction.Diagonalization.fixedpoint T₀ (𝔅.prov/[LO.FirstOrder.Semiterm.bvar 0] 🡒 σ/[])

Instances For

source

theorem LO.FirstOrder.ProvabilityAbstraction.kreisel_spec {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} {σ : Sentence L} :

T₀ ⊢ kreisel 𝔅 σ 🡘 (↑𝔅 (kreisel 𝔅 σ) 🡒 σ)

source

theorem LO.FirstOrder.ProvabilityAbstraction.löb_theorem {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} {σ : Sentence L} [𝔅.HBL] [L.DecidableEq] [T₀ ⪯ T] (H : T ⊢ ↑𝔅 σ 🡒 σ) :

T ⊢ σ

source

theorem LO.FirstOrder.ProvabilityAbstraction.formalized_löb_theorem {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] {𝔅 : Provability T₀ T} {σ : Sentence L} [𝔅.HBL] [L.DecidableEq] [T₀ ⪯ T] :

T₀ ⊢ ↑𝔅 (↑𝔅 σ 🡒 σ) 🡒 ↑𝔅 σ

source

theorem LO.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)

source

theorem LO.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 𝔅)

source

theorem LO.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 𝔅

source

theorem LO.FirstOrder.ProvabilityAbstraction.rosser_independent {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] [T₀ ⪯ T] [Entailment.Consistent T] {𝔅 : Provability T₀ T} [L.DecidableEq] [𝔅.Rosser] :

Entailment.Independent T (gödel 𝔅)

source

theorem LO.FirstOrder.ProvabilityAbstraction.rosser_first_incompleteness {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] [T₀ ⪯ T] [Entailment.Consistent T] [L.DecidableEq] (𝔅 : Provability T₀ T) [𝔅.Rosser] :

Entailment.Incomplete T

source

theorem LO.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.

Abstract incompleteness theorems and related results #