Description
The course discusses different proof systems for first-order logic (without equality) as well as limitations and extensions of first-order logic: semantic tableaux, sequent calculus, Hilbert systems; soundness and completeness; compactness; Herbrand's theorem; Craig's interpolation theorem; second-order logic; Curry-Howard isomorphism.