3 ms·
Roughly, that proving a statement of the form "For all a,b,c,..., there exists x,y,z such that some statement involving a,b,c,...,x,y, and z is true." requires
by a1369209993 6y ago
Roughly, that proving a statement of the form "For all a,b,c,..., there exists x,y,z such that some statement involving a,b,c,...,x,y, and z is true." requires actually constructing suitable x,y, and z given suitable a,b,c, etc to derive them from.
- Abhinav2000 6y agoThanks
- zozbot234 6y agoWith the proviso that the non-constructive statement '∃ x such that P(x)' can also be understood constructively as '¬∀ x ¬P(x)' which does not require constructing a suitable x, so classical proofs can be modeled without adding any extra axioms to the logic. (Clearly the two statements are classically, though not constructively equivalent). Similarly, all classical uses of LEM (A ∨ B) can be understood as constructive statements of the form ¬(¬A ∧ ¬B).