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.
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.