  The infinitary propositional logic of here-and-there is important for the
theory of answer set programming in view of its relation to strongly equivalent
transformations of logic programs. We know a formal system axiomatizing this
logic exists, but a proof in that system may include infinitely many formulas.
In this note we describe a relationship between the validity of infinitary
formulas in the logic of here-and-there and the provability of formulas in some
finite deductive systems. This relationship allows us to use finite proofs to
justify the validity of infinitary formulas. This note is under consideration
for publication in Theory and Practice of Logic Programming.
