‘Sweet’ little gem that breaks standard analysis

I came across this gorgeous chap in a paper (Paul Taylor, A lambda calculus for real analysis, <http://paultaylor.eu/ASD/lamcra/>).

We set s=∑2-ngn, where gn={1if n encodes a proof that 0⊢10otherwise.

The example in the paper is applied to various examples as Taylor shows how many everyday maths proofs rely on the decidability of questions like ‘Is a=b?’, while the above shows that this cannot be taken be for granted (‘Is s=0’ asks Gödel’s infamous proof).