[bvirus]

I’m not a mathematician, but the ELI30 version I got was that certain logical statements are labeled by certain number, such that doing arithmetic with those numbers corresponds to basic logical operations. So true statements about the number labels equal equivalent statements about the logical statements labeled by those numbers. So like, if 1 represents some logical statement and 2 represents some logical statement, and 3 represents another, then 1+2=3 is the same as saying that the two logical statements labeled by 1 and 2, when combined, produce the logical statement labeled by 3.

This idea is called Gödel numbering, and Wikipedia says “In formal number theory a Gödel numbering is a function which assigns to each symbol and formula of some formal language a unique natural number called a Gödel number (GN). ... A Gödel numbering can be interpreted as an encoding where a number is assigned to each symbol of a mathematical notation, and a stream of natural numbers can then represent some form or function.” That seems to sort of gel with what I heard, although it implies that maybe arthimetic operations like +, or -, aren’t actually involved. It might be more like 1 is a statement, and 2 is a statement, such that 12 is a combination of those two statements.

The point is that then you encode “this statement is not proveable” into numbers and show that you get a numerical contradiction (like 1=3 or something).