I’m rather skeptical of that possibility. There are diverse proofs of the consistency of Peano Arithmetic’s in systems just outside that, i.e. in epsilon_zero or in second order arithmetics.
Incidentally Voevodsky talks about Gentzen’s proof in the video.
I read the statement “I doubt PA is consistent” as a shorthand for “I have radical doubts about the consistency of modern foundations, up to and including the induction schema in PA. It might be possible to write a formally valid proof of a false statement.” So the fact that there exist formally valid proofs of consistency is not that relevant.
More relevant are objections like “in that case wouldn’t planes fall out of the sky?” or “what role could mathematicians and mathematics have in the world then?” These are the kinds of questions Voevodsky is addressing in the video.
I read the statement “I doubt PA is consistent” as a shorthand for “I have radical doubts about the consistency of modern foundations, up to and including the induction schema in PA. It might be possible to write a formally valid proof of a false statement.”
Yes, but from a mathematically point of view, I could ask “Why do you believe so? There’s something, a theorem or such, that makes you believe that, or is just a mathematical way of being fancy?”. The situation is: no system interesting enough can prove its own consistency, as per Goedel’s theorem. But there are consistency proofs in more powerful system. If you doubt ZFC, there’s a proof of its consistency in ZFC + inaccessible cardinal. If you doubt “ZFC + inaccessible”, there’s a proof in ZFC + measurable cardinal, and so on.
Facing this, you have two options: believe at some point that there is a consistent model, out there in the world, that makes some set of axiom consistent (even if we might not know, even in princple), or believe that no model ever exists that makes some formal system consistent. But in that case, then you would be forced to believe that reality itself has some form of inconsistency.
It is true that logician believe in classical logic applied to world (a model can’t be inconsistent, reductio ad absurdum proofs are valid, etc.), but if you don’t like it, you could always jump to an intuitionist or paraconsistent view, and then proceed to rebuild math and logic from that point on. But if you believe that reality itself is inconsistent...well good luck for that!
I’m rather skeptical of that possibility. There are diverse proofs of the consistency of Peano Arithmetic’s in systems just outside that, i.e. in epsilon_zero or in second order arithmetics.
Incidentally Voevodsky talks about Gentzen’s proof in the video.
I read the statement “I doubt PA is consistent” as a shorthand for “I have radical doubts about the consistency of modern foundations, up to and including the induction schema in PA. It might be possible to write a formally valid proof of a false statement.” So the fact that there exist formally valid proofs of consistency is not that relevant.
More relevant are objections like “in that case wouldn’t planes fall out of the sky?” or “what role could mathematicians and mathematics have in the world then?” These are the kinds of questions Voevodsky is addressing in the video.
Yes, but from a mathematically point of view, I could ask “Why do you believe so? There’s something, a theorem or such, that makes you believe that, or is just a mathematical way of being fancy?”. The situation is: no system interesting enough can prove its own consistency, as per Goedel’s theorem. But there are consistency proofs in more powerful system. If you doubt ZFC, there’s a proof of its consistency in ZFC + inaccessible cardinal. If you doubt “ZFC + inaccessible”, there’s a proof in ZFC + measurable cardinal, and so on.
Facing this, you have two options: believe at some point that there is a consistent model, out there in the world, that makes some set of axiom consistent (even if we might not know, even in princple), or believe that no model ever exists that makes some formal system consistent. But in that case, then you would be forced to believe that reality itself has some form of inconsistency.
It is true that logician believe in classical logic applied to world (a model can’t be inconsistent, reductio ad absurdum proofs are valid, etc.), but if you don’t like it, you could always jump to an intuitionist or paraconsistent view, and then proceed to rebuild math and logic from that point on. But if you believe that reality itself is inconsistent...well good luck for that!