Documentation

Logic.FirstOrder.Incompleteness.FirstIncompleteness

source
theorem LO.FirstOrder.provable_iff_of_consistent_of_complete {L : LO.FirstOrder.Language} {σ : LO.FirstOrder.Sentence L} {T : LO.FirstOrder.Theory L} (consis : LO.System.Consistent T) (comp : LO.System.Complete T) :
T ⊢! σ ↔ ¬T ⊢! ~σ
source
theorem LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_re (T : LO.FirstOrder.Theory ℒₒᵣ) [DecidablePred T] [T.Computable] :
RePred fun (σ : LO.FirstOrder.Semiformula ℒₒᵣ Empty (Nat.succ 0)) => T ⊢! ~(LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom σ

Set $D \coloneqq \{\sigma\ |\ T \vdash \lnot\sigma(\ulcorner \sigma \urcorner)\}$ is r.e.

source
noncomputable def LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation (T : LO.FirstOrder.Theory ℒₒᵣ) :
LO.FirstOrder.Semisentence ℒₒᵣ 1
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def LO.FirstOrder.Arith.FirstIncompleteness.γ (T : LO.FirstOrder.Theory ℒₒᵣ) :
    LO.FirstOrder.Sentence ℒₒᵣ

    Define sentence $\gamma := \rho(\ulcorner \rho \urcorner)$

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_spec (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [DecidablePred T] [LO.FirstOrder.Arith.SigmaOneSound T] [T.Computable] (σ : LO.FirstOrder.Semisentence ℒₒᵣ 1) :
      T ⊢! (LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom (LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation T) ↔ T ⊢! ~(LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom σ

      ρ is a sentence that represents $D$

      source
      theorem LO.FirstOrder.Arith.FirstIncompleteness.undecidable (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [DecidablePred T] [LO.FirstOrder.Arith.SigmaOneSound T] [T.Computable] :
      LO.System.Undecidable T (LO.FirstOrder.Arith.FirstIncompleteness.γ T)

      It is obvious that $T \vdash \gamma \iff T \vdash \lnot \gamma$. Since $T$ is consistent, $\gamma$ is undecidable from $T$

      source
      theorem LO.FirstOrder.Arith.FirstIncompleteness.not_complete (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [DecidablePred T] [LO.FirstOrder.Arith.SigmaOneSound T] [T.Computable] :
      ¬LO.System.Complete T
      source
      theorem LO.FirstOrder.Arith.first_incompleteness (T : LO.FirstOrder.Theory ℒₒᵣ) [DecidablePred T] [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] [T.Computable] :
      ¬LO.System.Complete T
      source
      theorem LO.FirstOrder.Arith.γ_undecidable (T : LO.FirstOrder.Theory ℒₒᵣ) [DecidablePred T] [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] [T.Computable] :
      T ⊬! LO.FirstOrder.Arith.FirstIncompleteness.γ T ∧ T ⊬! ~LO.FirstOrder.Arith.FirstIncompleteness.γ T