  I formalize important theorems about classical propositional logic in the
proof assistant Coq. The main theorems I prove are (1) the soundness and
completeness of natural deduction calculus, (2) the equivalence between natural
deduction calculus, Hilbert systems and sequent calculus and (3) cut
elimination for sequent calculus.
