# Mechanization of Second-order Logic

The first part of the project consists of mechanizing the syntax and full semantics of second-order logic and proving that no complete effective deduction system can exist.