Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

Question

This question extends my inquiry from a previous post [0].

Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ techniques that might be described as "excluding diagonalizaton" from a given domain, while preserving other properties usually considered as concomitant with diagonalization.

Willard: "In outline, the key to Willard's construction of his system is to formalise enough of the Gödel machinery to talk about provability internally without being able to formalise diagonalisation. Diagonalisation depends upon being able to prove that multiplication is a total function (and in the earlier versions of the result, addition also). Addition and multiplication are not function symbols of Willard's language; instead, subtraction and division are, with the addition and multiplication predicates being defined in terms of these. Here, one cannot prove the PI-0-2 sentence expressing totality of multiplication:"

Brown and Palsberg: "After a careful analysis of the classical theorem, we show that static type checking in Fω can exclude the proof’s diagonalization gadget, leaving open the possibility for a self-interpreter."

Therefore: Are these techniques related?

Separate from this core question, but possibly useful for answerers, I speculate that, if so, the relation might be characterizable via a common bypassing of Lawvere's Fixed Point Theorem, which itself unifies a number of diagonalization based proofs.

[0] Is there a relationship between Brown and Palsberg's Self-Interpreter for F-Omega and Lawvere's Fixed Point Theorem?

[1] https://en.wikipedia.org/wiki/Self-verifying_theories

[2] http://compilers.cs.ucla.edu/popl16/

Answer 1

I'll defer if someone more knowledgeable on the subject arrives, but I think the answer is that they are not the same.

Willard's work is about building theories that avoid the typical formulation of the incompleteness theorem. I.E. you formalize provability as a relation $\mathsf{Prf} : ℕ → ℕ → Ω$, and consistency as something like:

$$∀(n : ℕ) → ¬\mathsf{Prf}(\ulcorner⊢ ⊥\urcorner,n)$$

So, the idea is that you have a theory with enough strength to successfully encode $\mathsf{Prf}$ and (de)coding of formulas as natural numbers, but without being able to do enough arithmetic to encode diagonalization.

However, the Brown-Palsberg idea is to reject the notion that formulas and their proofs must be uniformly coded as e.g. natural numbers. Instead, there is something more like a (meta) family of types for proofs depending on the formula, so more like:

$$\mathsf{Prf}_φ : \ulcorner φ \urcorner → Ω$$

In terms of the incompleteness theorem, this is a rejection of a hidden (in plain sight) assumption about how "consistency" must be formally stated. Diagonalization is ruled out because each type of proof cannot be applied to itself, just like how the $\sf Y$ combinator is normally ruled out in typed lambda calculi. $F_ω$ is plenty powerful to be subject to problems if you hypothesize that there is a self-interpreter whose terms are given by (Church) naturals, so that functions can apply to their own encodings and such. The point is to alter the definition of "self-interpreter" such that it no longer even makes sense to apply a function to its own encoding.

I think a closer formal logic analogue of Brown-Palsberg is The Provability of Consistency by Artemov. In that, he argues that the way of formulating "consistency" in the traditional incompleteness theorem is flawed. For instance, the practical concern is that we could actually write down false proofs, but the incompleteness theorem is requiring that this concern extends uniformly to all models of arithmetic, including ones where there are weird, infinitary naturals, and thus infinitary proofs that don't correspond to something a human could write down. So, he suggests a more realistic notion of consistency where the internal formulation varies on a case-by-case basis. The setup is not exactly the same as Brown-Palsberg, but I think the approach is similar.

I suppose it's possible in the details that the arithmetic "weakness" of Willard's theories correspond somehow to type checking ruling out self-application. However, prima facie, they seem to be different approaches.