I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?

 It is not about systems that can "do" basic arithmetic but that can "talk about" basic arithmetic.The mere execution of basic arithmetic does not require the capability of manipulating propositions of basic arithmetic.Doing basic arithmetic:12 * ( 5 + 8 ) --> 12 * 13 --> 156Talking about basic arithmetic:a * ( b + c ) == a * b + a * cThe formal language needed to describe basic arithmetic is much more powerful than a simple execution engine, such as a stack engine, that can merely carry out basic arithmetic.For example, I must be able to express that for all natural numbers x and y, if x = y, then y = x. The result could look like this:∀ x,y ∈ N: x=y ⇔ y=xHence, this language must be able to express all Dedekind-Peano's axioms as well as every proposition provable from these axioms, along with their formal proofs.In that sense, the Gödel numbering system is the "bytecode" of quite a serious programming (or at least, specification) language. (https://en.wikipedia.org/wiki/G%C3%B6del_numbering)
 It should be noted that the special sauce that makes arithmetic really difficult is induction.Induction isn't just reasoning about computation, (i.e simple equations). Instead it is reasoning about reasoning about equations (i.e. reasoning about all equations).Specifically we have: this formula https://wikimedia.org/api/rest_v1/media/math/render/svg/67e2...
 But it should be pointed out that induction is essentially unrelated to Gödel's theorem.For example, Robinson Arithmetic is a finitely axiomatized theory whose axioms contain only one existential quantifier, but just like full (Peano) arithmetic, it is subject to Gödel's incompleteness theorems.
 Wow, I thought it was required to have second order logic for godel to apply, but this seems to be a first order logic that is still undecidable.
 From the other side of the fence, another thing to look at would be the decidability of presburger, and skolem arithmetic, the following paper then goes over the extensions of these, which render the result undecidable. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.21...
 Thanks for the answer! Out of curiosity what about systems we can prove able to "do" basic arithmetic, ignoring whether they can talk about it?I'm imagining the difference between a system that can show "P(n)" for any n, rather than a system that can show "P(n) for any n."It seems like the former must come with a proof about the system. The quantifiers "for any n" have to come somewhere. If they aren't embedded within the system, do we still end up with a system that must be able to express "This sentence is not provable?"
 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).
 Nowadays it's pretty simple:1. Encode the propositions of your formal system in ascii (or whatever encoding you like)2. Observe that the resulting bit patterns can be interpreted as numbers, and so the rules of inference of your formal system can be expressed as mathematical operations on those numbers3. ProfitGoedel had to invent all of that from scratch. On top of that, he had to describe how to actually carry out step 2 without the benefit of a programming language. All he had to work with was raw math. So his encoding was very different from ascii, or anything you are familiar with, because it was "optimized to run on raw math" rather than a digital computer.
 The general idea is that if you have a logical system that can reason about numbers, if you figure out a way to encode the operators of the system itself as numbers, you can reason about the system itself within the system.

Applications are open for YC Summer 2019

Search: