Proof-theoretic semantics

Advanced Course, ESSLLI, Bordeaux, 27-31 July 2009

This page as pdf — Contents — Summary — Materials

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 and the problem of procedures

III. Local inversion and reflection

• Critique of globalization
• The model of the sequent calculus
• Bidirectional natural deduction
• Systems based on atomic clauses (inductive definitions)
• Adequacy
• Variants of definitional reflection
• Beyond definitional reflection
• Partial and global meaning

IV. Assertion and denial

• Proofs vs. refutations: Asymmetry
• Duality in logic
• Dualizing proof-theoretic semantics
• Explicit denial clauses
• Balanced definitions
• Assumption clauses

V. Generalized definitional reflection and the sequent calculus

• Duality in the sequent calculus
• Definitional reflection and hypersequents
• Reflection based on explicit definitions: Basic Logic
• Generalized definitional reflection and definitional interaction
• Outlook: Bidirectionality and dialogues

Summary

Proof-Theoretic Semantics (PTS) is an alternative to 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 "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 course 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 as developed by the instructor himself jointly with Lars Hallnäs (Gothenburg) using the principle of "definitional reflection". This approach puts the validity of rules and inference steps (rather than that of whole proofs) first. As compared to the Dummett-Prawitz approach, it is local rather than global and does not require that global properties of proofs such as normalization or cut elimination hold in every possible case. This approach is is not restricted to logical constants but uses clausal definitions 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.

The fourth part deals with the treatment of denial and negation in the general framework developed. After making precise in which sense duality principles, which are well-known from classical logic, also hold in the constructive realm, it pleads for a "direct" treatment of negation in terms of rules for the denial of sentences, where the denial operator only occurs in outermost position (and thus cannot be iterated). This leads to a framework of clausal definitions for assertion and denial, formally related to extended logic programming. Principles of definitional reflection and definitional closure with respect to such definitions are discussed. Overall, this approach is intended as an alternative to the "indirect" approach to negation prevailing in the intuitionistic tradition.

The approach favoured is "bidirectional" in that assertions and assumptions are treated on par. Technically, this implies a shift from natural deduction to the sequent calculus as the basic model of reasoning, or at least to some bidirectional variant of natural deduction. Therefore, in the final fifth part, the idea of definitional reflection is used to deal with the symmetry features of the sequent calculus, in which the duality between assertions and assumptions is much more explicit than in natural deduction. Various approaches are discussed and related to existing theories. Particular emphasis is given to substructural issues.

A tutorial comprising (essentially) parts I-III of the present course was given at the School on Universal Logic, Xi'an (China) in August 2007. Parts IV and V are new.

Materials

General

• Proof-Theoretic versus Model-Theoretic Consequence. In: M. Peliš (ed.), The Logica Yearbook 2007, Prague: Filosofia 2008, 187-200. Draft: pdf

Part I: E rules as functions of I rules

• A natural extension of natural deduction. Journal of Symbolic Logic 49 (1984), 1284-1300. pdf
• Structural Frameworks with Higher-Level Rules. Philosophical Investigations on the Foundations of Formal Reasoning. (Habilitationsschrift.) Konstanz 1987. pdf

Part II: Proof-theoretic validity

• Validity Concepts in Proof-Theoretic Semantics. In: R. Kahle, P. Schroeder-Heister (eds.), Proof-Theoretic Semantics. Synthese 148 (2006), 525-571. pdf

Part III: Local inversion and reflection

• Rules of definitional reflection. In: Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (Montreal 1993), Los Alamitos 1993, 222-232. pdf
• Generalized Definitional Reflection and the Inversion Principle. Logica Universalis 1 (2007), 355-376. pdf

Part IV: Assertion and denial

• Definitional Reasoning in Proof-Theoretic Semantics and the Square of Opposition. Proceedings of the International Congress on the Square of Opposition (Montreux, June 1-3, 2007). pdf

Part V: Generalized definitional reflection and the sequent calculus

• Sequent Calculi and Bidirectional Natural Deduction: On the Proper Basis of Proof-Theoretic Semantics. In: M. Peliš (ed.), The Logica Yearbook 2008, London: College Publications 2009. pdf
• Wagner de Campos Sanz & Thomas Piecha, Inversion by Definitional Reflection and the Admissibility of Logical Rules. The Review of Symbolic Logic 2 (2009), 550-569. pdf (© 2009 Association for Symbolic Logic)

Further materials are available from the (password protected) webpage http://ls.cs.uni-tuebingen.de/esslli/esslli09/materials.html.

The password will be disclosed to those who attend or plan to attend my course.

Email: psh@informatik.uni-tuebingen.de.