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

[WILLIAM TAIT]

Takeuti conjectured that derivability in logic of finite order implied cut-free derivability. Tait (that's me) proved that conjecture for second-order logic (which was enough for my purposes) based on a result of Schuette. Prawitz and Takahashi independently obtained that result (also using Schuette's result) and then subsequently proved the full Takeuti's conjecture. 

But that conjecture concerns classical logic. A constructive proof of cut-elimination for intuitionistic logic of finite types was given by Girard in the 1970's. The system that you describe is intuitionistic. Rather than showing that, let me just point out that if  you have proved cut-elimination for the system you described, then that system does not admit the derivation of the sequent

(A \implies absurdity) \implies absurdity |- A 

when, say,  A is an atomic sentence other than absurdity.  

It is, alas, amazing (at least to me) how much difference the law of excluded middle makes. I don't think that you will find a 'constructive' proof of cut elimination for second order logic and beyond, in any reasonable sense. But I hope you will find one that is of interest. 

Best regards,
Bill Tait



On Feb 25, 2014, at 4:55 PM, Sandro Skansi <skansi.sandro at gmail.com> wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom