Sommersemester 2007
Tutorial on Proof-Theoretic Semantics, 2nd World Congress and School on Universal Logic, Xi'an, 16-19 August 2007
Contents
0. Preliminaries
- Gentzen-style natural deduction
- Philosophical preliminaries
I. E rules as syntactical functions of I rules
- Generalized rules for logical constants
- The adequacy of generalized rules
- Case study: Negative circularity
- Natural deduction with atomic rules
II. Proof-theoretic validity
- Proofs, rules and consequence
- The origin of proof-theoretic validity: computability
- Prawitz's definition of validity
- Validity based on E rules
- General proof structures and justifications
- The trivialization problem
III. Local inversion and reflection
- Critique of globalization
- The model of the sequent calculus
- Systems based on atomic clauses (inductive definitions)
- Adequacy
- Variants of definitional reflection
- Beyond definitional reflection
- Partial and global meaning
- Conclusion
Abstract
Proof-Theoretic Semantics (PTS) is an alternative of model-theoretic (or truth-condition) semantics. It is based on the idea that the central notion in terms of which meanings are assigned to expressions is that of proof rather than truth. In this sense PTS is inferential rather than denotational in spirit. Although the claim that meaning is use has been quite prominent in philosophy for more than half a century, the model-theoretic approach has always dominated formal semantics. This is, as I see it, due to the fact that for denotational semantics very sophisticated formal theories are available, going back to Tarski's definition of truth, whereas "meaning is use" has often been just a slogan without much formal underpinning. However, within general proof theory several formal approaches to PTS have been developed which promise to provide a 'real' alternative to the model-theoretic approach. They are all based on ideas of Gentzen-style proof-theory, which are then turned into logico-philosophical principles.
After recalling certain basics from the theory of natural deduction, this tutorial presents in its first part the idea of generalized introduction and elimination rules for logical or non-logical (atomic) constants, discusses adequacy criteria for such rules and investigates, as a case study, the example of negative circularity as it occurs with the paradoxes.
In its second part it develops and discusses the Dummett-Prawitz approach to PTS and their definition of proof-theoretic validity. It discusses various options of how to define the validity of proofs and relates them to corresponding notions of logical consequence. It puts particular emphasis on the "universal" aspects of these ideas, dealing with general proof structures and arbitrary proof reduction systems as models with respect to which validity is defined.
The third part is devoted to definitional and clausal approaches to PTS, partly developed by the instructor himself jointly with Lars Hallnäs (Gothenburg). This approach puts the validity of rules and inference steps (rather than that of whole proofs) first. As compared with the Dummett-Prawitz approach, it is local rather than global, thus not requiring global properties of proofs like normalization or cut elimination to hold in every possible case. Technically it implies a shift from natural deduction to the sequent calculus as the basic model of reasoning. This allows in particular a more general way of dealing with assumptions and negation, including their substructural features. This approach is is not restricted to logical constants but uses clausal definitions in a universal sense as the basis of reasoning, which means that it goes far beyond logic in the narrower sense. Interesting applications are theories of equality, circular reasoning, universal theories of denial and negation, and extensions of logic programming. Whether cut is eliminable in the various theories discussed is always an interesting problem, though not crucial for the approach to be meaningful.