structure LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate (L₀ : LO.FirstOrder.Language) (L : LO.FirstOrder.Language) : Type u_1

• prov : LO.FirstOrder.Semisentence L₀ 1

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.pr {L₀ : LO.FirstOrder.Language} {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L₀ (LO.FirstOrder.Sentence L)] {n : ℕ} (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L₀ L) (σ : LO.FirstOrder.Sentence L) : LO.FirstOrder.Semisentence L₀ n

Equations

• ⦍β⦎σ = (LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom β.prov

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.«term⦍_⦎_» : Lean.ParserDescr

Equations

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

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 θ

def LO.FirstOrder.DerivabilityCondition.consistency {L₀ : LO.FirstOrder.Language} {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L₀ (LO.FirstOrder.Sentence L)] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L₀ L) : LO.FirstOrder.Sentence L₀

Equations

• Con⦍β⦎ = ~⦍β⦎⊥

def LO.FirstOrder.DerivabilityCondition.«termCon⦍_⦎» : Lean.ParserDescr

Equations

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

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

• iff : ∀ (σ : LO.FirstOrder.Sentence L), T ⊢! σ ↔ T₀ ⊢! ⦍β⦎σ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Conservative.iff {L₀ : LO.FirstOrder.Language} {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L₀ (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L₀ L} {T₀ : LO.FirstOrder.Theory L₀} {T : outParam (LO.FirstOrder.Theory L)} [self : β.Conservative T₀ T] (σ : LO.FirstOrder.Sentence L) : T ⊢! σ ↔ T₀ ⊢! ⦍β⦎σ

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

• D1 : ∀ {σ : LO.FirstOrder.Sentence L}, T ⊢! σ → T₀ ⊢! ⦍β⦎σ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL1.D1 {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.HBL1 T₀ T] {σ : LO.FirstOrder.Sentence L} : T ⊢! σ → T₀ ⊢! ⦍β⦎σ

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

• D2 : ∀ {σ τ : LO.FirstOrder.Sentence L}, T₀ ⊢! ⦍β⦎(σ ⟶ τ) ⟶ ⦍β⦎σ ⟶ ⦍β⦎τ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL2.D2 {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.HBL2 T₀ T] {σ : LO.FirstOrder.Sentence L} {τ : 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)] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) (T₀ : LO.FirstOrder.Theory L) (T : outParam (LO.FirstOrder.Theory L)) : Type

• D3 : ∀ {σ : LO.FirstOrder.Sentence L}, T₀ ⊢! ⦍β⦎σ ⟶ ⦍β⦎⦍β⦎σ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL3.D3 {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.HBL3 T₀ T] {σ : 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)] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) (T₀ : LO.FirstOrder.Theory L) (T : outParam (LO.FirstOrder.Theory L)) extends LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL1 , 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)] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) (T₀ : LO.FirstOrder.Theory L) (T : outParam (LO.FirstOrder.Theory L)) : Type

• LT : ∀ {σ : LO.FirstOrder.Sentence L}, T ⊢! ⦍β⦎σ ⟶ σ → T ⊢! σ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Loeb.LT {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} (T₀ : LO.FirstOrder.Theory L) {T : outParam (LO.FirstOrder.Theory L)} [self : β.Loeb T₀ T] {σ : 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)] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) (T₀ : LO.FirstOrder.Theory L) (T : outParam (LO.FirstOrder.Theory L)) : Type

• FLT : ∀ {σ : LO.FirstOrder.Sentence L}, T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.FormalizedLoeb.FLT {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.FormalizedLoeb T₀ T] {σ : 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)] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) (T₀ : LO.FirstOrder.Theory L) (T : outParam (LO.FirstOrder.Theory L)) : Type

• Ro : ∀ {σ : LO.FirstOrder.Sentence L}, T ⊢! ~σ → T₀ ⊢! ~⦍β⦎σ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.Rosser.Ro {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.Rosser T₀ T] {σ : LO.FirstOrder.Sentence L} : T ⊢! ~σ → T₀ ⊢! ~⦍β⦎σ

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D1 {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.HBL1 T₀ T] {σ : LO.FirstOrder.Sentence L} : T ⊢! σ → T₀ ⊢! ⦍β⦎σ

Alias of LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.HBL1.D1.

theorem LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2 {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.HBL2 T₀ T] {σ : LO.FirstOrder.Sentence L} {τ : LO.FirstOrder.Sentence L} : T₀ ⊢! ⦍β⦎(σ ⟶ τ) ⟶ ⦍β⦎σ ⟶ ⦍β⦎τ

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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.HBL3 T₀ T] {σ : LO.FirstOrder.Sentence L} : T₀ ⊢! ⦍β⦎σ ⟶ ⦍β⦎⦍β⦎σ

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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} (T₀ : LO.FirstOrder.Theory L) {T : outParam (LO.FirstOrder.Theory L)} [self : β.Loeb T₀ T] {σ : LO.FirstOrder.Sentence L} : T ⊢! ⦍β⦎σ ⟶ σ → 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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.FormalizedLoeb T₀ T] {σ : LO.FirstOrder.Sentence L} : T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ

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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : outParam (LO.FirstOrder.Theory L)} [self : β.Rosser T₀ T] {σ : LO.FirstOrder.Sentence L} : T ⊢! ~σ → T₀ ⊢! ~⦍β⦎σ

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

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D1s {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] {σ : LO.FirstOrder.Sentence L} [β.HBL1 T₀ T] : T ⊢! σ → T ⊢! ⦍β⦎σ

