Constructivist mathematics states that in order to prove something, we must construct this something, in a notion similar to computation, where things don't spring out of nowhere from some "mystery platonic relationship". The theory behind this I already know. A thing that I just can't understand is, if computation requires that the law of excluded middle be false, then why it's possible through binary code (a system based in 1/0 or true-false, like excluded middle).

  • 2
    $\begingroup$ There is 1, and there is 0, and there is nothing in the middle. Who told you that "the law of excluded middle" would be false? $\endgroup$
    – gnasher729
    Jul 15, 2022 at 14:00

1 Answer 1


If I were to attempt to make a computing analogue of this question, it would be this: instead of relating 0 and 1 with 'false' and 'true', suppose we called them 'diverge' and 'halt'. Now by encoding all data as bits, we have a computational system where every (data) building block has been associated with definitely halting or not halting, and we can just test the bit to decide which one it is. But, the halting problem for Turing machines with this naming scheme remains undecidable. Why?

The answers are similar. Even though you can describe a Turing machine as a bunch of bits that you have called "halt" and "diverge", the halting problem is about what the described machine does, not some simple aggregation of the bits in its description.

The relation of classical logic to bits has to do with the former having (in the simplest case) two "truth values". So, you can describe those two values with states of a bit, and given a finite propositional calculus formula and bits for the truth values of the variables, you can calculate a bit for the truth value of the whole proposition. It also happens that the bit calculated for $P ∨ ¬P$ this way is $1$ regardless of the bit for $P$.

However, this is not what is done when we give computational meanings for (first/higher order) intuitionistic logic formulas. Formulas are not interpreted as bits but as specifications for machines or programs. And which programs meet the specification is not determined by what bits they are built out of, but what they do. In some cases, this might be very simple, like:

  • Every program meets the specification for truth, or $⊤$.
  • No program meets the specification for false, or $⊥$.

But there are complex examples like:

  • A program for $A ∨ B$ must output $0$ together with a program for $A$, or $1$ together with a program for $B$
  • A program for $A → B$ must accept a program for $A$ and produce a program for $B$.
  • A program for $∀ n:ℕ. P(n)$ must accept a natural number $k$ and produce a machine for $P(k)$.

Importantly, this means that a machine meeting the specification for $P ∨ ¬P$ must decide $P$, where $P$ is not just a bit, but a specification for machines. And the logic is rich enough that it can encode undecidable computational programs as machine specifications. So, because there are undecidable computational problems, there is in turn no hope of the principle $P ∨ ¬P$ holding generally. For instance, $∀n. P(n) ∨ ¬P(n)$ could have to be a machine that decides the halting problem, because $P(n)$ is an encoding of, "the $n$th machine (under some numbering) halts."

The bit version of things can be embedded into the specification framework. For propositions that do correspond to decidable problems, the specification does correspond to some other expression involving bits, and machines deciding the problem will answer according to the classical truth value represented by the bit. But, of course, this only works for problems/propositions that are decidable.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.