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

Deadline for submissions: March 20, 2012

Tutorial speakers: :

George Metcalfe (University of Bern): Admissible Rules in Logic and Algebra
Sara Negri (University of Helsinki)

Invited speakers :

Arnon Avron (University of Tel-Aviv): Construction of Cut-free Sequent Calculi for Paraconsistent Logics
Kosta Dosen (University of Belgrade): The Main Question of General Proof Theory
Hermann Ruge Jervell (University of Oslo): Cut elimination
Simone Martini (University of Bologna)
Alex Simpson (University of Edinburgh)
Jan von Plato (University of Helsinki)

Contributed Talks: To be announced

Participants: To be announced

Programme: To be announced

Venue:

Dipartimento di Filosofia, via Paoli 15, Pisa.

Practical information (accommodation, transport, etc.): Available soon.

Abstracts:

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.

Herman Jervell (University of Oslo): Cut elimination