[FOM] An attempt of a constructive proof for Takeuti Conjecture

[Sandro Skansi]

Dear FOM-ers,

In 1953, Gaisi Takeuti posed the question of the eliminability of cuts for
full second order logic, and this was proven non-constructively by Tait in
1966 and independently by Prawitz 1967. The idea of possible
impredicativity suggested that a constructive proof was out of reach, but
this might be still possible in my opnion. An attempt to make a
constructive proof of cut elimination for full second order logic available
at http://www.logic101.net/upload/4296/documents/Article%20SO%20Skansi.pdf.
I would greatly appreciate your feedback and comments!

Best regards,

Sandro Skansi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140225/3f4394d0/attachment-0001.html>