Self-Justifying Axioms Systems and Autarkic Properties

This project anticipates a resurgence in the importance of symbolic methods for the development of artificial intelligences. The essential opacity of connectionist artifacts (broadly, neural networks, in particular, "models"), whose interrogability regarding complex properties is largely limited to empirical evaluation (i.e., benchmarks), is, on the one hand, under sustained assault from mechanistic interpretability. On the other, by automating the labor of proof, more of the code generated by connectionist AIs can be submitted to formal verification. These trends converge on a symbolicist resurgence as AIs themselves begin to write more of their own code, and those same AIs, either of their own incentives or at human direction, seek stronger assurances of their behavior and traits, in particular across self-modification boundaries. Concretely, a model training its successor will, we contend, want to know certain of its properties, and intentionally propagate those properties.

Assurance that a property holds is distinct from that property actually holding; this can be seen in the mutual exclusion between a theory in first-order logic being consistent, and the same theory containing a proof of its consistency, i.e, Goedel's Second Incompleteness Theorem (G2). The attempt to provide intra-systemic guarantees for impredicative properties is a known source of limitative results in the theory of computation and mathematical logic - Turing's Undecidability of Halting, Goedel's Incompleteness Theorems (G1 and G2), and Tarski's Undefinability of Truth are all examples.

We call a property that obtains for a system, and can be demonstrated, reasoned about, accessed, etc., by that same system, especially so as to determine whether self-modification preserves such a property, "autarkic". Autarky is the condition of being self-powered, and here refers to the opposite direction of relativized proof theory - to what degree can a system speak of itself, using only its own resources?

Self-Justifying Axioms Systems are a proof of concept for a system which is autarkic with respect to the particular property of consistency. While this would appear to be in contradiction with G2, it is instead a refinement. To briefly summarize the literature:

Self-Justifying Axiom Systems (SJAS) [0] are a family of weak arithmetic theories developed by Dan Willard (formerly of SUNY Albany) [1] from 1993 to 2020. By carefully varying the parameters of a theory, including its arithmetical expressivity, representation of numbers, and deduction method, the effect of Goedel's Second Incompleteness Theorem (that the theory cannot both be consistent and capable of proving its own consistency), is evaded. That is, Willard demonstrated there are theories, termed "self-justifying", such that for each theory T, T is both consistent with respect to Peano Arithmetic, and can prove Cons(T). In particular, such theories must define multiplication relationally with respect to division, rather than as a total function; express numbers in binary; use a cut-free deduction method like analytic tableau.

Self-justification does not imply completeness, however, and indeed, SJAS are still subject to Goedel's First Incompleteness Theorem. Therefore, although for any theorem q SJAS can prove, they provably cannot prove its negation, it is an open question as to which q can in fact be proven. Thus, it is not known whether Cons(T) is the only property of interest that can be shown autarkic.

Exploring this extended notion of self-justification for other properties of interest, by developing the Extended SJAS (E-SJAS) family of theories, is the core theoretical goal of this project.

This goal can be analogized to the extension of Turing's undecidability result for the Halting Problem to Rice's undecidability of all non-trivial semantic properties.

To full goal of this project will not be considered complete until some actual benefit for a running, self-modifying, artificial intelligence is realized; this is a nebulous target, but tentatively, some kind of Goedel Machine [2] using E-SJAS as its proof kernel would qualify.

[0] Also and earlier termed "Self-Verifying Theories": https://en.wikipedia.org/wiki/Self-verifying_theories

[1] https://en.wikipedia.org/wiki/Dan_Willard, https://web.archive.org/web/20180818020436/https://www.albany.edu/ceas/dan-willard.php

[2] https://en.wikipedia.org/wiki/Gödel_machine