[FOM] infinite logical derivations

Stephen G Simpson simpson at math.psu.edu
Wed Aug 22 08:28:52 EDT 2007

In the 1960s and 1970s there was a great deal of interest in
infinitary logic.  Formulas were allowed to contain infinite
conjunctions and disjunctions.  Derivations were allowed to be
infinite.  Barwise and Feferman were important names in this field.
Feferman's long article cited below contains a proof of cut
elimination for infinitary, many-sorted predicate calculus.

Stephen G. Simpson
Professor of Mathematics
Pennsylvania State University
Research interests: mathematical logic, foundations of mathematics


  MR0235996 (38 #4294)

  Feferman, Solomon

  Lectures on proof theory. 1968 Proceedings of the Summer School in
  Logic (Leeds, 1967) pp. 1--107 Springer, Berlin

  This paper is concerned with Gentzen-type proof theory for finitary
  and infinitary many-sorted languages, and contains much recent


  A new, direct proof, using infinitary logic is given of the theorem
  on the ordinal bounds (namely,
  $\varepsilon_0,\varepsilon_{\varepsilon_0}$) on the provable
  well-orderings in first-order number theory and arithmetic
  analysis. As usual, the author's exposition is clear and

  Reviewed by A. S. Troelstra

More information about the FOM mailing list