<p>I'll defer if someone more knowledgeable on the subject arrives, but I think the answer is that they are <em>not</em> the same.</p>
<p>Willard's work is about building theories that avoid the typical formulation of the incompleteness theorem. I.E. you formalize provability as a relation <span class="math-container">$\mathsf{Prf} : ℕ → ℕ → Ω$</span>, and consistency as something like:</p>
<p><span class="math-container">$$∀(n : ℕ) → ¬\mathsf{Prf}(\ulcorner⊢ ⊥\urcorner,n)$$</span></p>
<p>So, the idea is that you have a theory with enough strength to successfully encode <span class="math-container">$\mathsf{Prf}$</span> and (de)coding of formulas as natural numbers, but without being able to do enough arithmetic to encode diagonalization.</p>
<p>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:</p>
<p><span class="math-container">$$\mathsf{Prf}_φ : \ulcorner φ \urcorner → Ω$$</span></p>
<p>In terms of the incompleteness theorem, this is a rejection of a hidden (in plain sight) assumption about <em>how</em> &quot;consistency&quot; must be formally stated. Diagonalization is ruled out because each type of proof cannot be applied to itself, just like how the <span class="math-container">$\sf Y$</span> combinator is normally ruled out in typed lambda calculi. <span class="math-container">$F_ω$</span> 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 &quot;self-interpreter&quot; such that it no longer even makes sense to apply a function to its own encoding.</p>
<p>I think a closer formal logic analogue of Brown-Palsberg is <a href="https://arxiv.org/abs/1902.07404" rel="nofollow noreferrer">The Provability of Consistency</a> by Artemov. In that, he argues that the <em>way</em> of formulating &quot;consistency&quot; in the traditional incompleteness theorem is flawed. For instance, the practical concern is that we could <em>actually</em> write down false proofs, but the incompleteness theorem is requiring that this concern extends uniformly to <em>all</em> 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.</p>
<p>I suppose it's possible in the details that the arithmetic &quot;weakness&quot; of Willard's theories correspond somehow to type checking ruling out self-application. However, prima facie, they seem to be different approaches.</p>

CC BY-SA 4.0
2022-06-21T16:09:52.903Z
Nice find with that Artemov paper!
cody
CC BY-SA 4.0
2022-06-20T18:48:12.620Z
2022-06-20T18:48:12.620Z
Dan Doel
<p>This question extends my inquiry from a previous post [0].</p>
<p>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 &quot;excluding diagonalizaton&quot; from a given domain, while preserving other properties usually considered as concomitant with diagonalization.</p>
<p>Willard:
&quot;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:&quot;</p>
<p>Brown and Palsberg:
&quot;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.&quot;</p>
<p>Therefore: Are these techniques related?</p>
<p>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.</p>
<p>[0] <a href="https://cstheory.stackexchange.com/questions/51579/is-there-a-relationship-between-brown-and-palsbergs-self-interpreter-for-f-omeg">Is there a relationship between Brown and Palsberg&#39;s Self-Interpreter for F-Omega and Lawvere&#39;s Fixed Point Theorem?</a></p>
<p>[1] <a href="https://en.wikipedia.org/wiki/Self-verifying_theories" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Self-verifying_theories</a></p>
<p>[2] <a href="http://compilers.cs.ucla.edu/popl16/" rel="nofollow noreferrer">http://compilers.cs.ucla.edu/popl16/</a></p>

CC BY-SA 4.0
2022-06-26T22:36:38.073Z
As soon as we have basic arithmetic (Robinson's Q), we can start using natural numbers to encode and express things. Once there, incompleteness follows. Willard's theory are not strong enough to allow encoding trick to work.
Kaveh
CC BY-SA 4.0
2022-06-26T22:42:26.663Z
The Artemov's trick on the other hand, iiuc, is using non-unformity. It is, imo, not that different from proving soundness of each level of arithmetic hierarchy by induction over formula one level up. PA can prove soundness of any proof using only $\Sigma_k$ formulas (for any fixed value of k). Or even simpler consider theory made up of PA + axioms each stating all the axioms before it are consistent.
Kaveh
<pl.programming-languages><ct.category-theory><proof-complexity><proof-theory><fixed-points>
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
jpt4
# Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

(Asked by: username_0 on 2022-06-11)

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?](https://cstheory.stackexchange.com/questions/51579/is-there-a-relationship-between-brown-and-palsbergs-self-interpreter-for-f-omeg)

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

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

**Tags:** pl.programming-languages, ct.category-theory, proof-complexity, proof-theory, fixed-points

> **Comments:**
> **username_1**: As soon as we have basic arithmetic (Robinson's Q), we can start using natural numbers to encode and express things. Once there, incompleteness follows. Willard's theory are not strong enough to allow encoding trick to work.  
> **username_1**: The Artemov's trick on the other hand, iiuc, is using non-unformity. It is, imo, not that different from proving soundness of each level of arithmetic hierarchy by induction over formula one level up. PA can prove soundness of any proof using only $\Sigma_k$ formulas (for any fixed value of k). Or even simpler consider theory made up of PA + axioms each stating all the axioms before it are consistent.  

---

## 1 answers

### Answer by username_2 on 2022-06-20. Score: 4 | Accepted answer

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](https://arxiv.org/abs/1902.07404) 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.

> **Comments:**
> **username_3**: Nice find with that Artemov paper!  

---

