4 ms·
I find computer scientists have a stronger grasp on encodings than mathematicians, who tend to get bogged down in these details due to lack of familiarity. Wit
by kmill 7y ago
I find computer scientists have a stronger grasp on encodings than mathematicians, who tend to get bogged down in these details due to lack of familiarity. With what I wrote up, the point I failed to make is that it comes down to some cleverness in how you mess around with read, eval(=provable), and print. That is, follow the Lisp way and think in s-expressions.
I was responding specifically to
> All the rest, all the heavy lifting, is just cranking out the tedious details of what those mathematical operations actually are, but none of that is necessary in order to understand the core idea of the proof.
The thing I'm taking issue with is calling parsing the core idea, with the rest "just"[1] being tedious details, where, as someone who has done some PL implementations, the parsing seems to me to be the tedious part. It's an important idea that's essential to the proof, but, again, that's like saying parsing is the core problem in writing a compiler (or that writing read is the core problem in implementing a Lisp interpreter). This is not exactly evidence of any kind, but notice your whole final paragraph is a diagonalization argument, and it is longer than the first paragraph of your exposition, which quickly explains how strings can represent logical statements and proofs.
Maybe this is a synthesis: the core idea is that you can write an interpreter that takes an encoding of a logical statement and returns whether or not it is provable. Since the interpreter is itself a logical statement, you can apply a diagonalization argument to produce a true statement that refutes its own provability. (When I say the core idea is the diagonalization, I mean both the interpreter and the fixed point finding. When you say the core idea is encoding, I suspect you might mean more the interpreter than how your comment reads to me.)
By the way, with the halting problem argument, it seems like if you're very careful you can write out an explicit Godel sentence, like what the Lawvere fixed point theorem would provide. I'm sort of curious what it would look like, rather than your recipe for how to construct it. (I also wonder what the shortest Godel sentence is. But only as much as I wonder what the shortest quines are.)
> "The string corresponding to N has no proof"
Small correction: it's that "N being true is equivalent to N having no proof." If N is false, then it is provable (bad), so if things are consistent it must be true, hence unprovable. It's interesting that N is a true statement.
[1] I have a banned words list in my office; one entry is "just" because of just what it lets you sweep under the rug.
- charlie298436 7y agoAssume 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 agoThat 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 agoA 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.