instance LO.FirstOrder.Theory.Alt.instSubtheorySyntacticFormulaThyAlt_incompleteness {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {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 : LO.FirstOrder.Theory L} {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₀ : LO.FirstOrder.Theory L) (T : LO.FirstOrder.Theory L) : Type u_1

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

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.spec {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} (self : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T) {σ : LO.FirstOrder.Sentence L} : T ⊢!. σ → T₀ ⊢!. (LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom self.prov

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

Equations

• 𝔅.pr σ = (LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom 𝔅.prov

instance LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.instCoeFunForallSentence {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {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₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} (𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T) : LO.FirstOrder.Sentence L

Equations

• 𝔅.con = ∼𝔅.pr ⊥

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.Rew.substs ![⌜LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T θ⌝]).hom θ

theorem LO.FirstOrder.DerivabilityCondition.Diagonalization.diag {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {T : LO.FirstOrder.Theory L} [self : LO.FirstOrder.DerivabilityCondition.Diagonalization T] (θ : LO.FirstOrder.Semisentence L 1) : T ⊢!. LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T θ ⭤ (LO.FirstOrder.Rew.substs ![⌜LO.FirstOrder.DerivabilityCondition.Diagonalization.fixpoint T θ⌝]).hom θ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

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

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

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₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} {σ : LO.FirstOrder.Sentence L} : T ⊢!. σ → T ⊢!. 𝔅.pr σ

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Equations

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

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

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

• γ_sound : T ⊢!. 𝔅.pr (LO.FirstOrder.DerivabilityCondition.goedel T₀ T 𝔅) → T ⊢!. LO.FirstOrder.DerivabilityCondition.goedel T₀ T 𝔅

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.GoedelSound.γ_sound {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [self : 𝔅.GoedelSound] : T ⊢!. 𝔅.pr (LO.FirstOrder.DerivabilityCondition.goedel T₀ T 𝔅) → T ⊢!. LO.FirstOrder.DerivabilityCondition.goedel T₀ T 𝔅

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

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

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

theorem LO.FirstOrder.DerivabilityCondition.first_incompleteness {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] [DecidableEq (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [LO.System.Consistent T] [𝔅.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)] [DecidableEq (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} {σ : LO.FirstOrder.Sentence L} [𝔅.HBL] : T₀ ⊢!. ∼𝔅.pr σ ➝ 𝔅.con

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

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)] [DecidableEq (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [𝔅.HBL] : T ⊢!. LO.FirstOrder.DerivabilityCondition.goedel T₀ T 𝔅 ⭤ 𝔅.con

theorem LO.FirstOrder.DerivabilityCondition.unprovable_consistency {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] [DecidableEq (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [𝔅.HBL] [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)] [DecidableEq (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [𝔅.HBL] [LO.System.Consistent T] [𝔅.GoedelSound] : T ⊬. ∼𝔅.con

def LO.FirstOrder.DerivabilityCondition.kreisel {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] (T₀ : LO.FirstOrder.Theory L) (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

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• LO.FirstOrder.DerivabilityCondition.instLoebOfHBL = { LT := ⋯ }

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

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

Equations

• LO.FirstOrder.DerivabilityCondition.instFormalizedLoebOfHBL = { FLT := ⋯ }

theorem LO.FirstOrder.DerivabilityCondition.unprovable_consistency_via_loeb {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {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)] [DecidableEq (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [LO.System.Consistent T] [𝔅.HBL] [𝔅.GoedelSound] : T ⊬. 𝔅.con ➝ ∼𝔅.pr (∼𝔅.con)

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

@[reducible, inline]

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

Equations

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

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

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

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

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

theorem LO.FirstOrder.DerivabilityCondition.rosser_first_incompleteness {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [LO.System.Consistent 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₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T₀ T} [𝔅.Rosser] : T ⊢!. 𝔅.con

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