[FOM] inconsistency

[Martin Davis]

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