Infinitary (ie non-wellfounded) and circular proof systems received much attention in recent years, since the seminal work by Brotherston and Simpson. Such proof systems allow non-wellfounded proof trees and impose some global validity condition in order to ensure soundness which requires that every infinite branch is supported by some “thread” which trace some formula in a bottom-up manner and witnesses infinitely many progress points of a coinductive property.

Unfortunately, existing notions of validity impose a quite limited use of cuts in non-wellfounded proofs and many proofs that should be accepted as valid are rejected.

We introduce a new validity condition for muMALL infinitary and circular proofs. This criterion generalizes the existing one, taking inspiration from Geometry of Interaction, enriching the structure of threads and relaxing their geometry: bouncing threads can leave the branch they validate and “bounce” (ie change direction, moving upward but also downward along the proof branches) on axioms and cut rules.

In this talk we will focus on the multiplicative fragment muMLL. We will see that this “bouncing validity” criterion is sound with respect to boolean semantics and that it admits a cut-elimination theorem. We also prove that checking whether a circular pre-proof satisfies the criterion is undecidable, however the criterion can be decomposed into an infinite hierarchy of decidable validity conditions.