3 ms·

> if you can prove a contradiction from the Peano axioms using classical logic, you can also do so using intuitionistic logic. Are you sure it isn't the other

> if you can prove a contradiction from the Peano axioms using classical logic, you can also do so using intuitionistic logic. Are you sure it isn't the other way around? If you can prove a contradiction using intuitionistic logic, it's also a contradiction using classical. If you proved the contradiction using the excluded middle then that proof wouldn't hold when you use intuitionistic logic. Maybe I'm missing or not understanding something here.

Sniffnoy 5y ago
I mean, the other way around is also true, but the other way around is obvious. Obviously going from a weaker logic to a stronger logic can't eliminate contradictions. What's surprising is that in this particular case (the Peano axioms), the reverse is also true; you won't be able to eliminate contradictions by passing to this weaker logic. Note, all I said is, if you can prove a contradiction classically, then you can prove a contradiction constructively! I didn't say, if you have a classical proof of a contradiction then it's a valid constructive proof of a contradiction. Obviously not! But it will still be true that you'll be able to prove a contradiction constructively; it just won't necessarily be the same proof. If you want to know more about the particular transformation, well, here's a relevant Wikipedia article: https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation
- nocturnial 5y ago
  Thank you for your explanation and pointing me to the double negation translation. I know this is off-topic but if you have a book recommendation which teaches about intuitionistic logic/constructive math and also mentions the double negation translation, I'm interested. Most books I've read seem to either concentrate on only constructive or classical math.
  - Sniffnoy 5y ago
    I don't, sorry. I'm not really a logician, just a mathematician who thinks the foundations are worth understanding. :) I don't know what proper references on this material would be.
taejo 5y ago
Classical logic can be embedded into intuitionistic logic. The double-negation translation N [0] turns any tautology of classical logic into a tautology of intuitionistic logic, so if θ ∧ ¬θ is provable with classical logic, N(θ) ∧ ¬N(θ) is provable with intuitionistic logic. [0]: https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation

Sniffnoy 5y ago

I mean, the other way around is also true, but the other way around is obvious. Obviously going from a weaker logic to a stronger logic can't eliminate contradictions. What's surprising is that in this particular case (the Peano axioms), the reverse is also true; you won't be able to eliminate contradictions by passing to this weaker logic. Note, all I said is, if you can prove a contradiction classically, then you can prove a contradiction constructively! I didn't say, if you have a classical proof of a contradiction then it's a valid constructive proof of a contradiction. Obviously not! But it will still be true that you'll be able to prove a contradiction constructively; it just won't necessarily be the same proof. If you want to know more about the particular transformation, well, here's a relevant Wikipedia article: https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation

nocturnial 5y ago
Thank you for your explanation and pointing me to the double negation translation. I know this is off-topic but if you have a book recommendation which teaches about intuitionistic logic/constructive math and also mentions the double negation translation, I'm interested. Most books I've read seem to either concentrate on only constructive or classical math.
- Sniffnoy 5y ago
  I don't, sorry. I'm not really a logician, just a mathematician who thinks the foundations are worth understanding. :) I don't know what proper references on this material would be.

taejo 5y ago

Classical logic can be embedded into intuitionistic logic. The double-negation translation N [0] turns any tautology of classical logic into a tautology of intuitionistic logic, so if θ ∧ ¬θ is provable with classical logic, N(θ) ∧ ¬N(θ) is provable with intuitionistic logic. [0]: https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation