Bibliography · Foundations and Logic

Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles

Article Formal Antecedent Foundations and Logic

Citation

Dan E. Willard. (2001). Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles. Journal of Symbolic Logic. 66(2). pp. 536–596.

Why this reference is included

Willard’s 2001 Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles, published in Journal of Symbolic Logic, is one of the program’s working technical references. Cited across Book I (Categorical Foundations), Part 18, Chapter The Self-Hosting Landscape; Book I (Categorical Foundations), Part 18, Chapter The Enrichment Frontier — the central framing is “Willard constructed formal arithmetic theories that can prove their own consistency”.

Cited in

  • Book I — Categorical Foundations Part 18
    Chapter The Self-Hosting Landscape
    Willard constructed formal arithmetic theories that can prove their own consistency
  • Book I — Categorical Foundations Part 18
    Chapter The Enrichment Frontier
    Precedent. Two programs have approached E_3 from different directions, each achieving it partially: Willard constructs self-verifying axiom systems — theories that prove their own consistency without violating G\"odel's second incompleteness theorem
  • Book I — Categorical Foundations Part 18
    Chapter The Enrichment Frontier
    Willard : self-verification at sub-PA strength
  • Book I — Categorical Foundations Part 18
    Chapter The Enrichment Frontier
    _0 → E_1 & Altenkirch–Kaposi 2016 ; Bocquet–Kaposi–Sattler 2023 & Non-Boolean, constructive adaptation to four-valued Ω_τ & Earned topos E_τ (I.D59) , E_1 → E_2 & Joyal arithmetic universes ; Abel graded modal DTT & Linear DTT not yet complete; no internal cut-elimination & 5 diagonal discipline; three-grade semiring , E_2 → E_3 & Willard 2001 (weak); Girard TX (fragments) & No full system at CIC-level proof-theoretic strength & *-autonomous proof theory via 5 (I.T39) , Book III proposes to attempt something that has not been done before

Bibliographic Details

BibTeX KeyWillard2001
AuthorsDan E. Willard
Year
TypeArticle
Journal / BookJournal of Symbolic Logic
Volume66(2)
Pages536--596