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:
“When children feel good about themselves, it’s like a snowball rolling downhill. They are continually able to recognize and integrate new proof of their value as they grow and mature.”
—Stephanie Martson (20th century)
“No theory is good unless it permits, not rest, but the greatest work. No theory is good except on condition that one use it to go on beyond.”
—André Gide (1869–1951)
“Once we begin to appreciate that the apparent destructiveness of the toddler in taking apart a flower or knocking down sand castles is in fact a constructive effort to understand unity, we are able to revise our view of the situation, moving from reprimand and prohibition to the intelligent channeling of his efforts and the fostering of discovery.”
—Polly Berrien Berends (20th century)
“Mathematics alone make us feel the limits of our intelligence. For we can always suppose in the case of an experiment that it is inexplicable because we don’t happen to have all the data. In mathematics we have all the data ... and yet we don’t understand. We always come back to the contemplation of our human wretchedness. What force is in relation to our will, the impenetrable opacity of mathematics is in relation to our intelligence.”
—Simone Weil (1909–1943)