Here’s a more interesting angle than the water droplets:
There’s presumably some chance that there will be more math discovered—something with an effect like Goedel, but ever so much more so—which will make 2 + 2 = 4 not quite so certain.
For example, PA may turn out to be inconsistent. Here’s a great story about that possibility. Similar things have happened already: many people were surprised when Russell’s paradox broke naive set theory which looked as obviously consistent then as PA looks to us now.
This is another point for my claim that we need to understand how actual humans do math, not invest everything into one set of axioms.
Similar things have happened already: many people were surprised when Russell’s paradox broke naive set theory which looked as obviously consistent then as PA looks to us now.
Note that we have good reasons for believing that PA is consistent. Gentzen’s theorem is the most obvious one. I’d say we have much more reason to believe that PA is consistent than someone would have had prior to Russell believing that naive set theory was consistent. But that may involve some hindsight bias.
Note that we have good reasons for believing that PA is consistent. Gentzen’s theorem is the most obvious one.
Gentzen’s theorem assumes a much stronger claim to prove this weaker one. Yes, it grounds consistency of PA in another mathematical intuition, and in this sense could be said to strengthen the claim a bit, but formally it’s a sham.
(Of course, modern mathematics is much stronger than a century ago, so that alone counts for a good reason to believe that PA is consistent.)
Gentzen’s theorem assumes a much stronger claim to prove this weaker one.
No. The minimal axioms needs to prove Gentzen’s theorem are not stronger than PA. There are claims in PA that cannot be proven in the minimal context for Gentzen’s theorem.
There is a lot of weirdness here, once you try to reduce the question.
Imagine an AI programmed to believe in the axioms of PA and nothing else. What credence should it assign to the arithmetical statement Con(PA)? The answer is that there’s no answer. Assuming PA is “in fact” consistent, Con(PA) is formally independent from PA—which means I may add the negation of Con(PA) to PA as an extra axiom and get a consistent system. (Equivalently, that “self-hating” system has a model in ordinary set theory. Building it is a neat little exercise.) So believing or disbelieving in the “actual” consistency of PA, as we humans can, requires some notion of Platonism or semantics that we cannot yet teach to a computer.
And the question why you instinctively believe Gentzen’s proof, which uses transfinite induction up to epsilon zero, is even more mysterious. You’re comfortable relying on the consistency of a stronger system than PA because it sounds intuitive to you, right? Where do those intuitions come from? The very same place where naive set theory came from, I think.
“There’s presumably some chance that there will be more math discovered—something with an effect like Goedel, but ever so much more so—which will make 2 + 2 = 4 not quite so certain.”
Here’s a more interesting angle than the water droplets:
There’s presumably some chance that there will be more math discovered—something with an effect like Goedel, but ever so much more so—which will make 2 + 2 = 4 not quite so certain.
For example, PA may turn out to be inconsistent. Here’s a great story about that possibility. Similar things have happened already: many people were surprised when Russell’s paradox broke naive set theory which looked as obviously consistent then as PA looks to us now.
This is another point for my claim that we need to understand how actual humans do math, not invest everything into one set of axioms.
Note that we have good reasons for believing that PA is consistent. Gentzen’s theorem is the most obvious one. I’d say we have much more reason to believe that PA is consistent than someone would have had prior to Russell believing that naive set theory was consistent. But that may involve some hindsight bias.
Gentzen’s theorem assumes a much stronger claim to prove this weaker one. Yes, it grounds consistency of PA in another mathematical intuition, and in this sense could be said to strengthen the claim a bit, but formally it’s a sham.
(Of course, modern mathematics is much stronger than a century ago, so that alone counts for a good reason to believe that PA is consistent.)
No. The minimal axioms needs to prove Gentzen’s theorem are not stronger than PA. There are claims in PA that cannot be proven in the minimal context for Gentzen’s theorem.
There is a lot of weirdness here, once you try to reduce the question.
Imagine an AI programmed to believe in the axioms of PA and nothing else. What credence should it assign to the arithmetical statement Con(PA)? The answer is that there’s no answer. Assuming PA is “in fact” consistent, Con(PA) is formally independent from PA—which means I may add the negation of Con(PA) to PA as an extra axiom and get a consistent system. (Equivalently, that “self-hating” system has a model in ordinary set theory. Building it is a neat little exercise.) So believing or disbelieving in the “actual” consistency of PA, as we humans can, requires some notion of Platonism or semantics that we cannot yet teach to a computer.
And the question why you instinctively believe Gentzen’s proof, which uses transfinite induction up to epsilon zero, is even more mysterious. You’re comfortable relying on the consistency of a stronger system than PA because it sounds intuitive to you, right? Where do those intuitions come from? The very same place where naive set theory came from, I think.
“There’s presumably some chance that there will be more math discovered—something with an effect like Goedel, but ever so much more so—which will make 2 + 2 = 4 not quite so certain.”
Uh, no.