3 ms·
I believe most constructive mathematics (mathematics not using the law of the exluded middle) is actually weaker than peano arithmetic. Certainly there is less
by rocqua 5y ago
I believe most constructive mathematics (mathematics not using the law of the exluded middle) is actually weaker than peano arithmetic. Certainly there is less that has been proven in it. Most type theory is constructive afaik, hence it might be weaker than even Godel implies.
- zozbot234 5y agoConstructive mathematics can prove anything that classical mathematics can, and more. The only catch is that propositions which are proven classically must always be stated in the negative fragment of the logic: there's no general duality as there is in classical logic, but a positive and a negative statement mean something different.
- Koshkin 5y ago> and more I am not sure about that - there are some "pathological" phenomena in classical math that are rejected (for the lack of proof) in constructive math.
- deleted 5y ago[deleted]
- rocqua 5y agoHow does this work for the banach tarski paradox?
- zozbot234 5y agoThat depends on the axiom of choice. From a constructive POV, this means you would have to introduce some sort of extra assumptions to the theorem itself. (The axiom of choice is also inconsistent with some popular extensions to constructive mathematics, so Banach-Tarski simply cannot apply to those mathematical objects.)