  Given a regular cardinal $\kappa$ such that $\kappa^{<\kappa}=\kappa$ (e.g.,
if the Generalized Continuum Hypothesis holds), we develop a proof system for
classical infinitary logic that includes heterogeneous quantification (i.e.,
infinite alternate sequences of quantifiers) within the language
$\mathcal{L}_{\kappa^+, \kappa}$, where there are conjunctions and disjunctions
of at most $\kappa$ any formulas and quantification (including the
heterogeneous one) is applied to less than $\kappa$ many variables. This type
of quantification is interpreted in $\mathcal{S}et$ using the usual
second-order formulation in terms of strategies for games, and the axioms are
based on a stronger variant of the axiom of determinacy for game semantics.
Within this axiom system we prove the soundness and completeness theorem with
respect to a class of set-valued structures that we call well-determined.
Although this class is more restrictive than the class of determined structures
in Takeuti's determinate logic, the completeness theorem works in our case for
a wider variety of formulas of $\mathcal{L}_{\kappa^+, \kappa}$, and the
category of well-determined models of heterogeneous theories is accessible. Our
system is formulated within the sequent style of categorical logic and we do
not need to impose any specific requirements on the proof trees, disregarding
thus the eigenvariable conditions needed in Takeuti's system. We also
investigate intuitionistic systems with heterogeneous quantifiers and prove
analogously a completeness theorem with respect to well-determined structures
in categories in general, in $\kappa$-Grothendieck toposes in particular, and,
when $\kappa^{<\kappa}=\kappa$, also in Kripke models. Finally, we consider an
extension of our system in which heterogeneous quantification with bounded
quantifiers is expressible, and extend our completeness results to that case.
