Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
summary
The project mechanizes central metatheory of second‑order logic in Coq mechanization, producing about 8,000 lines of code (plus 1,500 reused) and reimplementing binder and substitution tooling. It proves undecidability and nonenumerability of PA2 validity by a concrete many‑one reduction from Hilbert’s tenth problem (reduction from Hilbert's tenth), shows categoricity of second‑order PA implies incompleteness under full semantics, and establishes completeness for Henkin semantics by a verified translation to mono‑sorted FOL that transports compactness and Löwenheim–Skolem.
AI-written summary · about