3 ms·
There is an entire movement within maths called 'intuitonist logic' that does not want to use ¬¬ϕ = ϕ. The point behind it is to only use 'constructive' proofs
by rocqua 10y ago
There is an entire movement within maths called 'intuitonist logic' that does not want to use ¬¬ϕ = ϕ.
The point behind it is to only use 'constructive' proofs. Or rather, to avoid proofs that show a counter-example is impossible.
- ajarmst 10y agoI don't get it. Do they feel that ¬¬ϕ = ϕ is invalid or contingent? Or is it just a matter of taste?
- ajarmst 10y agoReplying to myself. Roqua has a nice description of the motivation elsewhere in this thread, with regard to how a constructive proof can offer more insight into the thing being proven than a mere 'yes, it's true'. I can see their point.
- tel 10y agoThey feel that there are some sorts of statements ϕ for which ¬¬ϕ = ϕ is invalid. Or, more interestingly, that if we force it to be such that all statements have that property then we lose the ability to talk about certain interesting things where it is not available.