3 ms·

Oh, let me close up one little hole in my comment, before anyone points it out. :) This may require rather more mathematical knowledge I'm afraid. Above I sai

Oh, let me close up one little hole in my comment, before anyone points it out. :) This may require rather more mathematical knowledge I'm afraid. Above I said the only reasonable way to weaken Peano arithmetic was to weaken induction. But that's not quite true. There's another way: Not changing any of the axioms, but weakening the underlying logic. See, there's a school of mathematics known as "constructivism", and they object to the usual laws of logic, saying that they're too strong; they use a weaker logic. It ought to be called "constructive logic", but for historical reasons (that are really not worth getting into) it's called "intuitionistic logic" instead. And this might seem to be a better approach, because weakening the laws of logic is something that can be done without regard for the setting; it doesn't matter here whether you're talking about just whole numbers, or mathematics as a whole. (Well, almost. Actually, from ZFC and intuitionistic logic, you can effectively get back classical logic. But there are pretty good ideas about how to modify ZFC to avoid that.) The problem is, doing this doesn't help. Because it's known that if you can prove a contradiction from the Peano axioms using classical logic, you can also do so using intuitionistic logic. So even if you went constructive, you'd still be stuck with all the same problems.

nocturnial 5y ago
> 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
chithanh 5y ago
In addition to weakening the logic (or avoiding the parts that introduce incompleteness, especially the existential quantifier) you also need to weaken your arithmetic. We know that Primitive Recursion (PR) is too weak to prove its own consistency, and Peano Arithmetic (PA) is too strong. So you may have to look at a strengthening of PR and/or weakening of PA in order to achieve a theory that proves its own consistency. Whether that theory exists is still an open question.
- Sniffnoy 5y ago
  Getting a theory that proves its own consistency isn't what's being discussed here. What's being discussed here is just weakening a theory to remove a particular inconsistency after an inconsistency is found. Trying to make a usable theory that also proves its own consistency is probably also a futile goal, per Gödel, but it's a separate one, and not one that people would likely go for if an inconsistency were found in Peano arithmetic.

nocturnial 5y ago

> 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

chithanh 5y ago

In addition to weakening the logic (or avoiding the parts that introduce incompleteness, especially the existential quantifier) you also need to weaken your arithmetic. We know that Primitive Recursion (PR) is too weak to prove its own consistency, and Peano Arithmetic (PA) is too strong. So you may have to look at a strengthening of PR and/or weakening of PA in order to achieve a theory that proves its own consistency. Whether that theory exists is still an open question.

Sniffnoy 5y ago
Getting a theory that proves its own consistency isn't what's being discussed here. What's being discussed here is just weakening a theory to remove a particular inconsistency after an inconsistency is found. Trying to make a usable theory that also proves its own consistency is probably also a futile goal, per Gödel, but it's a separate one, and not one that people would likely go for if an inconsistency were found in Peano arithmetic.