Advisor: Dominik Kirst
Second-order logic is an extension of first-order logic, allowing quantifiers to not only range over individuals, but also over functions and predicates. This leads to major differences in behaviour compared to its first-order counterpart. Notably, second-order logic (interpreted in standard semantics) does not admit a complete proof system.
The first part of the project consists of a Coq mechanization of second-order logic including a proof that no sound, complete and enumerable deduction system can exist for standard semantics. We require Markov's Principle and make use of the categoricity of second-order Peano arithmetic and a reduction from the solvability of Diophantine equations. Using this result, we conclude the incompleteness of a concrete mechanized deduction system. Additionally, we use the reduction to establish the undecidability of second-order PA and the undecidability of validity and satisfiability for second-order logic in arbitrary (in particular empty) signatures.
However, completeness for second-order logic can be recovered if one switches to Henkin semantics. While the usual Henkin completeness proof also works in the second-order case, we chose to follow a different route to obtain this result. Namely, we make use of the first-order completeness theorem, by reducing SOL with Henkin semantics to mono-sorted FOL.