We introduce a non-wellfounded proof system based on a non-wellfounded language , having roughly the expressive strength of the language of finitely iterated inductive definitions \(\textrm{ID}_{<\omega }\) . As a measure of its strength, we analyze the proof theoretic properties of consistency, cut-elimination and soundness of from a reverse mathematical point of view. Establishing a natural semantic for the non-wellfounded language through games of infinite length, we show that all three properties are equivalent to the determinacy assertion \(\forall n.(\mathrm \Pi ^0_1)_n\mathrm {-Det}\) over Baire space and to the system \(\mathrm \Pi ^1_{3}\mathrm {-RFN}\left( \mathrm {\Pi ^1_1-CA}_0\right) \) of second order arithmetic. For a restricted system based on a non-wellfounded language with binary connectives, we show that syntactic cut-elimination versus semantic cut-admissibility have vastly different reverse mathematical strength. The former still corresponds to \(\mathrm \Pi ^1_{3}\mathrm {-RFN}\left( \mathrm {\Pi ^1_1-CA}_0\right) \) . The latter, together with consistency and soundness for the system , correspond to the determinacy assertion \(\forall n.(\mathrm \Pi ^0_1)_n\mathrm {-Det^{\star }}\) over Cantor space and to the second order theory \(\mathrm \Pi ^1_{2}\mathrm {-RFN}\left( \textrm{ACA}_0\right) \equiv \textrm{ACA}_0'\) .