Wednesday, April 16, 2014

Tasks of Proof Theory?

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? 

1 comment:

  1. It seems that the definition claiming that proof theory is primarily a syntactic investigation, and not including semantic based approaches.