There's an ongoing discussion on math sites about Vladimir Voevodsky's Fall 2010 lecture expressing doubts that math is consistent, i.e. doubts that it is not possible to deduce formally correct proofs of false statements starting from standard axioms.
I like Voevodsky's pragmatism. The universe/mathematics doesn't explode when you find an inconsistency, only your current tools for determining mathematical truth. And that one might possibly locally patch up our tools for verifying proofs even in a globally inconsistent system.
It sort of depends on what you mean by false. Syntactically, inconsistency would mean that I can derive anything, including proofs of impossibility of completeness, proofs of completeness etc.
Taking the lecture literally, I take it that Voevodsky considers it wholly possible that PA will cough up mutually incompatible statements at some point and we will no longer have a good reason to suppose that it is inconsistent.
Another possibility is that he wanted to to point out that this is not strictly speaking ruled out so you should pay attention to his work on a nice alternative that just so happens to be in line with his goal of streamlining automated theorem proving and proof verification ;).
I get the impression that he is likely a constructivist who does not accept current consistency proofs of PA, and he is to some degree leveraging his position in order to push for a streamlined, automated constructivist foundations for future mathematics research. An effort that I support 100%.
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 like Voevodsky's pragmatism. The universe/mathematics doesn't explode when you find an inconsistency, only your current tools for determining mathematical truth. And that one might possibly locally patch up our tools for verifying proofs even in a globally inconsistent system.
Nicely put!