![[Arno]](arno.jpg)
Pisa Summer Workshop on Proof Theory
Pisa, Italy, 12-15 June 2012
Organizers: Department of Philosophy, University of Pisa;
Department of Philosophy, University of Helsinki
Call for papers
Aimed at understanding the structure of mathematical proofs, proof theory has undergone
different phases: it has been reductive, general, structural. Especially thanks to
sequent calculus formalizations, deep results were attained as far as proofs in pure
logic and arithmetic are concerned. Through significant connections with computer
science, proof theory contributed to the birth of new areas of research outside
traditional mathematics, such as the verification of correctness of computer programs.
Natural deduction has led to the Curry-Howard correspondence and to connections with
functional programming, and sequent calculus is often used in systems of automatic proof
search, as in logic programming. Rooted in general proof theory, a proof-theoretic
semantics has been recently developed as an alternative to standard denotational
truth-condition semantics.
The workshop will focus mainly on proof systems, but we aim at touching several areas of
proof-theoretical research.
The workshop will be framed in two six-hour tutorials, six one-hour lectures, and is open
to half-hour contributed talks. People interested to present a paper in the workshop may
send a title with a short abstract to one of the following e-mail addresses:
moriconi[at]fls.unipi.it
tesconi[at]fls.unipi.it
sara.negri[at]helsinki.fi
jan.vonplato[at]helsinki.fi
Tutorial speakers: :
Invited speakers :
Participants: To be announced
Venue:
Dipartimento di Filosofia,
via Paoli 15, Pisa
Social programme and practical information (accommodation, transport, etc.):
Social dinner on Thursday 14 at 20.00: Ristorante la Clessidra, via del Castelletto 26/30, directions
Official Tourism Website for Pisa Province
Civic Network Pisa
Visit Pisa
Trenitalia
Please notice that the Workshop takes place in a very special time of the
year for the town of Pisa, being so close to the celebration of the patron
saint's feast day:
La luminara
The magic of the luminara
Therefore, we warmly recommend you to reserve your accommodation as soon as
possible.
Though there is no formal agreement or committment, the following hotels
have been informed and will be glad to accommodate partecipants of Pisa
Summer Workshop:
Hotel Leonardo Pisa
Hotel Royal Victoria
Hotel Verdi
Gand Hotel Bonanno
Registration
(early registration deadline May 30)
Abstracts:
Tutorials:
George Metcalfe (University of Bern): Admissible Rules in Logic and Algebra
Abstract: The aim of this tutorial is to provide some insight into the fascinating and
varied roles played by admissible rules in logic and algebra, focusing
in particular on proof-theoretic applications and frameworks.
The concept of admissibility was introduced explicitly by Lorenzen in the 1950s
in the context of intuitionistic logic, but played an important role already in
the earlier work of Gentzen, Whitman, and others. Informally, a rule
is admissible for a logic (understood as a consequence relation) if adding it to the
system produces no new theorems. Equivalently, the rule is admissible if for each
instance of the rule, whenever the premises are theorems, the conclusion is also a
theorem. In algebra, such rules correspond to quasi-equations holding in free algebras,
while from a computer science perspective, admissibility is intimately related to, and
in certain cases may be reduced to, equational unification.
For classical logic, derivability and admissibility coincide: the logic is structurally
complete. However, for many non-classical logics - in particular, intermediate,
modal, many-valued, and substructural logics - this is no longer the case.
An interesting and potentially useful task is then to investigate questions of
decidability, complexity, finite axiomatizability, etc. for these rules. Moreover,
admissible non-derivable rules may represent "hidden properties" of the logic,
which can then be used to establish completeness results or shorten proofs.
Sara Negri (University of Helsinki): Proof Systems for Modal and Epistemic Logics
Abstract: The semantics of modal logic has received a general treatment since late fifties/early
sixties, after the introduction of possible world semantics by Hintikka, Kripke, and
others. On the other hand, the proof theory has not had such a systematic development,
and many simple questions have remained unsolved for decades.
The tutorial will present a general method for building proof systems in compliance with
the
desiderata of proof-theoretic semantics for a wide variety of modal, non-classical
logics, provability, and epistemic logics. The proof systems will be also used to
establish in a uniform way completeness, decidability, and faithful embedding results.
Invited talks:
Arnon Avron (University of Tel Aviv): Construction of Cut-free Sequent Calculi for Paraconsistent Logics
Abstract: We describe a general method for a systematic
and modular generation of cut-free calculi for thousands of
paraconsistent logics. The method relies on the use of
non-deterministic semantics for these logics.
Kosta Dosen (University of Belgrade): The Main Question of General Proof Theory
Abstract: General proof theory deals with the structure of proofs, as exhibited, for example, in the Curry-Howard correspondence, and not with the strength of proofs measured by ordinals, which is what one finds in proof theory that arose out of Hilbert's programme. This theory addresses the question "What is a proof" by dealing with questions related to normal forms of proofs, and in particular with the question of identity criteria for proofs, which may be found, at least implicitly, in Hilbert's 24th problem. In general proof theory one looks for an algebra of proofs, and for that one concentrates on the operations of this algebra, which come with the inference rules. As an equational theory, the algebra of proofs involves the question of identity criteria for proofs, the main question of general proof theory. Much of general proof theory is the field of categorial proof theory, where through results called coherence results, which provide a model theory for equality of proofs, logic finds new ties with geometry, topology and algebra.
Hermann Ruge Jervell (University of Oslo): Cut elimination
Abstract: We investigate the combinatorics involved in cut elimination.
As a tool we use Gentzen games which is helpful to see why the cut
elimination terminate and how we get the estimates of the complexity of
cut elimination for various systems.
Simone Martini (University of Bologna): Implicit Computational Complexity and the quest for intensional completeness
Abstract: ICC aims to the description of complexity phenomena based on language restrictions,
and not on external measure conditions or on explicit machine models.
Proof-theory has given several ICC characterizations of complexity classes,
in which any function computed in a certain bound is represented by a proof in the calculus.
A system is intensionally complete for a complexity class C if any
algorithm computing a function in C is represented by a proof in the calculus.
Jan von Plato (University of Helsinki): The interpretation of cuts in natural deduction
Abstract: Arbitrary derivations in sequent calculus with cuts are interpreted in terms of
natural deduction. The interpretation consists of a translation from sequent derivations
to natural derivations.
Alex Simpson (University of Edinburgh): Proof systems for intuitionistic modal logics revisited
Abstract: For classical modal logic, there is general agreement on the main
calculi of interest. Moreover, for most such calculi, well-behaved
structural proof systems (e.g., sequent calculi) are available in many
styles (e.g., ordinary sequents, hypersequents, labelled sequents,
etc.). In contrast, for intuitionistic modal logic, there is no
consensus on the main calculi, and, for each choice of calculus, the
range of applicable proof styles seems much more constrained. In this
talk, I shall present a personal perspective on the state of affairs.
One topic I intend to focus on, in particular, is the tension between
labelled and unlabelled approaches to modal proof systems.
- Jesse Alama: Experiments with obvious inferences in formal proofs
- Michael Arndt, Laura Tesconi: A Framework of Explicit Composition
- Luca Bellotti (joint
work with Lorenzo Carlucci): Von Neumann's consistency proof
- Agata Ciabattoni (joint work with Matthias Baaz): Proof theory for non-classical logics: a negative result
- Vincent Degauquier: Cut-elimination, Excluded Middle and Non-contradiction
- José Espírito Santo: Intuitionistic asymmetry: how the classical CBN/CBV duality breaks
- Jeroen Goudsmit: Admissible Rules of Gabbay-de Jongh Logics
- Bogdan Dicher: Sequent calculus, bilateralism and logical consequence
- Antonino Drago: Proof theory in the case of a change in the kind of logic. The crucial role played by Leibniz' principle of sufficient reason
- Nissim Francez: Relevant Harmony
- Jens Ulrik Hansen: Tableau systems for Hybrid public announcement logic with distributed knowledge
- Yoichi Hirai: A Lambda Calculus for Goedel-Dummett Logic Capturing Waitfreedom
- Rosalie Iemhoff: Unification in modal and intermediate logics
- Roman Krenicky: A 2-Categorical Notion of Proof Equality
- Björn Lellmann: Constructing Cut-free Sequent Systems with Context Restrictions
- Tadeusz Litak: Extended Curry-Howard correspondence for constructive Loeb logics
- Dale Miller: Describing canonical proof structures by abstracting sequent calculus proofs
- Pierluigi Minari: Variations on G3K
- Alberto Momigliano (joint work with Alessandro Avellone and Camillo Fiorentini):
Focusing, Termination and the Gödel-Dummett Logic
- Franco Parlamento (joint work with Flavio Previale): The subterm property for the sequent calculus with equality
- Dirk Pattinson: Labelled Sequent Calculi for Many-Valued Modal
Logics
- Luis Pinto (joint work with José Espírito Santo, Ralph Matthes, and Koji
Nakazawa): Monadic translation of classical and intuitionistic sequent calculus
- Carlo Proietti: Non-classical Modal Logics and tableau testing
- Giselle Reis (joint work with Vivek Nigam and Elaine Pimentel): An Extended Framework for Specifying and Reasoning about Proof Systems
- Allard Tamminga (joint work with Barteld Kooi): Correspondence Theory for the Logic of Paradox
- Luca Tranchini: Proof-theoretic semantics, paradoxes and the distinction between sense and denotation
- Diego Valota: Building Strongest Deductive Interpolants in Nilpotent Minimum Logic
- Anna Zamansky (joint work with Matthias Baaz and Ori Lahav): Effective Finite-valued Semantics for Labelled Calculi
Last updated on 24.4.2012 by Sara Negri