Takeuti (1987, 223) derives a cut-elimination theorem for infinitary logic from the soundness-and-completeness theorems. However, is there a way to adapt the original Gentzen-style proof?
The relevant version of the cut rule is (roughly)
From proofs of $\Gamma\to \Delta,A_\alpha$ for all $\alpha<\lambda$ and a proof of $\{A_\alpha\}_{\alpha<\lambda}, \Pi\to \Lambda$,
obtain a proof of $\Gamma,\Pi\to \Delta,\Lambda$.
The obstacles I can see are these... The notion of rank used in the original Gentzen argument (as in Takeuti, 23) assumes that a mix has only two upper sequents, which is not so in the infinite case.
Also, in the original argument, the transformations involved in reducing the left-rank of a proof ending in a mix depend on which rule was used to obtain the upper sequent $\Gamma\to\Delta,A$; but with the infinitary cut rule there will in general be many upper-left sequents, these obtained by many different rules.
So, to clarify the question a little: are the adaptations required (i) routine? ...(hint?) (ii) hairy but done someplace? ...(reference?) (iii) impossible? ...(explanation?)?
Sorry for the slightly lazy question, but I am both old and a novice...
Thanks-in-advance,
Max
PS: by 'infinitary logic' I mean what Takeuti calls 'a system of infinitary logic with homogeneous quantifiers' (1987, 211ff). Roughly speaking, this system generalizes sequent calculus for first-order logic by allowing up-to-card(L)-many simultaneous applications of any given 'finitary' rule, where card(L) is the cardinality of the set of formulas of L.
