Documentation

Logic.FirstOrder.Incompleteness.SelfReference

source
noncomputable def LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.ssbs :
LO.FirstOrder.Semisentence ℒₒᵣ 3
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.ssbs_spec {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] (σ : LO.FirstOrder.Semisentence ℒₒᵣ 1) (π : LO.FirstOrder.Semisentence ℒₒᵣ 1) :
    T ⊢! (“∀' (!((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0, ⌜σ⌝, ⌜π⌝]).hom LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.ssbs) ↔ !!(LO.FirstOrder.Semiterm.bvar 0) = !!⌜(LO.FirstOrder.Rew.substs ![⌜π⌝]).hom σ⌝)”)
    source
    noncomputable def LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.diag (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) :
    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.SelfReference.fixpoint (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) :
      LO.FirstOrder.Sentence ℒₒᵣ
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.substs_diag (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) (σ : LO.FirstOrder.Semisentence ℒₒᵣ 1) :
        (LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom (LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.diag θ) = ∀' ((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0, ⌜σ⌝, ⌜σ⌝]).hom LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.ssbs ⟶ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom θ)
        source
        theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.fixpoint_eq (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) :
        LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.fixpoint θ = ∀' ((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0, ⌜LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.diag θ⌝, ⌜LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.diag θ⌝]).hom LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.ssbs ⟶ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom θ)
        source
        theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.main (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) :
        T ⊢! LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.fixpoint θ ⟷ (LO.FirstOrder.Rew.substs ![⌜LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.fixpoint θ⌝]).hom θ

        Fixpoint Lemma

        source
        noncomputable def LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.provableSentence {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] (U : LO.FirstOrder.Theory L) :
        LO.FirstOrder.Semisentence ℒₒᵣ 1
        Equations
        Instances For
          source
          theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.provableSentence_representation {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] {U : LO.FirstOrder.Theory L} [DecidablePred U] [U.Computable] {σ : LO.FirstOrder.Sentence L} :
          T ⊢! (LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom (LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.provableSentence U) ↔ U ⊢! σ
          source
          noncomputable def LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.goedel (T : LO.FirstOrder.Theory ℒₒᵣ) :
          LO.FirstOrder.Sentence ℒₒᵣ

          Gödel Sentence $G$

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.goedel_spec (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] :
            T ⊢! LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.goedel T ⟷ ~(LO.FirstOrder.Rew.substs ![⌜LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.goedel T⌝]).hom (LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.provableSentence T)
            source
            theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] [DecidablePred T] [T.Computable] :
            LO.System.Undecidable T (LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.goedel T)
            source
            theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.incomplete (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] [DecidablePred T] [T.Computable] :
            ¬LO.System.Complete T
            source
            theorem LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.not_disjunctive (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] [𝐏𝐀⁻ ≼ T] [LO.FirstOrder.Arith.SigmaOneSound T] [DecidablePred T] [T.Computable] :
            ¬LO.System.Disjunctive T