Kurt Gödel and the romance of logic

Genuine question: how will we know that we have reached the point where “every true statement” is provable? What about unknown unknowns? Is there a “concept” (for a lack of a better word) for these “unknown unknowns” in modern logic? I know neo-Platonism (Plotinus and his friends) was circling around this idea/concept, but truth be told I haven’t read all that much coming from them, plus they may be reguarded by modern logicians/mathematicians as maybe too “mystical”.

Gödel's result, being constructive, is buildable without the Law of Excluded Middle, and it should be buildable in any topos that has Boolean logic and LEM. (And probably some other features, like infinities.) Recall that provability from a set of axioms is a path or a chaining-together of many small deductions, each one machine-checkable, and thus we can construct a proof mechanically. Therefore we are in the realm of the Booleans since that is the realm in which the proof checker is operating. Crucially, for a given set of axioms and a given arbitrary statement, either the proof does exist, in which case we may machine-check it and use the proof statement as a witness to the proof's existence, or it does not exist, and it is equivalent to the Halting Problem to show so.

To be pithy, if we choose a (true, undetermined, false) compatible with topos logic, we should be able to encode Gödel's work using only the "true" and "false" values.

You have hit upon something important, though. Recall that, in constructive logic, (WFF) statements are either true, false, or not false, where "not false" is not an actual intermediate truth value, merely a potential truth value. If we take as an axiom that statements that are not false are true (double-negation elimination) then we can derive LEM. Nonetheless, "not false" is a wonderful truth value to assign to the classic paradoxes.

To continue to be pithy, and to paraphrase a category theorist, "not false" is something that we see from the outside, but it isn't visible from the inside, and Gödel's theorems are all about encoding things into the inside.

Suppose, indeed, that we write out the Gödel statement G in some formalized English, as "This statement is true and unprovable within Formal English." Can G be true? Yeah, sure, it's true in the integers, but not in a way that Formal English can show. (That's the incompleteness!) Can G be false? Meh, yes, but it gets nasty, because G is true in the integers, so ~G leads to a non-standard model. Could G be not false? Surprisingly, yes!

I wonder whether this is the line of thought that led Bishop to his terminology.

Questions, question... I invite to learn some mathematical logic but I can give points.

But what's say there was some conjecture that if proved to be the case proved a unifying theory of everything in Physics that relied on that conjecture, but that conjecture couldn't be proven under the given set of axioms... then in that case wouldn't it be that there were some truths about the universe that aren't possible to prove?

- Well, the axioms of a given model generally can't be proven. Every model one builds begins with "unprovable things". However, the "truth about the universe" would have to be demonstrated by experimentation and mathematics would only provide the model. So every theory about the universe is using something unprovable (the axioms of its model). But Godel's theorem in particular (technically Godel's 1st incompleteness theorem) is still just a statement about proof processes work and how truth-assignments work. Whether are ineffable truths or not is a different question.

"There's this thing we can't prove under the given axioms"..."Ok, well just extend the axioms"..."Right but there is still this other thing we can't prove under that set of axioms."..."Ok, so rinse and repeat?"

- Yes, you can do that, well you can talk about doing it. In fact, Godel's "completeness theorem" is based on this procedure, more or less. The thing is you start with a set of axioms, add a proposition that can't be proven either true or false under the axioms, and decide arbitrarily whether to make it true or false. Continue forever (or transfinitely, depending how huge your system is) and you get a complete truth-assignment. Of course, there's no algorithm for finding all these undecidable propositions so this procedure is very theoretical. You or I or an AI couldn't do this to arrive pocessing this complete set but mathematically you can say "I hereby choose all the unprovable axioms and string them together thus (one of those weird "axiom of choice" things). So this approach is used, it's just it doesn't us to escape unprovable things.

In the case of True Arithmetic, the true statements are the axioms. Thus a proof of any true statement consists of just invoking the corresponding axiom, which is a valid proof in any formal system (constructive or otherwise).

The weirdness of True Arithmetic comes not from proofs (which are trivial) but from the axioms themselves. You can object that it’s not a “reasonable” or “proper” theory because it’s not recusively axiomatizable (i.e. there’s no effective procedure for even deciding whether a statement is an axiom), but I don’t think that objection is specifically constructivist.

You either don't understand the point of the theorems or are being contrarian.

In the context for the Incompleteness theorems, there are two 'kinds' of truths: a more informal kind used by all of us everyday and the mathematical kind as in, proven true under a given system.

The entire purpose of the theorems is to establish that there exists theorems in the first set that are not in the second set, while being expressable in the system. To deny the existence of the first kind of true statements ignores the entire purpose of it all.