Last month, The Edge published an article by Verena Huber-Dyson entitled Gödel and the Nature of Mathematical Truth II. The nice thing about Huber-Dyson's paper is the way it describes the work of Kurt Gödel in the greater context of the work of David Hilbert.
In 1920, Hilbert proposed a mathematical research program that would show that all of mathematics follows from a finite set of axioms, and that the resulting axiomatic system would be provably consistent.
Of Hilbert's program Huber-Dyson writes:
Wanted was a proof that the system using, what Hilbert called "ideal elements" — reasoning about infinite sets the way we are used to reason about finite ones — was not going to lead beyond the realm of what is justified by finitary reasoning, in other words, that the make believe world of predicate logic was a mere conservative extension of finitism. Alas, he wishfully thought that all he needed was a proof of simple consistency as defined above. That is why the demand for a finitist proof of the consistency of any of the current formal systems was his major concern.
Of course, Gödel showed that Hilbert's program was not feasible:
...Gödel showed how to construct, in any formal system that encompasses a minimal fragment of elementary arithmetic, a sentence, which is true if and only if it cannot be proved, and therefore is true but not provable, unless the system is unsound.
For me, the most interesting part of the paper is something called mathematical intuitionism.
In a nutshell: intuitionist reasoning is a refinement of classical thinking. Identifying notnotA with A only when there is good reason to do so is much closer to everyday reasoning than the practice of the classical law of double negation. With a bit of care most of the popular but devious proofs of positive claims by reductio ad absurdum can be replaced by direct arguments...
claim (A or B) only if you have a method for deciding which one of them is the case; if you want to insist on the existence of an object with a certain property, be sure you have a method for producing such an object when called for.
Wikipedia says this about intuitionism:
For example, to say A or B, to an intuitionist, is to claim that either A or B can be proved. In particular, the law of excluded middle, A or not A, is disallowed since one cannot assume that it is always possible to either prove the statement A or its negation.
I like the sound of this idea (though I will have to do a lot more reading on this subject before I accept it). You see, I read this as a mathematical analogue of logical positivism. If there is no mechanism by which proposition A can be verified, we are not justified in assigning it a truth value at all.