Content-Type: text/shitpost


Subject: The uselessness of consistency proofs
Path: you​!your-host​!wintermute​!wikipedia​!uunet​!batcomputer​!plovergw​!plovervax​!shitpost​!mjd
Date: 2017-11-14T22:14:46
Newsgroup: comp.protocols.tcp-ip.consistency-proofs
Message-ID: <ccc2351554ee6b20@shitpost.plover.com>
Content-Type: text/shitpost

A consistency proof is like an insurance [policy] against an explosion of [the] Earth.
— Jean-Yves. Girard, The Blind Spot

By which I think he certainly means, if the Earth explodes, the policy is worthless since it has been destroyed along with the rest of the Earth.

And if your system turns out to be inconsistent, thus rendering all its theorems worthless, your consistency proof is thereby just as worthless.

Why then are mathematicians even interested in consistency proofs? ZF proves that PA is consistent. But ZF would prove that PA was consistent whether or not this was actually true. I suppose it is possible that PA could be consistent but ZF could fail to prove it, so it is of some interest that this case is ruled out. Still it seems like pretty thin soup.