4 ms·
A proof in mathematics is not purely syntactic because it's not purely logical. This is confusing constructive reasoning with the decision problem for proof va
by mafribe 11y ago
A proof in mathematics is not purely syntactic because it's not purely logical.
This is confusing constructive reasoning with the decision problem for proof validity. They are different things.
The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make use of non-logical axioms of the ambient theory. If proof-hood is not decidable, it's not a logic.
Reasoning is constructive if it avoids certain proof principle like LEM (law of excluded middle) or double negation.
- kazinator 11y agoI seem to have the impression that constructivism in math is the same thing as constructive logic, though they are related. Constructivism in mathematics: https://en.wikipedia.org/wiki/Constructivism_%28mathematics%29 https://en.wikipedia.org/wiki/Constructivism_%28mathematics%... Constructive (intuitionistic) logic: https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic Surely, one can be a constructivist mathematician, yet not eschew double negatives?
- mafribe 11y agoNo. Classically, LEM and double negation are equivalent. Intuitionistically the situation is more complicated, see the discussion in this thread by IngoBlechschmid: We can prove that LEM implies double negation, but not the other way around. Intuitionistically, we can only prove that ⊢¬¬A⊃A, then ⊢A∨¬A, but not ⊢(¬¬A⊃A)⊃(A∨¬A). For these and related reasons, double negation is not considered constructivistically valid.