One of my mistakes was believing in Bayesian decision theory, and in constructive logic at the same time. This is because traditional probability theory is inherently classical, because of the axiom that P(A + not-A) = 1.
Could you be so kind as to expand on that?
Classical logics make the assumption that all statements are either exactly true or exactly false, with no other possibility allowed. Hence classical logic will take shortcuts like admitting not(not(X)) as a proof of X, under the assumptions of consistency (we’ve proved not(not(X)) so there is no proof of not(X)), completeness (if there is no proof of not(X) then there must be a proof of X) and proof-irrelevance (all proofs of X are interchangable, so the existence of such a proof is acceptable as proof of X).
The flaw is, of course, the assumption of a complete and consistent system, which Goedel showed to be impossible for systems capable of modelling the Natural numbers.
Constructivist logics don’t assume the law of the excluded middle. This restricts classical ‘truth’ to ‘provably true’, classical ‘false’ to ‘provably false’ and allows a third possibility: ‘unproven’. An unproven statement might be provably true or provably false or it might be undecidable.
From a probability perspective, constructivism says that we shouldn’t assume that P(not(X)) = 1 - P(X), since doing so is assuming that we’re using a complete and consistent system of reasoning, which is impossible.
Note that constructivist systems are compatible with classical ones. We can add the law of the excluded middle to a constructive logic and get a classical one; all of the theorems will still hold and we won’t introduce any inconsistencies.
Another way of thinking about it is that the law of the excluded middle assumes that a halting oracle exists which allows us to take shortcuts in our proofs. The results will be consistent, since the oracle gives correct answers, but we can’t tell which results used the oracle as a shortcut (and hence don’t need it) and which would be impossible without the oracle’s existence (and hence don’t exist, since halting oracles don’t exist).
The only way to work out which ones are shortcuts is to take ‘the long way’ and produce a separate proof which doesn’t use an oracle; these are exactly the constructive proofs!
Classical logics make the assumption that all statements are either exactly true or exactly false, with no other possibility allowed. Hence classical logic will take shortcuts like admitting not(not(X)) as a proof of X, under the assumptions of consistency (we’ve proved not(not(X)) so there is no proof of not(X)), completeness (if there is no proof of not(X) then there must be a proof of X) and proof-irrelevance (all proofs of X are interchangable, so the existence of such a proof is acceptable as proof of X).
The flaw is, of course, the assumption of a complete and consistent system, which Goedel showed to be impossible for systems capable of modelling the Natural numbers.
Constructivist logics don’t assume the law of the excluded middle. This restricts classical ‘truth’ to ‘provably true’, classical ‘false’ to ‘provably false’ and allows a third possibility: ‘unproven’. An unproven statement might be provably true or provably false or it might be undecidable.
From a probability perspective, constructivism says that we shouldn’t assume that P(not(X)) = 1 - P(X), since doing so is assuming that we’re using a complete and consistent system of reasoning, which is impossible.
Note that constructivist systems are compatible with classical ones. We can add the law of the excluded middle to a constructive logic and get a classical one; all of the theorems will still hold and we won’t introduce any inconsistencies.
Another way of thinking about it is that the law of the excluded middle assumes that a halting oracle exists which allows us to take shortcuts in our proofs. The results will be consistent, since the oracle gives correct answers, but we can’t tell which results used the oracle as a shortcut (and hence don’t need it) and which would be impossible without the oracle’s existence (and hence don’t exist, since halting oracles don’t exist).
The only way to work out which ones are shortcuts is to take ‘the long way’ and produce a separate proof which doesn’t use an oracle; these are exactly the constructive proofs!