Incompleteness.DC.Basic

source

instance LO.FirstOrder.Theory.Alt.instSubtheorySyntacticFormulaThyAlt_incompleteness {L : Language} {T U : Theory L} [s : T ≼ U] :

T ≼ U.alt.thy

Equations

LO.FirstOrder.Theory.Alt.instSubtheorySyntacticFormulaThyAlt_incompleteness = s

source

instance LO.FirstOrder.Theory.Alt.instSubtheorySentenceAltOfSyntacticFormula_incompleteness {L : Language} {T U : Theory L} [s : T ≼ U] :

T.alt ≼ U.alt

Equations

LO.FirstOrder.Theory.Alt.instSubtheorySentenceAltOfSyntacticFormula_incompleteness = { prf := fun {f : LO.FirstOrder.Sentence L} (b : T.alt ⊢ f) => LO.System.Subtheory.prf b }

source

structure LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] (T₀ T : Theory L) :

Type u_1

prov : Semisentence L 1
spec {σ : Sentence L} : T ⊢!. σ → T₀ ⊢!. self.prov/[⌜σ⌝]

Instances For

LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.instCoeFunForallSentence

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.pr {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) (σ : Sentence L) :

Sentence L

Equations

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

source

instance LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.instCoeFunForallSentence {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} :

CoeFun (ProvabilityPredicate T₀ T) fun (x : ProvabilityPredicate T₀ T) => Sentence L → Sentence L

Equations

LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.instCoeFunForallSentence = { coe := LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.pr }

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.con {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) :

Sentence L

Equations

𝔅.con = ∼↑𝔅 ⊥

source

class LO.FirstOrder.DerivabilityCondition.Diagonalization {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] (T : Theory L) :

Type u_1

fixpoint : Semisentence L 1 → Sentence L
diag (θ : Semisentence L 1) : T ⊢!. fixpoint T θ ⭤ θ/[⌜fixpoint T θ⌝]

Instances

LO.FirstOrder.Arith.instDiagonalization

source

class LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL2 {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) :

Prop

D2 {σ τ : Sentence L} : T₀ ⊢!. ↑𝔅 (σ ➝ τ) ➝ ↑𝔅 σ ➝ ↑𝔅 τ

Instances

LO.FirstOrder.Arith.instHBL2StandardDP

source

class LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL3 {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) :

Prop

D3 {σ : Sentence L} : T₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 (↑𝔅 σ)

Instances

LO.FirstOrder.Arith.instHBL3StandardDP

source

class LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) extends 𝔅.HBL2, 𝔅.HBL3 :

Prop

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

Instances

LO.FirstOrder.Arith.instHBLStandardDP

source

class LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Loeb {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) :

Prop

LT {σ : Sentence L} : T ⊢!. ↑𝔅 σ ➝ σ → T ⊢!. σ

Instances

LO.FirstOrder.DerivabilityCondition.instLoeb

source

class LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.FormalizedLoeb {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) :

Prop

FLT {σ : Sentence L} : T₀ ⊢!. ↑𝔅 (↑𝔅 σ ➝ σ) ➝ ↑𝔅 σ

Instances

LO.FirstOrder.DerivabilityCondition.instFormalizedLoebOfDecidableEq

source

class LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Rosser {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) :

Prop

Ro {σ : Sentence L} : T ⊢!. ∼σ → T₀ ⊢!. ∼↑𝔅 σ

Instances

source

@[reducible, inline]

abbrev LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D1 {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} {σ : Sentence L} :

T ⊢!. σ → T₀ ⊢!. ↑𝔅 σ

Equations

⋯ = ⋯

