4 ms·

The biggest qualm that I have with the example for the incompleteness theorem, is the use of two-valued, Boolean/Aristotelian logic, in which "not true" automat

The biggest qualm that I have with the example for the incompleteness theorem, is the use of two-valued, Boolean/Aristotelian logic, in which "not true" automatically becomes "false". If you allow the use of a three-valued logic, for example, with (true, undetermined, false), the Gödel statement, “I am not provable" amounts to saying "My provability is false or undetermined". The same problem occurs in Russell's paradox, "Does the set of all sets that do NOT contain themselves, contain itself?" The use of the NOT-operator is degenerated in a cyclic group Z2. It is the only situation in which the NOT-operator is not set-valued. In my opinion, if the "isProvable()" predicate allowed for multi-valued logic, Gödel's incompleteness theorem would look much less paradoxical. In other words, the paradoxical outcome could simply be the result of Boolean shoehorning.

deleted 8y ago
[deleted]
theaeolist 8y ago
The incompleteness result does not even mention "true" and "false". It says that "there are statements of the language of F which can neither be proved nor disproved in F." Whether those statements are true/false is left unsaid.
chewz 8y ago
You don't grasp. Gödel's incompleteness theorems is not dependent on chosen logic or any set of axioms. It stands in 3-, 4- and N-value logic as well.
myWindoonn 8y ago
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.

deleted 8y ago

[deleted]

theaeolist 8y ago

The incompleteness result does not even mention "true" and "false". It says that "there are statements of the language of F which can neither be proved nor disproved in F." Whether those statements are true/false is left unsaid.

chewz 8y ago

You don't grasp. Gödel's incompleteness theorems is not dependent on chosen logic or any set of axioms. It stands in 3-, 4- and N-value logic as well.

myWindoonn 8y ago

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.