Proof Theory:
In logic: The theory of
proofs. The mathematician Hilbert formulated the ideal that
in mathematics every
true mathematical
statement would get its
deductive proof, and in the first four
decades of the 20th century mathematicians and logicians spend a lot of
time on establishing systems of proof to do this and to clarify the
whole notion of mathematical deductive proof.
The clarification succeeded, and several new and useful formats for
mathematical proofs were found, notably Gentzen's sequent systems and
techniques of natural deduction
and Beth's semantic tableaux.
The notion that all mathematically true statements in a system of
mathematical assumptions could and would eventually find their
deductive proof was refuted by Gödel,
who proved that in mathematical systems that are strong enough to
contain arithmetic, one can formulate statements in the language of the
system that assert their own unprovability, and that therefore cannot be
validly proved in the system (if it is
consistent) and must be intuitively true (since the statement
asserts what is the case). See
Gödel's Theorems.
Modern introductions to mathematical logic contain normally
expositions of several techniques of proof. Kleene's 'Mathematical
Logic' is one such exposition, that explains both axiomatic proofs, and
proofs by natural deduction and by sequents. Smullyan's 'First Order
Logic' surrects the whole basic theory of firstorder logic using
tableaux methods. Gentzen's 'Untersuchungen über das logische
Schlieszen' is still worth reading and can be found in many collections
(such as Berka & Kreiser). And one textbook with elegant and fargoing
systems is Schütte's 'Proof Theory'.
