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

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 }

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/[⌜σ⌝]

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/[⌜σ⌝]

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

Equations

• 𝔅.con = ∼↑𝔅 ⊥

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 θ⌝]

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

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₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 (↑𝔅 σ)

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₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 (↑𝔅 σ)

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 ⊢!. σ

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₀ ⊢!. ↑𝔅 (↑𝔅 σ ➝ σ) ➝ ↑𝔅 σ

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₀ ⊢!. ∼↑𝔅 σ

@[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

• ⋯ = ⋯

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.

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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])

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

• γ_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₀ ≼ T] [Diagonalization T₀] [System.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} [T₀ ≼ T] [Diagonalization T₀] [System.Consistent T] [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [𝔅.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₀ ≼ T] [Diagonalization T₀] [System.Consistent T] [L.DecidableEq] [𝔅.GoedelSound] : System.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₀ ≼ T] [Diagonalization T₀] [System.Consistent T] [L.DecidableEq] [𝔅.GoedelSound] : ¬System.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} [L.DecidableEq] [𝔅.HBL] {σ : 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} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization 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} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization 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} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization T₀] [System.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} [L.DecidableEq] [𝔅.HBL] [T₀ ≼ T] [Diagonalization T₀] [System.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) [𝔅.HBL] (σ : Sentence L) : Sentence L

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} [𝔅.HBL] [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₀ ≼ 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₀ ≼ 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₀ ≼ T] [Diagonalization T₀] [𝔅.HBL] {σ : Sentence L} [L.DecidableEq] : T₀ ⊢!. ↑𝔅 (↑𝔅 σ ➝ σ) ➝ ↑𝔅 σ

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

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

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)

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)

@[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])

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

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

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

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

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

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.