[Concerning A Project from the List: https://jpt401.substack.com/p/project-list]
As a research programme, Autarkic Formal Systems (AFS) asks, broadly: To what extent are the aspects of a formal system determined by its own powers? This intentionally encompasses a wide range of objects, properties, and behaviors of interest; in my presentation to the Indiana University Logic Seminar [0], I closed with a few examples:
- Consistency (of logical theories)
Self-Justifying Axiom Systems
- Definability (of sets, paradigmatically true sentences of arithmetic)
- Decidability (of program behavior)
- Interpretation (of programming languages)
Brown and Palsberg, self-interpretation in System F-Omega
- Replication (of structures)
Von Neumann automata
In many cases, a subject of inquiry in AFS is found by considering a limitative result, and exploring the criteria under which that result holds; I consider the development SJAS to be paradigmatic of this protocol, and so, for this and other reasons, personally prioritize investigation into AFS via SJAS. Two active lines of inquiry are:
1) As a practical matter, what, if any, is the equivalent of the Curry-Howard Correspondence for SJAS? Subordinate to this, how might a computationally executable instance (either as a program or programming language) of an SJAS be implemented? What effects do the logical properties of an SJAS have on its computational counterpart? In particular, do different evaluation methods (e.g., if implemented in/as a logic programming language, different proof search algorithms) affect the preservation of such effects in the translation from the logical to computational domains?
To compare, there already exists a system of relational arithmetic in the pure relational logic programming language miniKanren, which could be tailored to match the weak arithmetic of an SJAS, but the proof search method of mk is different from that of the deduction methods used to demonstrate the presence/absence of self-justification.
2) From the theoretical perspective, analyzing Willard's results in light of the Lawvere-Yanofsky "generalized diagonalization" framework [1], and determining whether/how this framework can be used to explain the inadmissibility of diagonalization within an SJAS; in turn, whether/how the method by which an SJAS avoids diagonalization can be reciprocally generalized, for potential application to other limitative theorems that follow from Lawvere-Yanofsky.
Further questions regarding epistemically secure self-modifying cognitive entities, the certification of kernels for towers of proof systems, and other matters of generalized bootstrapping, also fall within the purview of AFS; it is sympathetic to the motivations of Jean-Yves Girard's Transcendental Syntax.
To address a partial name collision: Hank Barendregt's "Autarkic Computations" research [2] concerns the efficient, auditable incorporation into computerized proof systems of statements that may require large derivations to directly justify. By 1) providing the means to prove metamathematical results, and 2) allow for structure sharing across proofs (proof objects constructed by reference to previously proven statements), these derivations can be reduced in size until they are feasible, in an ergonomic sense, for a mathematician to be confident in their correctness. This work is interesting, and has tendrils of connection to AFS, but is not predicated on AFS, nor vice-versa.
Currently, the Self-Justifying Axiom Systems and Pervasively Reconfigurable Computing (PRC) git repositories [3] [4] contain those publicly available artifacts related to Autarkic Formal Systems; however, these will very likely be re-organized with respect to a new, dedicated AFS repository [5].
[0] Disrupted, alas, by the large scale Zoom outage that day, and so recommenced partway through the allocated time; that recording is available here: https://iu.mediaspace.kaltura.com/media/t/1_1bopykdb
A revised version of the talk will likely be given at a future date.
[1] Yanofsky, N., 2003, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points, https://arxiv.org/abs/math/0305282
[2] Barendregt, H., Barendsen, E., 1999, Autarkic Computations in Formal Proofs, https://link.springer.com/content/pdf/10.1023/a:1015761529444.pdf
[3] https://github.com/jpt4/sjas
[4] https://github.com/jpt4/prc
[5] https://github.com/jpt4/afs
