Basic

instance LO.FirstOrder.Theory.Alt.instWeakerThanSyntacticFormulaThyAlt {L : Language} {T U : Theory L} [s : T wkn U] : T wkn U.alt.thy

instance LO.FirstOrder.Theory.Alt.instWeakerThanSentenceAltOfSyntacticFormula {L : Language} {T U : Theory L} [s : T wkn U] : T.alt wkn U.alt

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

Imported declaration from the Incompleteness formalization.

• prov : Semisentence L 1

  Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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 }

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

Imported declaration from the Incompleteness formalization.

Equations

• 𝔅.con = ∼↑𝔅 ⊥

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

Imported declaration from the Incompleteness formalization.

• fixpoint : Semisentence L 1 → Sentence L

  Imported declaration from the Incompleteness formalization.

• diag (θ : Semisentence L 1) : T ⊢!. fixpoint T θ <=> θ/[⌜fixpoint T θ⌝]

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

• LT {σ : Sentence L} : T ⊢!. ↑𝔅 σ ==> σ → T ⊢!. σ

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

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.

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.

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.

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.

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.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D1_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ wkn T] {𝔅 : ProvabilityPredicate T₀ T} {σ : Sentence L} : T ⊢!. σ → T ⊢!. ↑𝔅 σ

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ wkn T] {𝔅 : ProvabilityPredicate T₀ T} {σ τ : Sentence L} [𝔅.HBL2] : T ⊢!. ↑𝔅 (σ ==> τ) ==> ↑𝔅 σ ==> ↑𝔅 τ

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D3_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ wkn T] {𝔅 : ProvabilityPredicate T₀ T} {σ : Sentence L} [𝔅.HBL3] : T ⊢!. ↑𝔅 σ ==> ↑𝔅 (↑𝔅 σ)

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.FLT_shift {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} [T₀ wkn T] {𝔅 : ProvabilityPredicate T₀ T} {σ : Sentence L} [𝔅.FormalizedLoeb] : T ⊢!. ↑𝔅 (↑𝔅 σ ==> σ) ==> ↑𝔅 σ

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2' {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} {σ τ : Sentence L} [𝔅.HBL2] [Entailment.ModusPonens T] : T₀ ⊢!. ↑𝔅 (σ ==> τ) → T₀ ⊢!. ↑𝔅 σ ==> ↑𝔅 τ

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_distribute_and {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} : T₀ ⊢!. ↑𝔅 (σ ⋏ τ) ==> ↑𝔅 σ ⋏ ↑𝔅 τ

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_distribute_and' {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} : T₀ ⊢!. ↑𝔅 (σ ⋏ τ) → T₀ ⊢!. ↑𝔅 σ ⋏ ↑𝔅 τ

Imported declaration from the Incompleteness formalization.

theorem 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₀ ⊢!. ↑𝔅 σ ⋏ ↑𝔅 τ ==> ↑𝔅 (σ ⋏ τ)

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

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

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

theorem LO.FirstOrder.DerivabilityCondition.unrefutable_goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [L.DecidableEq] [T₀ wkn T] [Diagonalization T₀] [Entailment.Consistent T] [𝔅.GoedelSound] : T ⊬. ∼𝔅.goedel

theorem LO.FirstOrder.DerivabilityCondition.goedel_independent {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ wkn T] [Diagonalization T₀] [Entailment.Consistent T] [𝔅.GoedelSound] : Entailment.Undecidable T ↑𝔅.goedel

theorem LO.FirstOrder.DerivabilityCondition.first_incompleteness {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [T₀ wkn T] [Diagonalization T₀] [Entailment.Consistent T] [𝔅.GoedelSound] : ¬Entailment.Complete T

theorem LO.FirstOrder.DerivabilityCondition.formalized_consistent_of_existance_unprovable {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] [L.DecidableEq] {σ : Sentence L} : T₀ ⊢!. ∼↑𝔅 σ ==> 𝔅.con

theorem LO.FirstOrder.DerivabilityCondition.formalized_unprovable_goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] [Diagonalization T₀] [L.DecidableEq] [T₀ wkn T] : T ⊢!. 𝔅.con ==> ∼↑𝔅 𝔅.goedel

Formalized First Incompleteness Theorem

theorem LO.FirstOrder.DerivabilityCondition.iff_goedel_consistency {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] [Diagonalization T₀] [L.DecidableEq] [T₀ wkn T] : T ⊢!. 𝔅.goedel <=> 𝔅.con

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.FirstOrder.DerivabilityCondition.kreisel_spec {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] (σ : Sentence L) : T₀ ⊢!. 𝔅.kreisel σ <=> (↑𝔅 (𝔅.kreisel σ) ==> σ)

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

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

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

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

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

theorem LO.FirstOrder.DerivabilityCondition.formalized_unprovable_not_consistency {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Entailment.Consistent T] [L.DecidableEq] [Diagonalization T₀] [T₀ wkn T] [𝔅.HBL] [𝔅.GoedelSound] : T ⊬. 𝔅.con ==> ∼↑𝔅 (∼𝔅.con)

theorem LO.FirstOrder.DerivabilityCondition.formalized_unrefutable_goedel {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Entailment.Consistent T] [L.DecidableEq] [Diagonalization T₀] [T₀ wkn T] [𝔅.HBL] [𝔅.GoedelSound] : T ⊬. 𝔅.con ==> ∼↑𝔅 (∼𝔅.goedel)

@[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) : Sentence L

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.FirstOrder.DerivabilityCondition.rosser_spec {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] : T₀ ⊢!. 𝔅.rosser <=> ∼↑𝔅 𝔅.rosser

theorem LO.FirstOrder.DerivabilityCondition.unprovable_rosser {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] [T₀ wkn T] [Entailment.Consistent T] : T ⊬. 𝔅.rosser

theorem LO.FirstOrder.DerivabilityCondition.unrefutable_rosser {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] [T₀ wkn T] [Entailment.Consistent T] [𝔅.Rosser] : T ⊬. ∼𝔅.rosser

theorem LO.FirstOrder.DerivabilityCondition.rosser_independent {L : Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} [Diagonalization T₀] [T₀ wkn T] [Entailment.Consistent T] [𝔅.Rosser] : Entailment.Undecidable T ↑𝔅.rosser

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

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

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