I intend to collate, cross-reference, and synthesize Professor Dan E. Willard's 30 years of publications on Self-Justifying Axiom Systems (SJAS) into a single, unified presentation.
Context: Goedel's Incompleteness Theorems are the paradigmatic limitative results in mathematical logic, defining the trade-off between expressivity (what statements can a logic produce) and self-certainty (what guarantees of correctness can a logic make about its own statements) that formal systems encounter as they increase in expressive power. Colloquially, the 2nd Incompleteness Theorem is taken to show that any formal system capable of expressing at least basic arithmetic is subject to very strong restrictions on its capacity for self-certainty: it cannot prove its own consistency, using the resources available within its system itself.
However, the full nature of this trade-off, and the criteria for its applicability, is nuanced, and more complex than its classic presentation. Prof. Willard has conducted ground-breaking work in this area, by devising a family of formal systems that explore the subtle boundary between logics subject to Goedel's 2nd Incompleteness Theorem, and those which are not. In doing so, he hints at deep connections between computation and proof theory, along dimensions not directly addressed by any other researcher.
Willard's work, though published in various reputable venues like the Journal of Symbolic Logic, has been entirely single-authored, and he has not taken on graduate students to continue his research programme. With his retirement from SUNY Albany three years ago, and advancing age, there is a risk his work will become lost to history.
I have been independently studying Willard's work for several years, and believe I can produce an authoritative treatment of his extant publications, to disseminate to other professionals within and beyond his focus area of mathematical logic. This would preserve an important body of academic work, and increase its visibility to others who might build upon it.
References:
https://en.wikipedia.org/wiki/Self-verifying_theories
https://web.archive.org/web/20180818020436/https://www.albany.edu/ceas/dan-willard.php
https://web.archive.org/web/20130915104548/http://www.cs.albany.edu/FacultyStaff/profiles/willard.htm
https://arxiv.org/search/?query=dan+willard&searchtype=all&source=header
What is your track record on similar projects?
Nonexistent. If funded, this will be my first externally supported academic project. I am an independent enthusiast of the field, and believe I have spent more time investigating Willard's work than all but a few professionals. I have also spoken and corresponded with Willard repeatedly, and visited him in person, in my pursuit to understand the full scope and context of his research.
References:
https://www.twitter.com/jpt401
https://www.github.com/jpt4
How will you spend your funding?
On travel, to co-ordinate key elements of the project with Willard in person. Due to Prof. Willard's age and health concerns, it is difficult to engage him in long form technical communication remotely. In the course of preparing an annotated edition of his many papers, it will be crucial to access his manuscripts, draft versions of articles, and his own memory. Having visited him once, I believe I know how to structure further in-person meetings to maximize their utilty for the project.