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:
“The source of Pyrrhonism comes from failing to distinguish between a demonstration, a proof and a probability. A demonstration supposes that the contradictory idea is impossible; a proof of fact is where all the reasons lead to belief, without there being any pretext for doubt; a probability is where the reasons for belief are stronger than those for doubting.”
—Andrew Michael Ramsay (1686–1743)
“The theory of rights enables us to rise and overthrow obstacles, but not to found a strong and lasting accord between all the elements which compose the nation.”
—Giuseppe Mazzini (1805–1872)
“Euphemisms are not, as many young people think, useless verbiage for that which can and should be said bluntly; they are like secret agents on a delicate mission, they must airily pass by a stinking mess with barely so much as a nod of the head, make their point of constructive criticism and continue on in calm forbearance. Euphemisms are unpleasant truths wearing diplomatic cologne.”
—Quentin Crisp (b. 1908)
“It is a monstrous thing to force a child to learn Latin or Greek or mathematics on the ground that they are an indispensable gymnastic for the mental powers. It would be monstrous even if it were true.”
—George Bernard Shaw (1856–1950)