[FOM] Is there a higher order Takeuti conjecture?

[William Tait]

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