There will be a short introduction to Gentzen's life and work at 11.00 by RD. The main event is the invited talk on Gentzen's Logical Calculi: Historical and Systematic Aspects by Jan von Plato (Helsinki) from 5--7 (as the weekly FLC seminar).
Talks will be split between Edgecliffe (The Scores) (11.00 to 12.50 and 17.00 to 19.00) and the Jack Cole Building (North Haugh) (14.15 to 16.45). Coffee will be served in Edgecliffe, from 10.30 to 11.00. Lunch will be served in the Jack Cole Building, from 13.00 to 14.15.
There are the following other invited talks (each followed by 5 minutes for questions):
To register, please contact RD.
Accommodation is available in the town if necessary. Travel information is available at the Universitty website. Parking for an 11.00 start is best achieved in the Bow Butts car park behind the Golf Museum, since it is free during the winter.Roy Dyckhoff and Stephen Read
Afshari: Proof theory of the infinite Ramsey Theorem
McAloon (1985) has shown that the infinite Ramsey Theorem is equivalent to the statement `for every set X and natural number n, the n-th Turing jump of X exists' over ACA_0. By analysing this theory we show that the infinite Ramsey Theorem has proof-theoretic strength epsilon_omega. The upper bound is obtained by means of cut elimination in a suitable infinitary calculus and the lower bound by extending the standard well-ordering proofs for ACA_0.
Brotherston: Display calculi for bunched logics
Display calculi, as formulated by Belnap in the 1980s, can be seen as natural successors of Gentzen's sequent calculi, suitable for the proof-theoretic analysis of substructural logics. They are characterised by the display property, which essentially states that proof judgments may be rearranged so that any chosen part appears alone on one side of the turnstile. Furthermore, this property guarantees cut-elimination whenever the rules of the calculus obey certain well-formedness conditions. In this talk, we seek to illustrate the advantages of display calculi by demonstrating their application to *bunched logics*, which originate in O'Hearn and Pym's BI and can be seen as the result of freely combining a standard (additive) propositional logic with a (multiplicative) linear logic. The practical interest in bunched logics stems from their Tarskian "resource" interpretation of formulas, as used e.g. in the heap model of separation logic. However, the cut-free sequent calculus for BI does not extend naturally to its important variants such as Boolean BI. We show how cut-eliminating display calculi may be obtained for all the principal varieties of bunched logic, and incidentally provide an explanation as to why sequent calculus solutions seem very unlikely to exist. See the speaker's A unified display proof theory for bunched logic (Submitted, 2009).
Chapman: Automation of Gentzen-style proof theory
Proofs in Structural Proof Theory frequently contain many similar cases. Whilst it may be possible in the literature to cover all such cases by proof methods like "similarly" and "trivial", a theorem prover requires all cases to be detailed in full. We present some formalisations of key metatheoretical results and new results about the invertibility of rules. The latter reduces the burden on the user of Isabelle, so that other formalisations can proceed more smoothly.
Dixon: Graphical Logic
I will present work in progress on a graphical, graph-based account of logic. This removes some symmetries between implication and conjunction which are present in traditional formulations of logic. I will present some properties of this logic and highlight how the proof terms correspond to computations. A curious feature of the logic is that, while it naturally describes linear logic, constants in the form of basic graphs can be added to make make it intuitionistic or classical. An implementation and formalisation of this logic are underway.
Leigh: Proof theory and theories of truth
Augmenting the language of first-order arithmetic with an additional predicate symbol allows one to formalise notions of `truth'. However the question of what principles of truth one allows is not so straightforward. Some apparently rich theories of axiomatic truth are relatively weak, whereas others built upon only a few principles are proof-theoretically very strong. In this talk I will introduce a sequent calculus for analysing theories of truth enabling one to determine (with relative ease) the proof-theoretic strength of a number of classical and intuitionistic truth theories.
Murzi: Proof-theoretic harmony and the meaning of the logical constants
Gentzen famously argued that introduction rules are meaning-constitutive, and eliminations are nothing but their 'consequences': they must respect the meanings defined by the corresponding introductions. The so-called general elimination account of harmony aims at making Gentzen's ideas more precise by offering an effective procedure for deriving harmonious elimination rules given arbitrary introductions. Symmetry considerations, though, suggest that, if introductions and eliminations are in harmony, one should likewise be able to derive introductions from eliminations. Yet, general elimination harmony doesn't really give us means for determining canonical grounds given arbitrary canonical consequences. What has gone wrong? I show how classical logic can be validated on a conception of harmony---harmony as full invertibility, as I shall call it---according to which both introductions and eliminations can fully determine meanings.
von Plato: Gentzen's logical calculi: historical and systematic aspects
Recently found documents shed new light on Gentzen's discovery of natural deduction and sequent calculus. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. The origin of sequent calculus lies, as has been known, in part in the work of Paul Hertz. An early handwritten manuscript of Gentzen's thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was the second component in the discovery of sequent calculus. A system intermediate between the standard sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934-35. On the whole, it is argued that the central component in Gentzen's work on logical calculi was the use of a tree form for derivations. It permits to compose derivations and to permute the order of application of rules, with a full control over the structure of derivations as a result.
Simpson: Non-well-founded proof theory
The standard approach to inductive (and coinductive) reasoning is to use proof systems with explicit induction (and coinduction) rules. Such systems have been comprehensively studied and are well understood. An alternative approach to such reasoning is to allow infinite non-well-founded proofs that implement a form of argument by "infinite descent". This approach was pioneered in the study of propositional fixed-point logics (the modal-mu calculus). As James Brotherston and I observed (Brotherston, PhD thesis 2006; Brotherston and S., LICS 2007), it adapts naturally to a sequent-calculus setting and to the context of inductive (and coinductive) reasoning.
In this talk, I will introduce the method of non-well-founded proof as an approach to (co)inductive theorem proving. The focus will be on non-well-founded sequent calculi as a general paradigm for (co)inductive proof - that is, independently of any one specific logic and proof system. There are several unresolved questions and directions for research in this area, and I will highlight some of these.Stirton: Gentzen's second consistency proof and its afterlife
It is perhaps not as well-known as it ought to be that Gentzen invented (at least) two distinct cut-elimination methods applicable to first-order logic. The less well-known one is presented in his 1938 article "New version of the consistency proof". I will try to explain why this method is less perspicuous than the better-known one presented in his "Investigations concerning logical inference" but also has a wider range of applications.