The Π¹₁-formula θ axiomatizes structures that interpret second-order quantification over a base set U as first-order quantification over the power-set expansion of U.

During round i of the game player I can pick a relation \(A_i\) on A (or an element \(a_i\) of A) and then player II has to pick a relation \(B_i\) on B of the same arity as \(A_i\) (or an element \(b_i\) of on B) and vice versa: Player I can instead pick a relation \(B_i\) on B (or an element \(b_i\) of B) and then II picks a relation \(A_i\) on A of the same arity as \(B_i\) (or an element \(a_i\)) of A. After n rounds the pairs of played elements \((a_i,b_i)\) form a binary relation R on \(A\