According to Buss in the Handbook of Proof Theory, the principal tasks of Proof Theory can be summarized as follows.
- First, to formulate systems of logic and sets of axioms which are appropriate for formalizing mathematical proofs and to characterize what results of mathematics follow from certain axioms; or, in other words, to investigate the proof-theoretic strength of particular formal systems.
- Second, to study the structure of formal proofs; for instance, to find normal forms for proofs and to establish syntactic facts about proofs. This is the study of proofs as objects of independent interest.
- Third, to study what kind of additional information can be extracted from proofs beyond the truth of the theorem being proved. In certain cases, proofs may contain computational or constructive information.
- Fourth, to study how best to construct formal proofs; e.g., what kinds of proofs can be efficiently generated by computers?
Isn't this too restrictive?
