3 ms·
The idea that a proof should show why something is true is one of the fundamental motivations for constructive mathematics. (Brouwer and Martin-Löf would both s
by intuitionist 8y ago
The idea that a proof should show why something is true is one of the fundamental motivations for constructive mathematics. (Brouwer and Martin-Löf would both say that this is what a proof is, almost by definition.) So for instance an existence proof is no good unless it gives you a way of constructing an actual witness.
At that point you can ask questions like “are these two reasons why theorem W is true the same or different?” which leads into things like homotopy type theory.