Takeuti (1987, 223) deduces a cut-elimination theorem for infinitary logic from the corresponding soundness-and-completeness theorems. However, is there a way to adapt the basic Gentzen-style argument?

The relevant cut rule says (this is a rephrasing from Takeuti, 215)

From proofs of $\Gamma\to \Delta, A_\alpha$ for all $\alpha<\lambda$ and a proof of $\{A_\alpha\}_{\alpha<\lambda},\Pi\vdash \Lambda$,

obtain a proof of $\Gamma,\Pi\to \Delta,\Lambda$.

The notion of rank used in the basic Gentzen argument assumes that an inference has only one upper-left sequent, whereas here we have maybe infinitely many. Perhaps one could redefine left-rank by a lexicographic ordering along the ranks of the upper-left sequents?

I was able to adapt the transformations needed for reduction in right-rank, but then got caught in a hairball on the upper left. The problem is that the transformations given in basic argument depend on the rule by which the upper-left sequent was obtained.

Has this been worked out someplace? A reference (or a hint!) would be much appreciated.



PS. The relevant notion of infinitary logic is what Takeuti (213) calls 'a system of infinitary logic with homogeneous quantifiers'. Basically, this adjusts the logical rules to fit the infinitary connectives as one would expect, but also allows infinitely many simultaneous applications of any one logical rule. (This is also apparent in the generalized form of the cut rule above.) Please let me know if more detail would be helpful here.

PPS. If it makes any difference, for my purposes the result is needed only for propositional infinitary logic.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.