Can you clarify the role of the referee in the weak quasi-strategy case. I'm unsure what it means to have a play in conformance for the weak case as opposed to the quasi-strategy case. For example, what if there can be no referee making those choices? Then there are no plays in conformance, so the quasi-strategy is vacuously winning?

If you change the axiom to assert that exactly one player has a winning quasi-strategy, then over ZF this implies DC, and in ZF+DC it is equivalent to your axiom. So this way of proceeding avoids the need to assume DC.

What you call a quasistrategy is also called a policy. So you play in accordance with a policy.

But isn't the legitimacy of recursive definition due to Dedekind in 1888? He showed on the basis of axioms of successor that recursive definitions succeed, and this was how he defined addition and multiplication etc. from successor and it was the basis for his categoricity theorem for the second-order theory of the successor operation.

What we need to do is to form the presentation directly from the program, in such a manner that produces a group whose size is related to the running time, whether this is finite or infinite. The examples I know have the feature that a halting computation causes a big collapse in the group; but perhaps the experts have other examples with the required feature.

@HJRW I don't think the $C_n\times(G_n*G_n)$ presentation idea is going to work, since the $C_n$ factor is what makes it size $n$, but we need this to be the (unknown) running time at the time we form the presentation. The size of the program $p$ is going to be typically far smaller than the running time, and we can't afford to find out what the running time is, since we don't know whether it halts.

Very nice question! It would suffice for us to provide, for any Turing machine program $p$, a group presentation (of about the same size as $p$), which presented a group at least as large as the running time of $p$, if it halts, otherwise infinite. If that were possible, then your function would essentially majorize the busy beaver function. But is this possible?

$\text{MA}_{\omega_1}$.

It is a very nice question!

Escapes means not-eventually-dominated-by?

Very nice observation.

Asaf, you give the extrinsic justification, but many people favor the intrinsic justification, holding that the axiom of choice expresses a fundamental truth about the nature of sets, and that is why they feel free to use it. At bottom, the view is that the axiom is a logical truth.