instance LO.FirstOrder.Theory.Alt.instSubtheorySyntacticFormulaThyAlt_incompleteness {L : LO.FirstOrder.Language} {T U : LO.FirstOrder.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 : LO.FirstOrder.Language} {T U : LO.FirstOrder.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 : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] (T₀ T : LO.FirstOrder.Theory L) : Type u_1

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

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

Equations

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

instance LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.instCoeFunForallSentence {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {T₀ T : LO.FirstOrder.Theory L} : CoeFun (LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T) fun (x : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T) => LO.FirstOrder.Sentence L → LO.FirstOrder.Sentence L

Equations

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

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

Equations

• 𝔅.con = ∼↑𝔅 ⊥

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

• fixpoint : LO.FirstOrder.Semisentence L 1 → LO.FirstOrder.Sentence L
• diag : ∀ (θ : LO.FirstOrder.Semisentence L 1), T ⊢!. LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T θ ⭤ θ/[⌜LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T θ⌝]

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

• D2 : ∀ {σ τ : LO.FirstOrder.Sentence L}, T₀ ⊢!. ↑𝔅 (σ ➝ τ) ➝ ↑𝔅 σ ➝ ↑𝔅 τ

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

• D3 : ∀ {σ : LO.FirstOrder.Sentence L}, T₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 (↑𝔅 σ)

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

• D2 : ∀ {σ τ : LO.FirstOrder.Sentence L}, T₀ ⊢!. ↑𝔅 (σ ➝ τ) ➝ ↑𝔅 σ ➝ ↑𝔅 τ
• D3 : ∀ {σ : LO.FirstOrder.Sentence L}, T₀ ⊢!. ↑𝔅 σ ➝ ↑𝔅 (↑𝔅 σ)

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

• LT : ∀ {σ : LO.FirstOrder.Sentence L}, T ⊢!. ↑𝔅 σ ➝ σ → T ⊢!. σ

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

• FLT : ∀ {σ : LO.FirstOrder.Sentence L}, T₀ ⊢!. ↑𝔅 (↑𝔅 σ ➝ σ) ➝ ↑𝔅 σ

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

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

@[reducible, inline]

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

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

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

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

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

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

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

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

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

Formalized First Incompleteness Theorem

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

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

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

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

Equations

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

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

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

@[reducible, inline]

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

Equations

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

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

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

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

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

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

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

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