Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.

Dominik Kirst, Marc Hermes

Browse the full ITP paper archive.