Mark Koch, Dominik Kirst: Undecidability, incompleteness, and completeness of second-order logic in Coq. CPP 2022: 274-290