  In this paper, we present an interactive semantics for derivations in an
infinitary extension of classical logic. The formulas of our language are
possibly infinitary trees labeled by propositional variables and logical
connectives. We show that in our setting every recursive formula equation has a
unique solution. As for derivations, we use an infinitary variant of
Tait-calculus to derive sequents. The interactive semantics for derivations
that we introduce in this article is presented as a debate (interaction tree)
between a test << T >> (derivation candidate, Proponent) and an environment <<
not S >> (negation of a sequent, Opponent). We show a completeness theorem for
derivations that we call interactive completeness theorem: the interaction
between << T >> (test) and << not S >> (environment) does not produce errors
(i.e., Proponent wins) just in case << T >> comes from a syntactical derivation
of << S >>.
