4 ms·

I don't get it. Do they feel that ¬¬ϕ = ϕ is invalid or contingent? Or is it just a matter of taste?

• ajarmst 10y ago
  Replying 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 ago
  They 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.