Harvey Friedman described his "Finite Promise Games" here and in my opinion a more clear version is described on the Googology Wiki page. He claims that several of the theorems proposed on that FOM mail require very high proof-theoretic strength to be determined. Specifically, he claims that the theorems asserting the finitistic nature of the four types of games are not provable in ZFC or even SMAH (ZFC augmented with an infinite set of axioms, each asserting the existence of a $k$-Mahlo cardinal for a different $k\in\mathbb N$), assuming they are both consistent. Furthermore, he claims that those same theorems are provable in what he calls SMAH+, that is, ZFC augmented with a single axiom asserting the existence of at least one $k$-Mahlo cardinal for each $k\in\mathbb N$, thus giving a very narrow window of proof-theoretic strength in which those theorems reside. Subsequently, the functions arising from the games dominate all functions provably recursive in any consistent fragment of SMAH that proves all of RCA$_0$'s statements. Friedman does not give any part of such a proof explicitly or even describe how one could go about proving the theorems of the finite promise games. His claims about the theorems being proof-theoretically bounded in a way by the strengths of SMAH and SMAH+ is equivalent to their correctness being implied by the existence of infinitely many different types of Mahlo cardinals together with the axioms of ZFC, but nothing less than that on the cardinal side. I have been aware for a long time that some statements about the finite world require the abstract notions of large cardinals to prove, but the exact details of how that works still elude me. I am not an expert at all, but I am keen on learning as much as possible about the art of constructing proofs of all kinds of things in set theory. This is my first question on this site and so I want to use it to get the gist of something otherwise very complicated.
So my question is on how the existence of infinitely many types of Mahlo cardinals could possibly be used in the proof of the finite promise games and subsequently the well-foundedness of the functions arising from them? What property of the Mahlo hierarchy of cardinals can be used to prove statements about the properties of certain functions on the integers? Furthermore, how in the world could doctor Friedman know that the existence of only finitely many different types of $k$-Mahlo cardinals together with the axioms of ZFC can't be enough to prove those statements? I am of course not asking for any explicit proofs, but just an intuitive explanation of where the connection may come from.
In the case that it isn't clear, a $0$-Mahlo cardinal is a strongly Mahlo cardinal (or equivalently without a strong failure of GCH, a weakly Mahlo cardinal) and an $ \alpha$-Mahlo cardinal is a regular cardinal $\kappa$ such that for every ordinal $\beta\in\alpha$, the $\beta$-Mahlo cardinals below $\kappa$ form a stationary subset of $\kappa$.