[FOM] Is there a higher order Takeuti conjecture?

[Colin McLarty]

Dear Bill,

Thanks for a full and very helpful reply.   I have downloaded your
paper, and the Schutte paper you cite there.

Is there a reason to doubt there can be an effective procedure for
eliminating cuts in finite order logic?  Or is it just that none is
yet known?

I hope the results are proved in Takeuti's book Proof Theory, as the
first edition was several years after the proofs.  But that book seems
not be available on line by normal channels, and I'm waiting for
interlibrary loan.

best, Colin







> From: William Tait <williamtait at mac.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Date: Sun, 05 Jun 2011 10:13:27 -0500
> Subject: Re: [FOM] Is there a higher order Takeuti conjecture?
> On Jun 4, 2011, at 7:47 PM, Colin McLarty wrote:
>
>> 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?
>
> Dear Colin,
>
> Takeuti conjectured that any sequent deduced in (the sequent calculus formalization of) predicate logic of finite order can be deduced without cuts. I first proved the conjecture for second order logic (1965). (I was interested in the 'consistency problem' for second-order number theory and wanted to see, first of all, whether even nonconstructively, provability implied provability without cuts.)  Independently, Dag Prawitz also proved the conjecture for second-order around the same time. Takahashi (and , as I recall, also Prawitz) then proved it for logic of finite order.
>
> In none of these cases was this a proof that a certain effective procedure would transform a deduction with cuts into a deduction without cuts (so-called "cut-elimination"), only a proof that deducibility with cut implied deducibility without cut.
>
> Girard proved that deductions in the natural deduction formalization of logic of finite order can be normalized: By successively eliminating inferences introducing a formula immediately followed by an inference eliminating the same formula, one arrives at a deduction containing no such successive pairs of inferences. (As I recall, Girard proved this for a certain procedure for successively eliminating such pairs. But it was then realized that the result holds no matter what order of elimination one chooses: the so-called 'strong normalization theorem.)  Although this has been called a cut-elimination result ( I think that Girard used this terminology), it does not imply that every sequent deducible with cut can be deduced without cut---at least, I have seen no proof that it does.
>
> Bill Tait