[FOM] truth and consistency

[Martin Davis]

Albert Einstein is reputed to having expressed some bewilderment concerning 
the quarrel between Hilbert and Brouwer, asking: "What is this frog and 
mouse battle among the mathematicians about anyway?"

I feel rather like that regarding philosophers as I read some recent FOM 
postings on the question of in what sense one can be secure in the belief 
that Gödel's undecidable sentence G is true. I think the basic fact is 
straightforward and acknowledged by all. One is entitled to unequivocally 
assert G only if one is convinced of the consistency of the underlying 
formal system. So the only question, and it is certainly an important one 
is: what sort of evidence can one bring to bear in deciding this question. 
The question of whether a contradiction is derivable in a given formal 
system is, on the face of it, an intricate combinatorial question.  I'm 
fond of noting that the list of logicians who have seriously proposed 
formal systems that turned out to be inconsistent reads like an honor roll: 
Frege, Church, Curry, Quine, Rosser.

If the underlying system is PA (first order number theory), I believe that 
one can claim that the evidence for its consistency is simply overwhelming. 
Even the trivial consistency proof based on the standard model uses far 
less than much well-accepted ordinary mathematics. And the various 
proof-theoretic epsilon-zero consistency proofs by Gentzen, Ackermann, and 
Gödel are entirely compelling.

For higher order systems like type theory or ZFC, I know no reason for 
believing in their consistency other than the fact that the axioms are 
satisfied by our intuitive Cantorian picture of sets of sets of sets of 
.... To someone who has no doubt that the properties of this construct are 
objective (even if only partially determinable by us) the matter is 
unproblematic. Others have to live with the uncertainty that is with us in 
most aspects of the human condition.

Invoking reflection principles such as Turing's prov(p) -> p, is really no 
help. Someone who accepts such a principle must already be convinced.

I will close with a quote (that also represents my own view) from Gödel's 
famous Gibbs lecture in 1951:

<<If mathematics describes an objective world just like physics, there is 
no reason why inductive methods should not be applied in mathematics just 
the same as in physics. The fact is that in mathematics we still have the 
same attitude today that in former times one had toward all science, namely 
we try to derive everything by cogent proofs from the definitions (that is, 

 from the essences of things). Perhaps this method, if it claims monopoly, 
is as wrong in mathematics as it was in physics.>>

-Martin