Consistency Proofs
As previously mentioned, the spur for the mathematical investigation of proofs in formal theories was Hilbert's program. The central idea of this program was that if we could give finitary proofs of consistency for all the sophisticated formal theories needed by mathematicians, then we could ground these theories by means of a metamathematical argument, which shows that all of their purely universal assertions (more technically their provable sentences) are finitarily true; once so grounded we do not care about the non-finitary meaning of their existential theorems, regarding these as pseudo-meaningful stipulations of the existence of ideal entities.
The failure of the program was induced by Kurt Gödel's incompleteness theorems, which showed that any ω-consistent theory that is sufficiently strong to express certain simple arithmetic truths, cannot prove its own consistency, which on Gödel's formulation is a sentence.
Much investigation has been carried out on this topic since, which has in particular led to:
- Refinement of Gödel's result, particularly J. Barkley Rosser's refinement, weakening the above requirement of ω-consistency to simple consistency;
- Axiomatisation of the core of Gödel's result in terms of a modal language, provability logic;
- Transfinite iteration of theories, due to Alan Turing and Solomon Feferman;
- The recent discovery of self-verifying theories, systems strong enough to talk about themselves, but too weak to carry out the diagonal argument that is the key to Gödel's unprovability argument.
See also Mathematical logic
Read more about this topic: Proof Theory
Famous quotes containing the words consistency and/or proofs:
“People who love only once in their lives are ... shallow people. What they call their loyalty, and their fidelity, I call either the lethargy of custom or their lack of imagination. Faithfulness is to the emotional life what consistency is to the life of the intellect—simply a confession of failures.”
—Oscar Wilde (1854–1900)
“Would you convey my compliments to the purist who reads your proofs and tell him or her that I write in a sort of broken-down patois which is something like the way a Swiss waiter talks, and that when I split an infinitive, God damn it, I split it so it will stay split, and when I interrupt the velvety smoothness of my more or less literate syntax with a few sudden words of bar- room vernacular, that is done with the eyes wide open and the mind relaxed but attentive.”
—Raymond Chandler (1888–1959)