Equations

• ⋯ = ⋯

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2s {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] {σ : LO.FirstOrder.Sentence L} {τ : LO.FirstOrder.Sentence L} [β.HBL2 T₀ T] : T ⊢! ⦍β⦎(σ ⟶ τ) ⟶ ⦍β⦎σ ⟶ ⦍β⦎τ

Equations

• ⋯ = ⋯

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D2' {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} {σ : LO.FirstOrder.Sentence L} {τ : LO.FirstOrder.Sentence L} [β.HBL T₀ T] [LO.System.ModusPonens T] : T₀ ⊢! ⦍β⦎(σ ⟶ τ) → T₀ ⊢! ⦍β⦎σ ⟶ ⦍β⦎τ

Equations

• ⋯ = ⋯

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.D3s {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] {σ : LO.FirstOrder.Sentence L} [β.HBL3 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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [β.HBL T₀ T] {σ : LO.FirstOrder.Sentence L} {τ : 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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [β.HBL T₀ T] {σ : LO.FirstOrder.Sentence L} {τ : LO.FirstOrder.Sentence L} (h : T ⊢! σ ⟷ τ) : T₀ ⊢! ⦍β⦎σ ⟷ ⦍β⦎τ

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate.prov_distribute_and! {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [β.HBL T₀ T] {σ : LO.FirstOrder.Sentence L} {τ : 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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [β.HBL T₀ T] {σ : LO.FirstOrder.Sentence L} {τ : LO.FirstOrder.Sentence L} : T₀ ⊢! ⦍β⦎σ ⋏ ⦍β⦎τ ⟶ ⦍β⦎(σ ⋏ τ)

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 L L) [β.HBL1 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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL1 T₀ T] : T₀ ⊢! LO.FirstOrder.DerivabilityCondition.goedel T₀ T β ⟷ ~⦍β⦎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)] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) (T₀ : LO.FirstOrder.Theory L) (T : LO.FirstOrder.Theory L) [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL1 T₀ T] : Type

• γ_sound : T ⊢! ⦍β⦎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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL1 T₀ T] [self : β.GoedelSound T₀ T] : T ⊢! ⦍β⦎LO.FirstOrder.DerivabilityCondition.goedel T₀ T β → T ⊢! LO.FirstOrder.DerivabilityCondition.goedel T₀ T β

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

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

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

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

theorem LO.FirstOrder.DerivabilityCondition.formalized_consistent_of_existance_unprovable {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} {σ : LO.FirstOrder.Sentence L} [β.HBL T₀ T] : T₀ ⊢! ~⦍β⦎σ ⟶ Con⦍β⦎

theorem LO.FirstOrder.DerivabilityCondition.formalized_unprovable_goedel {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL T₀ T] : T ⊢! Con⦍β⦎ ⟶ ~⦍β⦎LO.FirstOrder.DerivabilityCondition.goedel T₀ T β

Formalized First Incompleteness Theorem

theorem LO.FirstOrder.DerivabilityCondition.iff_goedel_consistency {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL T₀ T] : T ⊢! LO.FirstOrder.DerivabilityCondition.goedel T₀ T β ⟷ Con⦍β⦎

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

theorem LO.FirstOrder.DerivabilityCondition.unrefutable_consistency {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL T₀ T] [LO.System.Consistent T] [β.GoedelSound T₀ T] : 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 L L) [β.HBL T₀ T] (σ : 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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL T₀ T] (σ : LO.FirstOrder.Sentence L) : T₀ ⊢! LO.FirstOrder.DerivabilityCondition.kreisel T₀ T β σ ⟷ (⦍β⦎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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] {σ : LO.FirstOrder.Sentence L} [β.HBL T₀ T] (H : T ⊢! ⦍β⦎σ ⟶ σ) : T ⊢! σ

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

Equations

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

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

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

Equations

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

theorem LO.FirstOrder.DerivabilityCondition.unprovable_consistency_via_loeb {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [LO.System.Consistent T] [β.Loeb T₀ T] : T ⊬! Con⦍β⦎

theorem LO.FirstOrder.DerivabilityCondition.formalized_unprovable_not_consistency {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [LO.System.Consistent T] [β.HBL T₀ T] [β.GoedelSound T₀ T] : T ⊬! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎)

theorem LO.FirstOrder.DerivabilityCondition.formalized_unrefutable_goedel {L : LO.FirstOrder.Language} [DecidableEq (LO.FirstOrder.Sentence L)] [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [LO.System.Consistent T] [β.HBL T₀ T] [β.GoedelSound T₀ T] : T ⊬! Con⦍β⦎ ⟶ ~⦍β⦎(~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 L L) [β.HBL1 T₀ T] [β.Rosser T₀ T] : 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)] {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {T₀ : LO.FirstOrder.Theory L} {T : LO.FirstOrder.Theory L} [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] [β.HBL1 T₀ T] [β.Rosser T₀ T] : T₀ ⊢! LO.FirstOrder.DerivabilityCondition.rosser T₀ T β ⟷ ~⦍β⦎LO.FirstOrder.DerivabilityCondition.rosser T₀ T β

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

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

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

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

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

If β satisfies Rosser provability condition, then Con⦍β⦎ is provable in T.