source

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2 {L : Language} {inst✝ : Semiterm.Operator.GoedelNumber L (Sentence L)} {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [self : 𝔅.HBL2] {σ τ : Sentence L} :

T₀ ⊢!. ↑𝔅 (σ ➝ τ) ➝ ↑𝔅 σ ➝ ↑𝔅 τ

Alias of LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL2.D2.

source

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D3 {L : Language} {inst✝ : Semiterm.Operator.GoedelNumber L (Sentence L)} {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [self : 𝔅.HBL3] {σ : Sentence L} :

T₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 (↑𝔅 σ)

Alias of LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL3.D3.

source

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.LT {L : Language} {inst✝ : Semiterm.Operator.GoedelNumber L (Sentence L)} {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [self : 𝔅.Loeb] {σ : Sentence L} :

T ⊢!. ↑𝔅 σ ➝ σ → T ⊢!. σ

Alias of LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Loeb.LT.

source

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.FLT {L : Language} {inst✝ : Semiterm.Operator.GoedelNumber L (Sentence L)} {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [self : 𝔅.FormalizedLoeb] {σ : Sentence L} :

T₀ ⊢!. ↑𝔅 (↑𝔅 σ ➝ σ) ➝ ↑𝔅 σ

Alias of LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.FormalizedLoeb.FLT.

source

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Ro {L : Language} {inst✝ : Semiterm.Operator.GoedelNumber L (Sentence L)} {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [self : 𝔅.Rosser] {σ : Sentence L} :

T ⊢!. ∼σ → T₀ ⊢!. ∼↑𝔅 σ

Alias of LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Rosser.Ro.

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D1_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ ≼ T] {𝔅 : ProvabilityPredicate T₀ T} {σ : Sentence L} :

T ⊢!. σ → T ⊢!. ↑𝔅 σ

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ ≼ T] {𝔅 : ProvabilityPredicate T₀ T} {σ τ : Sentence L} [𝔅.HBL2] :

T ⊢!. ↑𝔅 (σ ➝ τ) ➝ ↑𝔅 σ ➝ ↑𝔅 τ

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D3_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ ≼ T] {𝔅 : ProvabilityPredicate T₀ T} {σ : Sentence L} [𝔅.HBL3] :

T ⊢!. ↑𝔅 σ ➝ ↑𝔅 (↑𝔅 σ)

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.FLT_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ ≼ T] {𝔅 : ProvabilityPredicate T₀ T} {σ : Sentence L} [𝔅.FormalizedLoeb] :

T ⊢!. ↑𝔅 (↑𝔅 σ ➝ σ) ➝ ↑𝔅 σ

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2' {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} {σ τ : Sentence L} [𝔅.HBL2] [System.ModusPonens T] :

T₀ ⊢!. ↑𝔅 (σ ➝ τ) → T₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 τ

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_distribute_imply {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} (h : T ⊢!. σ ➝ τ) :

T₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 τ

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_distribute_iff {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} (h : T ⊢!. σ ⭤ τ) :

T₀ ⊢!. ↑𝔅 σ ⭤ ↑𝔅 τ

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_distribute_and {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] [L.DecidableEq] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} :

T₀ ⊢!. ↑𝔅 (σ ⋏ τ) ➝ ↑𝔅 σ ⋏ ↑𝔅 τ

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_distribute_and' {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] [L.DecidableEq] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} :

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

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_collect_and {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} :

T₀ ⊢!. ↑𝔅 σ ⋏ ↑𝔅 τ ➝ ↑𝔅 (σ ⋏ τ)

Equations

⋯ = ⋯

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [Diagonalization T₀] (𝔅 : ProvabilityPredicate T₀ T) :

Sentence L

Equations

𝔅.goedel = LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T₀ (∼𝔅.prov/[LO.FirstOrder.Semiterm.bvar 0])

source

theorem LO.FirstOrder.DerivabilityCondition.goedel_spec {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] :

T₀ ⊢!. 𝔅.goedel ⭤ ∼↑𝔅 𝔅.goedel

source

class LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.GoedelSound {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} (𝔅 : ProvabilityPredicate T₀ T) [Diagonalization T₀] :

Prop

γ_sound : T ⊢!. ↑𝔅 𝔅.goedel → T ⊢!. 𝔅.goedel

Instances

LO.FirstOrder.Arith.instGoedelSoundStandardDP

source

theorem LO.FirstOrder.DerivabilityCondition.unprovable_goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [System.Consistent T] :

T ⊬. 𝔅.goedel

source

