Fri Apr 8, 2016
20 Barrows, 4:10–6 PM
|Alfred Tarski Lectures
William W. Tait (Professor Emeritus, Department of Philosophy and CHSS, University of Chicago)
Cut-Elimination for Subsystems of Classical Second-Order Number Theory: Cut-Elimination for Π_1^1 − CA with the ω-Rule—and Beyond(?)
I will present a simplification of the proof of cut-eliminability of Gaisi Takeuti and Mariko Yasugi for this system. In particular, I will avoid the use of Takeuti’s ordinal diagrams. (I do use the finite part of the Veblen hierarchy, though.) Given time and sufficient conviction, I may speak about the possibility of extending the result to Π_2^1 − CA and beyond.