[FOM] Is there a higher order Takeuti conjecture?

Colin McLarty colin.mclarty at case.edu
Sat Jun 4 20:47:40 EDT 2011

Takeuti in 1953 conjectured that a sequent formalisation of
second-order logic has cut-elimination,.  It was proved a good while
later by Tait, and Takahashi, and later Girard.

Is there an analogue, known or still open, for sequent formalisations
of third and higher-order logic?

thanks, Colin

More information about the FOM mailing list