Cross Perspectives on Proof Systems and their Significance
May 3, 2012 – ENS, 45 rue d'Ulm 75005 Paris
Salle de séminaire du Cirphles, Département de Philosophie (sous-sol du pavillon Pasteur)
Program
| 9h30 - 10h30 | Patrick Blackburn (University of Roskilde) Hybrid Proof Theory |
| 10h30 - 11h30 | Zoran Petrić & Kosta Došen (Mathematical Institute, SANU) Invariants for Classifcation of Propositional Formulae |
| 11h30 - 11h45 | coffee break |
| 11h45 - 12h45 | Dale Miller (INRIA & LIX/Ecole Polytechnique) Focused sequent calculus proof systems |
| 12h45 - 14h30 | lunch |
| 14h30 - 15h30 | Francesca Poggiolesi (IHPST-Université Paris 1) Analytic Logic of Proofs |
| 15h30 - 16h30 | Didier Galmiche (LORIA–UHP Nancy 1) Label-free Calculi for Intuitionistic Modal Logics |
| 16h30 - 16h45 | coffee break |
| 16h45 - 17h45 | Thomas Piecha (Universität Tübingen) Symmetries in the sequent calculus |
| 17h45 - 18h | General discussion/conclusion |
Abstracts
Patrick Blackburn (University of Roskilde)
Hybrid Proof Theory
Abstract: In this talk I will discuss and motivate hybrid proof theory. Hybrid proof theory comes in a number of styles: I will try to make clear what is common to them all, but will concentrate on tableaux systems. Although this is a proof on truth theory, a lot of my observations will be semantic, since I believe the heart of hybrid proof theory to be the tools it offers for constructing Robinson diagrams. I shall try to indicate the flexibility this offers by noting both classical applications and recent work on indexicals.
For the most part I shall examine the two basic tools offered by hybrid logic, nominals and @-operators, since these are two most relevant to hybrid proof theory. Time permitting, however, I may talk a little about the more powerful downarrow binder and it proof-theoretic impact.
Zoran Petrić & Kosta Došen (Mathematical Institute, SANU)
Invariants for Classifcation of Propositional Formulae
Abstract: We investigate deductive systems for some fragments of propositional logics. These systems are given by categories whose objects are propositional formulae and whose arrows are the equivalence classes of deductions with respect to some meaningful notion of equality of deductions. All the deductions representing one arrow have as the premise the source of this arrow, and as the conclusion, the target of this arrow. In this talk we consider the problem of characterizing pairs of isomorphic formulae in these systems. It is easy to see that if two formulae are isomorphic, then they mutually imply each other, but the converse need not hold. The set of deductions having the same premise is in bijection (up to the equality of deductions) with the set of deduction having an isomorphic premise; the same holds for the set of deductions with the same conclusion. So the isomorphic formulae may be taken to have the same proof-theoretical meaning.
The problem of classification of formulae up to isomorphism is of the same interest for categorial proof theory as the problem of classification of objects in categories related to some other fields of mathematics, like for example, the classification of groups in group theory, or classification of topological spaces in topology. We give some techniques based on particular functors that yield some invariants, which may help to classify propositional formulae of various systems.
Dale Miller (INRIA & LIX/Ecole Polytechnique)
Focused sequent calculus proof systems
Abstract: Gentzen's sequent calculus provides an appealing framework for describing the proof-theoretic semantics of logical connectives and for establishing their meta-theory (such as cut-elimination). However, when one attempts to use the sequent calculus in applications, such as studying proof identity or using them in computer science, one is immediately struck by how tiny inference rules are and how unstructured sequent calculus proofs can be. I shall present some recent work on focused proof systems that, in a sense, provide a "chemistry" for inference that allows one to combine the "atoms of inference" provide by Gentzen (namely, the introduction rules and the structural rules) into possibly large "molecules of inference". The first, comprehensive focused proof system was designed by Andreoli for linear logic in 1992. Since then, focused proof systems for classical and intuitionistic logics have appeared. I will present LKF, a focused proof system for classical sequent calculus, and consider an extension to LKF that adds fixed points as logical connectives. In addition, I will show a number of proof theoretic consequences of the completeness of LKF and a number of computer science applications of large scale inference rules.
Francesca Poggiolesi (IHPST-Université Paris 1)
Analytic Logic of Proofs
Abstract: The old question discussed by Gödel in 1933/38 concerning the intended provability semantics of the classical modal logic S4 and intuitionistic logic IPC was finally settled by the logic of proofs introduced by Artemov (2001). The logic of proofs Lp is a natural extension of classical propositional logic by means of proof-carrying formulas. The operations on proofs in the logic of proofs suffice to recover the explicit provability of modal and intuitionistic logic.
We can prove many results about Lp: e.g. the deduction theorem, the substitution lemma and the internalisation of proofs. Moreover, Lp can be shown to be sound and complete with respect to the modal logic S4, and with respect to Peano Arithmetic.
There also exists a version of Lp with an intuitionistic base, namely Ilp, introduced in Artemov (2002). Unsurprisingly, analogous results can be obtained in the logic of proofs with an intuitionistic base. From a Gentzen-style point of view, we can formulate two similar sequent calculi for the two systems Lp and Ilp. Although simple and cut-free, these sequent calculi fail to satisfy certain properties that are standardly required from a "good" sequent calculus (in Poggiolesi (2010) and Wansing (1998), one can find a precise description of everything that is required from a "good" sequent calculus).
In this talk we aim at repairing this situation. We will do it by extending the standard sequent calculus and by using the means of the lambda-calculus. We will only work with the system Ilp.
(Joint work with B. Hill)
Didier Galmiche (LORIA–UHP Nancy 1)
Label-free Calculi for Intuitionistic Modal Logics
Abstract: In this talk we present label-free calculi for the intuitionistic modal logics obtained from the combinations of the axioms T, B, 4 and 5. They are based on a multi-contextual sequent structure, called T-sequent, that allows us to deal with such modal logics and to design label-free calculi with good properties. Moreover we show how they can provide new alternative decision procedures for these logics.
(Joint work with Yakoub Salhi)
Thomas Piecha (Universität Tübingen)
Symmetries in the sequent calculus
Abstract: Approaches to proof-theoretic semantics, such as the constructive semantics considered by Prawitz, rely on the idea that proof systems extend atomic systems. We argue that the restriction of atomic systems to systems of production rules, which cannot discharge assumptions, leads to the validation of non-constructive principles such as Peirce's rule. This demonstrates that the choice of the format of atomic systems is of crucial importance for proof-theoretic semantics, and that the common choice of production systems renders minimal logic incomplete with respect to this semantics. The 'global' justification of the logical rules of a proof system by a completeness result might thus not be feasible.
As an alternative, we will consider a 'local' justification of logical rules. We present a hypersequent system which is based on the principle of definitional reflection and its admissibility interpretation. Using this system, we show for the sequent calculus of minimal propositional logic that the left introduction rules are inverses of the right introduction rules in the sense of being admissible given the right introduction rules as primitive. Due to the symmetries in the sequent calculus, we can also show the converse direction, namely that the right introduction rules are admissible given the left introduction rules as primitive. This generalizes the well-known relationship between introduction and elimination rules in natural deduction to the framework of the sequent calculus. Besides definitional reflection, the hypersequent system contains structural rules; we will discuss their significance.
(Joint work with W. de Campos Sanz and P. Schroeder-Heister)
Local organizers
Francesca Poggiolesi (poggiolesi@gmail.com) and Mattia Petrolo (mattia.petrolo@univ-paris-diderot.fr)