[FOM] infinite logical derivations

[Stephen G Simpson]

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
  material.

  [...]

  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
  well-organized.

  Reviewed by A. S. Troelstra