You're looking for **infinitary logic** - probably $\mathcal{L}_{\omega_1\omega_1}$ if you're using countably many distinct free varables. See https://en.wikipedia.org/wiki/Infinitary_logic, as well as https://www.math.wisc.edu/~keisler/kk2.pdf (the latter is a biographical paper about Barwise, but it is also a good source on infinitary logic in general). **** Basically, here's how it works: we fix cardinals $\kappa$ and $\lambda$, with $\kappa\ge\lambda$. Then $\mathcal{L}_{\kappa\lambda}$ is (informally) the set of formulas generated by starting with first-order logic and closing under - conjunctions and disjunctions over sets of $<\kappa$-many formulas, and - quantification over $<\lambda$-many variables. We can also define proper class sized infinitary logics as $$\mathcal{L}_{\infty\lambda}=\bigcup_{\kappa\in Card} \mathcal{L}_{\kappa\lambda}\quad\mbox{and}\quad \mathcal{L}_{\infty\infty}=\bigcup_{\lambda\in Card}\mathcal{L}_{\infty\lambda}.$$ Of course, the precise definitions are a bit technical, but this is the key idea. Of special interest is $\mathcal{L}_{\infty\omega}$, which is roughly the "logic of back-and-forth arguments": two structures are $\mathcal{L}_{\infty\omega}$-equivalent iff player II has a winning strategy in the Ehrenfeucht-Fraisse game of length $\omega$ - or, equivalently, if there is some *forcing extension* of the universe in which they become isomorphic. (The first fact is due to Karp; the second is folklore, but I believe first observed by Barwise.) **** Note that we could similarly define infinitary second-order logic, etc. I know less about such things, though.