theorem LO.FirstOrder.DerivabilityCondition.unrefutable_goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [System.Consistent T] [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [𝔅.GoedelSound] :

T ⊬. ∼𝔅.goedel

source

theorem LO.FirstOrder.DerivabilityCondition.goedel_independent {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [System.Consistent T] [L.DecidableEq] [𝔅.GoedelSound] :

System.Undecidable T ↑𝔅.goedel

source

theorem LO.FirstOrder.DerivabilityCondition.first_incompleteness {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [System.Consistent T] [L.DecidableEq] [𝔅.GoedelSound] :

¬System.Complete T

source

theorem LO.FirstOrder.DerivabilityCondition.formalized_consistent_of_existance_unprovable {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [L.DecidableEq] [𝔅.HBL] {σ : Sentence L} :

T₀ ⊢!. ∼↑𝔅 σ ➝ 𝔅.con

source

theorem LO.FirstOrder.DerivabilityCondition.formalized_unprovable_goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization T₀] :

T ⊢!. 𝔅.con ➝ ∼↑𝔅 𝔅.goedel

Formalized First Incompleteness Theorem

source

theorem LO.FirstOrder.DerivabilityCondition.iff_goedel_consistency {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization T₀] :

T ⊢!. 𝔅.goedel ⭤ 𝔅.con

source

theorem LO.FirstOrder.DerivabilityCondition.unprovable_consistency {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization T₀] [System.Consistent T] :

T ⊬. 𝔅.con

source

theorem LO.FirstOrder.DerivabilityCondition.unrefutable_consistency {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization T₀] [System.Consistent T] [𝔅.GoedelSound] :

T ⊬. ∼𝔅.con

source

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.kreisel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [Diagonalization T₀] (𝔅 : ProvabilityPredicate T₀ T) [𝔅.HBL] (σ : Sentence L) :

Sentence L

Equations

𝔅.kreisel σ = LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T₀ (𝔅.prov/[LO.FirstOrder.Semiterm.bvar 0] ➝ σ/[])

source

theorem LO.FirstOrder.DerivabilityCondition.kreisel_spec {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] [Diagonalization T₀] (σ : Sentence L) :

T₀ ⊢!. 𝔅.kreisel σ ⭤ (↑𝔅 (𝔅.kreisel σ) ➝ σ)

source

theorem LO.FirstOrder.DerivabilityCondition.loeb_theorm {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [𝔅.HBL] {σ : Sentence L} (H : T ⊢!. ↑𝔅 σ ➝ σ) :

T ⊢!. σ

source

instance LO.FirstOrder.DerivabilityCondition.instLoeb {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [𝔅.HBL] :

𝔅.Loeb

source

theorem LO.FirstOrder.DerivabilityCondition.formalized_loeb_theorem {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [𝔅.HBL] {σ : Sentence L} [L.DecidableEq] :

T₀ ⊢!. ↑𝔅 (↑𝔅 σ ➝ σ) ➝ ↑𝔅 σ

source

instance LO.FirstOrder.DerivabilityCondition.instFormalizedLoebOfDecidableEq {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [Diagonalization T₀] [𝔅.HBL] [L.DecidableEq] :

𝔅.FormalizedLoeb

source

theorem LO.FirstOrder.DerivabilityCondition.unprovable_consistency_via_loeb {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [System.Consistent T] [𝔅.Loeb] :

T ⊬. 𝔅.con

source

theorem LO.FirstOrder.DerivabilityCondition.formalized_unprovable_not_consistency {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [System.Consistent T] [L.DecidableEq] [Diagonalization T₀] [T₀ ≼ T] [𝔅.HBL] [𝔅.GoedelSound] :

T ⊬. 𝔅.con ➝ ∼↑𝔅 (∼𝔅.con)

source

theorem LO.FirstOrder.DerivabilityCondition.formalized_unrefutable_goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [System.Consistent T] [L.DecidableEq] [Diagonalization T₀] [T₀ ≼ T] [𝔅.HBL] [𝔅.GoedelSound] :

T ⊬. 𝔅.con ➝ ∼↑𝔅 (∼𝔅.goedel)

source

@[reducible, inline]

abbrev LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.rosser {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [Diagonalization T₀] (𝔅 : ProvabilityPredicate T₀ T) [𝔅.Rosser] :

Sentence L

Equations

𝔅.rosser = LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T₀ (∼𝔅.prov/[LO.FirstOrder.Semiterm.bvar 0])

source

theorem LO.FirstOrder.DerivabilityCondition.rosser_spec {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] [𝔅.Rosser] :

T₀ ⊢!. 𝔅.rosser ⭤ ∼↑𝔅 𝔅.rosser

source

theorem LO.FirstOrder.DerivabilityCondition.unprovable_rosser {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] [T₀ ≼ T] [System.Consistent T] [𝔅.Rosser] :

T ⊬. 𝔅.rosser

source

theorem LO.FirstOrder.DerivabilityCondition.unrefutable_rosser {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] [T₀ ≼ T] [System.Consistent T] [𝔅.Rosser] :

T ⊬. ∼𝔅.rosser

source

theorem LO.FirstOrder.DerivabilityCondition.rosser_independent {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] [T₀ ≼ T] [System.Consistent T] [𝔅.Rosser] :

System.Undecidable T ↑𝔅.rosser

source

theorem LO.FirstOrder.DerivabilityCondition.rosser_first_incompleteness {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [Diagonalization T₀] [T₀ ≼ T] [System.Consistent T] (𝔅 : ProvabilityPredicate T₀ T) [𝔅.Rosser] :

¬System.Complete T

source

theorem LO.FirstOrder.DerivabilityCondition.kriesel_remark {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ ≼ T] [𝔅.Rosser] :

T ⊢!. 𝔅.con

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