dezakin

Not sure about the etiquette in replying in someone else's AMA, so I hope I'm not breaking the rules here. If I am I apologize.

Gödel’s incompleteness theorems formally suggest there are statements that are undecidable. They're essentially a number theoretic way of saying "this statement is not provable," which is a self reference trick, similar to the liar paradox. There are models where these statements are true, most notably the standard model of arithmetic... and there are models where this statement is false... that we call nonstandard models of arithmetic. So suggesting that the statement is "true, but unprovable" is a bit strong and misleading.

There are philosophical reasons why we prefer to think of these statements as unprovable but "true," like the result of Tennenbaum's theorem, which basically says that there's no recursive nonstandard model of arithmetic that's countable, so when the Gödel sentence is false, it's in a very different world than we are accustomed to.

Truth is about being satisfied by a particular model, but provability means you can satisfy it in every model (with the same axioms,) so I tend to think that Hofstadter got it backwards.

What do you make of the current enthusiasm for Homotopy Type Theory, compared to something more orthodox, like set theory? Because to me, set theory is more convenient for automated reasoning with it's embedding in first order/higher order logic with it's mature proof calculus (particularly resolution with clauses which have nice properties that are easy for machines to manipulate) and well developed model theory that allows one to do some tests for satisfiability or the (non)existence of finite models. Is HOTT really the wave of the future?

Does the negative answer to the entscheidungsproblem mean there are some first order statements that aren't unsatisfiable without any models, or does it mean these statements are simply "shrouded in darkness" from our ability to reason with finite tools?