Proof Theory and Constructive Mathematics
Proof theory is the study of formal proofs in various logical deduction systems. These proofs are represented as formal mathematical objects, facilitating their analysis by mathematical techniques. Several deduction systems are commonly considered, including Hilbert-style deduction systems, systems of natural deduction, and the sequent calculus developed by Gentzen.
The study of constructive mathematics, in the context of mathematical logic, includes the study of systems in non-classical logic such as intuitionistic logic, as well as the study of predicative systems. An early proponent of predicativism was Hermann Weyl, who showed it is possible to develop a large part of real analysis using only predicative methods (Weyl 1918).
Because proofs are entirely finitary, whereas truth in a structure is not, it is common for work in constructive mathematics to emphasize provability. The relationship between provability in classical (or nonconstructive) systems and provability in intuitionistic (or constructive, respectively) systems is of particular interest. Results such as the Gödel–Gentzen negative translation show that it is possible to embed (or translate) classical logic into intuitionistic logic, allowing some properties about intuitionistic proofs to be transferred back to classical proofs.
Recent developments in proof theory include the study of proof mining by Ulrich Kohlenbach and the study of proof-theoretic ordinals by Michael Rathjen.
Read more about this topic: Mathematical Logic
Famous quotes containing the words proof, theory, constructive and/or mathematics:
“If some books are deemed most baneful and their sale forbid, how, then, with deadlier facts, not dreams of doting men? Those whom books will hurt will not be proof against events. Events, not books, should be forbid.”
—Herman Melville (1819–1891)
“Hygiene is the corruption of medicine by morality. It is impossible to find a hygienest who does not debase his theory of the healthful with a theory of the virtuous.... The true aim of medicine is not to make men virtuous; it is to safeguard and rescue them from the consequences of their vices.”
—H.L. (Henry Lewis)
“The measure discriminates definitely against products which make up what has been universally considered a program of safe farming. The bill upholds as ideals of American farming the men who grow cotton, corn, rice, swine, tobacco, or wheat and nothing else. These are to be given special favors at the expense of the farmer who has toiled for years to build up a constructive farming enterprise to include a variety of crops and livestock.”
—Calvin Coolidge (1872–1933)
“In mathematics he was greater
Than Tycho Brahe, or Erra Pater:
For he, by geometric scale,
Could take the size of pots of ale;
Resolve, by sines and tangents straight,
If bread and butter wanted weight;
And wisely tell what hour o’ th’ day
The clock doth strike, by algebra.”
—Samuel Butler (1612–1680)