This is mathematical section of the parent essay Gödel Incompleteness for Startups
A formal system is just a collection of axioms and rules. Just like we did before we can record axioms in plain English like “Number 0 exists”.
Can we associate axioms and rules with natural numbers? As you know everything you read on computer, is actually encoded into numbers. Inside the computer letter “N” is 78, letter “u” is 117, etc. What is word “Number” for us, is just 7811710998101114 for the computer – just one long number. Why is it that “N” is 78 and not 87, or 8787? No reason, its arbitrary arrangement, called encoding standard. That specific standard called ASCII which states that all computers who want to be ASCII-compatible must assign “N” to 78 and vise versa.
But here is an interesting part, a key to Gödel’s proof: Our axiom “Number 0 exists” is first axiom in a system that defines existence of numbers and simple arithmetic. At same time we can encode “Number 0 exists” using ASCII encoding, or any other encoding we choose and get a number that represents that axiom (or a rule) about numbers themselves. You will get something like the following:
- Number 0 exists ⇔ 7811710998101114324832101120105115116115
- Each number has a successor that is a number ⇔ 6997991043211011710998101114321049711532973211511 7999910111511511111432116104971163210511532973211 011710998101114
That number is awfully long, yet it’s still just a number. And then we do the same for rest of your initial axioms and rules. Then you can start encoding your first deductions about the formal system, deductions of deductions, etc. In the end any axiom or sequence of deductions will be just a long arithmetical number.