What's interesting is that proof is computer assisted:
The proofs are automatically checked by a program I devised called qea (forquod est absurdum, since all the proofs are indirect). Most proof checkers require one to trust that the program is correct, something that is notoriously difficult to verify. But qea, from a very concise input, prints out full proofs that a mathematician can quickly check simply by inspection. To date there are 733 axioms, definitions, and theorems, and qea checked the work in 93 seconds of user time, writing to files 23 megabytes of full proofs that are available from hyperlinks in the book.
I don't think so; from a quick glance, I believe the theorem deals with inconsistencies when dealing with infinities, and the program and its output are all finite. If the program hangs or runs out of disk space, then that might be confirming evidence for the theorem ;-).
An consistent theorem system can know no bounds. There's halfway. If Peano arithmetic is inconsistent every statement in it is provably true and false. QED.
The proofs are automatically checked by a program I devised called qea (forquod est absurdum, since all the proofs are indirect). Most proof checkers require one to trust that the program is correct, something that is notoriously difficult to verify. But qea, from a very concise input, prints out full proofs that a mathematician can quickly check simply by inspection. To date there are 733 axioms, definitions, and theorems, and qea checked the work in 93 seconds of user time, writing to files 23 megabytes of full proofs that are available from hyperlinks in the book.