N.B.: Links to files are being added.
Elementary proof theory has its origins in Hilbert's program that in its beginnings tried to study the structure of mathematical proofs by finitary means. This led to success in pure logic, in Gentzen's systems of natural deduction and sequent calculi, but failed whenever arithmetic with full induction was part of a system.
The first results of our work in elementary proof theory appeared in 1998. One could think that seventy years after Gentzen, there can not be much to say about the proof theory of propositional and predicate logic. Instead, even the relation between Gentzen's two main formulations, natural deduction and sequent calculus, has not been completely cleared before. Within sequent calculus, it has been possible to give new formulations of the logical rules with interesting properties, such as our ``sequent calculus in natural deduction style,'' as well as new proofs of old results. A prime example of the latter is the proof of Gentzen's cut elimination theorem without the ``mix rule,'' Gentzen's method for hiding the problematic case of cut preceded by contraction. A reviewer said of our proof that ``it is surprising that it has taken over half a century since Gentzen's original work to reach this result.'' (M. Takano, Math. Reviews 2002).
The second main topic in our work has been the extension of proof analysis in sequent calculi of pure logic to calculi with additional rules that correspond to mathematical axioms. It has been a widespread belief that this is impossible, that ``cut elimination fails in the presence of axioms.'' Unaware of this, we found a way of converting universal axioms into sequent calculus rules and proved that Gentzen's cut elimination extends to these, with no cuts left even on atomic formulas. In cut-free derivations, logical rules can be applied only after the mathematical ones. In a root-first proof search, the latter can instantiate new terms in premisses. However, several theories obey a ``subterm property,'' analogous to Gentzen's subformula property, by which all the terms in minimum-size derivations are terms in the assumptions or conclusion. By this property, the structure of derivations is mastered completely. Theories that have the property include linear order, lattice theory, and projective and affine geometry. As byproducts, bounds for proof search for various classes of formulas are obtained, as well as syntactic proofs of consistency and independence. For example, a two-line failed proof search shows the independence of Euclid's parallel postulate from the other affine axioms.
At present, the program of converting mathematical axioms into rules has been carried through for theories the axioms of which are what are known as geometric implications in categorical terms. Our program can be seen as a contribution to Hilbert's original program of metamathematics pursued by elementary means. Successful proof analysis of abstract mathematical reasoning by elementary means is possible, provided that natural numbers are not part of the theory to be analyzed.
1. Sara Negri: Sequent calculus proof theory of intuitionistic apartness and order relations, downloadable from the publisher, Archive for Mathematical Logic, vol. 38 (1999), pp. 521-547.
Shows how the axioms for order and apartness relations can be converted into mathematical rules by which classical and intuitionistic sequent calculi can be extended. These extensions obey a strict cut elimination property: No cuts even on atoms are needed. In 1997, when the result was presented, it was considered an impossibility by many. As an application of cut elimination, conservativity results were obtained. In particular, the theory of an apartness relation is conservative over the theory of equality for formulas with all atoms negated. The second edition of Troelstra and Schwichtenberg's Basic Proof Theory contains a somewhat different proof of this result and an exposition of the general method in 2 below.
2. Sara Negri and Jan von Plato: Cut elimination in the presence of axioms, available here, The Bulletin of Symbolic Logic, vol. 4 (1998), pp. 418-435.
This paper, the title of which derives from Girard's dictum, ``Cut elimination fails in the presence of axioms,'' generalizes 1 into extensions of sequent calculi by any theories that permit a quantifier-free formulation.
3. Jan von Plato: A structural proof theory of geometry, ms. 1998.
Applies the results of 2 to plane affine geometry, with a syntactic proof of the independence of Euclid's parallel postulate. The results are mainly contained in item 12, section 6.6. A greatly improved approach is in item 21.
4. Jan von Plato: Proof theory of full classical propositional logic, ms. 1998.
A single succedent sequent calculus for classical propositional logic is presented, with cut elimination and the subformula property. The calculus also translates to natural deduction, with Glivenko's theorem obtained through an explicit proof transformation. The results are contained in item 12, section 8.6.
5. Sara Negri and Roy Dyckhoff: Admissibility of structural rules for contraction-free systems of intuitionistic logic, ps.gz file, The Journal of Symbolic Logic, vol. 65 (2000), pp. 1499-1518.
Dyckhoff's intuitionistic sequent calculus G4 is equivalent to the standard contraction-free calculus G3. However, adding rules corresponding to axioms to equivalent calculi can destroy the equivalence. It therefore became important to find a direct proof of cut elimination for G4, instead of the indirect argument given by Dyckhoff in 1992.
6. Sara Negri and Roy Dyckhoff: Admissibility of structural rules for extensions of contraction-free systems of intuitionistic logic, available here, Logic Journal of the IGPL, vol. 9 (2001), pp. 541-548.
It is shown that mathematical axioms converted into rules can be added to G4 with cut elimination maintained.
7. Jan von Plato: A problem of normal form in natural deduction, Mathematical Logic Quarterly, vol. 46 (2000), pp. 121-124.
Jan Ekman found a derivation in natural deduction with a substantial redundant part, the deletion of which makes the proof non-normal. It is shown that this phenomenon is caused by a non-normality inherent in the standard implication elimination rule.
8. Jan von Plato: A proof of Gentzen's Hauptsatz without multicut, Archive for Mathematical Logic, vol. 40 (2001), pp. 9-18.
Gentzen's original proof of cut elimination used a rule of multicut (or ``mix rule'') in which several copies of the cut formula were removed in one step. It is shown how to eliminate the standard cut rule directly.
9. Jan von Plato: Natural deduction with general elimination rules, Archive for Mathematical Logic, vol. 40 (2001), pp. 541-567.
All elimination rules are written in the way of disjunction elimination, with an arbitrary consequence. Normality becomes defined as: all major premisses of elimination rules are assumptions. Isomorphism between normal and cut-free derivations follows, with weakening and contraction interpreted as vacuous and multiple discharge. After the paper appeared, several people brought to our attention earlier discovery, during the 90's, of the system of general elimination rules, but without substantial results. It turned out that the first to have published them was Roy Dyckhoff in 1988. Felix Joachimski and Ralph Matthes proved (AML, in press) strong normalization for ND with general elimination rules through term assignment and an inductive definition of strongly normalizing terms, which convinced many of the advantage of using these rules.
10. Sara Negri: A sequent calculus for constructive ordered fields, in P. Schuster et al. (eds) Reuniting the Antipodes. Constructive and Nonstandard Views of the Continuum, pp. 143-155, Kluwer, Dordrecht 2001.
The method of extension of sequent calculi by mathematical rules is applied to the theory of constructive ordered fields, with cut elimination as the main result.
11. Sara Negri and Jan von Plato: Sequent calculus in natural deduction style, The Journal of Symbolic Logic, vol. 65 (2001), pp. 1803-1816.
The rules of sequent calculus are written so that weakening and contraction are implicit in them, as in natural deduction. A much more deterministic cut elimination procedure than in earlier sequent calculi follows.
12. Sara Negri and Jan von Plato: Structural Proof Theory , Contents, Cambridge University Press 2001, xvii + 257 p.
13. Sara Negri: Conservativity of apartness over equality, revisited, Research Report CS/99/4, Computer Science Division, St Andrews University, 1999, available here.
The conservativity of apartness over equality in 1 was originally proved for Dyckhoff's calculus G4, whereas in 1 a proof for G3 was given. However, for the proof using G4, a direct cut elimination result was required, found only later and presented in 5. This paper gives the original proof.
14. Sara Negri: A normalizing system of natural deduction for intuitionistic linear logic, downloadable from the publisher, Archive for Mathematical Logic, vol. 41 (2002), pp. 789-810.
General elimination rules of item 9 are applied to linear logic which gives a calculus with no sequent calculus style features (e.g., no rule of weakening), and with no anomalies for derivations in normal form.
15. Sara Negri: Varieties of linear calculi, online here, Journal of Philosophical Logic, vol. 31 (2002), pp. 569-590.
A general logical calculus for linear logic is presented that gives sequent calculi and their inversions and systems of natural deduction as special cases. The calculus derives from a corresponding calculus for standard predicate logic in the Conclusion of item 12.
16. Jan von Plato: Rereading Gentzen, Synthese, in press.
This paper collects together observations from a close reading of Gentzen's papers.
17. Jan von Plato: Gentzen und die Beweistheorie, in E. Menzler-Trott, Gentzens Problem: mathematische Logik im nationalsozialistischen Deutschland, pp. 313-328, Birkhäuser, Basel 2001.
An appendix to Menzler-Trott's biography that presents the situation in logic and foundations of mathematics when Gentzen started his work, then discusses his achievements and where they led.
18. Jan von Plato: Proof theory of classical and intuitionistic logic, in L. Haaparanta, ed, History of Modern Logic, Oxford University Press, in press.
A survey of the development of the proof theory of predicate logic from axiomatic treatments through Gentzen to the Curry-Howard isomorphism.
19. Sara Negri, Jan von Plato, and Thierry Coquand: Proof-theoretical analysis of order relations, ps file, Archive for Mathematical Logic, in press. Also available from Reports Institut Mittag-Leffler, Preprint series: Mathematical Logic - 2000/2001, no. 18.
In items 1 and 2, mathematical rules operate on the antecedent parts of sequents, here a dual is found for the succedent parts. A crucial ``subterm property'' is located and proved for the theory of linear order: all terms in a minimum-size derivation are terms in the endsequent. For theories with no hidden cases, i.e., no disjunctions in positive parts of axioms, single succedent rules can be used. This leads to conservativity results that are the proof-theoretical equivalents of model extension results.
20. Sara Negri: Contraction-free sequent calculi for geometric theories, with an application to Barr's theorem, available from Reports Institut Mittag-Leffler, Preprint series: Mathematical Logic - 2000/2001, no. 22, Archive for Mathematical Logic, vol. 41 (2002), in press.
It is shown that sequent calculi can be extended by rules corresponding to axioms that, in categorial terms, are ``geometric implications.'' Existential axioms are typical examples. Barr's theorem, stating that if such an implication is provable in a ``geometric theory'' by classical logic, it is provable by intuitionistic logic, comes out as an immediate corollary to cut elimination: A classical cut-free proof is already an intuitionistic proof.
21. Jan von Plato: Terminating proof search in elementary geometry, available from Report Institut Mittag-Leffler, Preprint series: Mathematical Logic - 2000/2001, no. 43, 2000/2001.
It is shown that minimum-size derivations in sequent calculi for projective and affine geometries have the subterm property (as in item 19). As an application, the independence of Euclid's parallel postulate is proved by a two-line failed proof search.
22. Jan von Plato: Translations from natural deduction to sequent calculus, submitted.
Gentzen's translation from normal ND derivations produces SC derivations with cuts, but Prawitz' 1965 translation gives instead cut-free derivations. The use of general elimination rules, as in item 9, gives an isomorphic translation and shows that Prawitz' translation contains a hidden cut elimination algorithm.
23. Sara Negri and Jan von Plato: Hilbert's last problem and Gentzen's program for its solution, submitted.
A short text by Hilbert, recently discovered in Göttingen, shows that he had considered adding a 24th problem to his famous list of mathematical problems of the year 1900. The problem he had in mind was to find criteria for the simplicity of proofs and to develop a general theory of methods of proof in mathematics. It is discussed to what extent proof theory has achieved the second of these aims.
24. Sara Negri and Jan von Plato: Proof systems for lattice theory, ps file, dvi file, Mathematical Structures in Computer Science, in press.
The subterm property is shown for a rule system of lattice theory that operates on the antecedent part. Next a relational axiomatization of lattice theory (i.e., extra relations and existential axioms instead of the meet and join operations) is turned into natural deduction style rules and the subterm property proved by permutability arguments. This latter gives a purely proof-theoretical approach to Skolem's work of 1920, forgotten until 1992, that established the decidability in polynomial time of universal formulas in lattice theory.
25. Sara Negri and Jan von Plato: Permutability of rules in lattice theory, Algebra Universalis, in press.
Lattice theory is turned into a system of mathematical rules in natural deduction style. It is shown that the rules have permutabililty properties by which all terms in a loop-free derivation must be subterms of the terms in open assumptions or the conclusion. Proof search becomes bounded by the sum of lengths of these terms. The proof is self contained and just slightly over one page in length.