3 ms·

Assume the layman has been informed that first-order mathematical theories that admit of quantifier elimination (Presburger arithmetic, Euclidean geometry, real

Assume the layman has been informed that first-order mathematical theories that admit of quantifier elimination (Presburger arithmetic, Euclidean geometry, real closed fields, abelian groups, random graphs, etc.) are complete and decidable. From the layman's perspective the question then is: WHY is Peano Arithmetic incomplete? What does it add to the mix that makes it categorically different from those other axiom systems? ENCODING power is the answer; that is, the expressive capacities of PA versus these other systems. In particular, PA is expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization/self-reference/Lawvere (depending on your background) are readily understood. So to my mind, the layman would be more puzzled by the differing expressive powers of formal languages, and why exactly they lead to differences in provability. E.g., is the defineability of exponentiation a prerequisite to linguistic self-encoding? What's the relationship between quantifier elimination and self-reference? To what extent does a robust concept of 'infinity' play a role. Etc., etc.

lisper 7y ago
That is one of the most insightful and thought-provoking comments I have ever seen anywhere on any topic. Welcome to HN, charlie298436! I hope we see more of you.
kmill 7y ago
A similar question is why are some Turing machines universal and some aren't? Or, more generally, why can you prove some Turing machines halt on all inputs and for some you cannot? I think what you mean by "encoding" is what I mean by "being able to write an interpreter." It's not hard to encode mathematical statements as real numbers in the axioms of a real closed field, which someone outside the theory is easily able to decode. However, the fact the theory is complete implies there is no way to write an interpreter within the theory. There are other kinds of interpreters you might be interested in. For example, one that determines absolute truth of a statement, that is, the truth of the statement in the "Platonic universe," whether or not it is provable. You can still apply the usual kind of argument, if such an interpreter existed, to generate a sentence that is true iff it is false. I imagine a heuristic sort of issue is that to write such an interpreter you need to be able to encode environments (like in a Scheme interpreter), but the set of possible environments is too big in a Russell's paradox sort of way. In model theory, they call such a function, when restricted to a particular model, a truth term. > expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization [...] are readily understood I don't really understand you here: a diagonalization/Lawvere-like argument is how the Gödel sentence is constructed in the first place.
kazinator 7y ago
Encoding is an answer; Goedel's work uses self-encoding to establishes the existence of statements that cannot be derived from existing axioms, but do not conflict with them. That doesn't seem to rule out the possibility of some "organic" way of obtaining such axioms.

lisper 7y ago

That is one of the most insightful and thought-provoking comments I have ever seen anywhere on any topic. Welcome to HN, charlie298436! I hope we see more of you.

kmill 7y ago

A similar question is why are some Turing machines universal and some aren't? Or, more generally, why can you prove some Turing machines halt on all inputs and for some you cannot? I think what you mean by "encoding" is what I mean by "being able to write an interpreter." It's not hard to encode mathematical statements as real numbers in the axioms of a real closed field, which someone outside the theory is easily able to decode. However, the fact the theory is complete implies there is no way to write an interpreter within the theory. There are other kinds of interpreters you might be interested in. For example, one that determines absolute truth of a statement, that is, the truth of the statement in the "Platonic universe," whether or not it is provable. You can still apply the usual kind of argument, if such an interpreter existed, to generate a sentence that is true iff it is false. I imagine a heuristic sort of issue is that to write such an interpreter you need to be able to encode environments (like in a Scheme interpreter), but the set of possible environments is too big in a Russell's paradox sort of way. In model theory, they call such a function, when restricted to a particular model, a truth term. > expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization [...] are readily understood I don't really understand you here: a diagonalization/Lawvere-like argument is how the Gödel sentence is constructed in the first place.

kazinator 7y ago

Encoding is an answer; Goedel's work uses self-encoding to establishes the existence of statements that cannot be derived from existing axioms, but do not conflict with them. That doesn't seem to rule out the possibility of some "organic" way of obtaining such axioms.