## Wednesday, August 27, 2014

(CW: coding exercise/study with zero higher purpose.)

In Paul Graham's 2002 essay, Revenge of the Nerds, Graham suggests one metric for the expressive power of a programming language: the ease of writing an accumulator.

[An accumulator is] a function that takes a number n, and returns a function that takes another number i and returns n incremented by i.

For example:

x = accumulator(7);
x(1); // 8
x(3); // 11
y = accumulator(-1);
y(1); // 0


In the parlance of OOP, an accumulator is a NumberIncrementerFactory. In the parlance of programming language theory, an accumulator produces a canonical example of a closure: a function together with a stateful external environment.

Graham uses the relative difficulty of writing accumulators in various languages to demonstrate the elegance/clumsiness of writing non-trivial code in them. (Of course, along with any notion of a metric comes Goodhart's law: a metric stops measuring anything useful if people start treating it as a target. If there are joke languages purpose-built to make writing quines easy, you can bet someone's written a language where there are accumulators as a language primitive.)

* Boldface mine.

## Saturday, August 9, 2014

### Knowledge out of nowhere: a note on Löb's theorem

Löb's theorem states that for any extension of Peano arithmetic, any “reasonable” intra-system definition of the term ‘provable’ and any statement $P$:

If $PA \vdash (Provable(P) \rightarrow P)$ (“$PA$ proves that (a proof of $P$ implies the truth of $P$)...”), then $PA \vdash P$ (“$PA$ proves $P$”).

Example. Let $P$ be “$0 = 1$”. Assume $PA \vdash \lnot Provable(0 = 1)$ (i.e. PA proves that there is no proof of $0 = 1$, or: $PA$ proves its own consistency.)

Then by explosion, $PA \vdash (Provable(0 = 1) \rightarrow 0 = 1)$, and by Löb's theorem, $PA \vdash 0 = 1$ (i.e. $PA$ is inconsistent). This result is Gödel's second incompleteness theorem.

There’s a stronger consequence at play from this strategy here — a consistent extension of $PA$ can’t prove the unprovability of anything within it, even what looks like blindingly obvious examples.

Consider the example of $PA_x$, which is exactly Peano arithmetic with the introduction of an additional named constant, $x$. Notably, $x$ does not appear in any of the axioms. $PA_x$ implies nothing about $x$ that it doesn’t already imply about other numbers.

Then by the same reasoning, if $PA_x \vdash \lnot Provable(x = 0)$, then $PA_x \vdash x = 0$. This conclusion is ridiculous, since from the “outside view” we can see that there should be no proof of $x = 0$ within the system. Given a model of $PA$ (such as the natural numbers), we can easily construct a model of $PA_x$ where $x \neq 0$.

Assuming the consistency of $PA_x$ (which trivially follows from the consistency of $PA$), this implies that $PA_x \not \vdash \lnot Provable(x = 0)$. But why can’t $PA_x$ prove the unprovability of the statement?