[FOM] inconsistency
Martin Davis
martin at eipye.com
Wed Oct 4 15:56:14 EDT 2006
Two points that have come up in the discussion of Lucas-Penrose:
1. In the "honor roll" of logicians who have seriously proposed systems
that later turned out to be inconsistent, I had included Rosser, and
someone questioned why. In his book "Logic for Mathematicians" Rosser uses
Quine's New Foundations as his base system. There is a chapter on
consequences of the axiom of choice. Because Specker proved that NF+AC is
inconsistent, I felt that Rosser had earned a place on the list. He was
angry with me over this.
2. There have been some statements to the effect that whereas an
inconsistent formal system will produce '0=1' (or the like) we will not
even if our reasoning is inconsistent. I once tried to make a computer
implementation of NF+AC do exactly that, with no success. A formal system
can be inconsistent although the shortest proof of a contradiciton can be
very long. It has also been suggested that we can recognize a contradiction
if we produce one unlike a computer implementation. But many formal
theorem-proving programs work exactly by beginning with the negation of
what is to be proved and attempting to derive a contradiction from that.
Martin
More information about the FOM
mailing list