# [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
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