Intuitionistic Gödel-Löb without Sharps

Das, van der Giessen, and Marin recently introduced \(\mathsf{IGL}\) , an intuitionistic version of Gödel-Löb logic. Their proof systems involves ill-founded proofs with a progressiveness condition. Their completeness proof uses the principle of \(\Sigma^{1}_{1}\) -determinacy; which is not provable in \(\mathsf{ZFC}\) . We define a cyclic proof system for \(\mathsf{IGL}\) and give a proof of its completeness theorem avoiding \(\Sigma^{1}_{1}\) -determinacy.