Title of the course: Calculi and completeness for classical and intuitionistic logics
Instructor: Dr. Sergei Odintsov
Institution: Sobolev Institute of Mathematics, Novosibirsk
Dates: 29 July – 3 August 2024
Prerequisites: Knowledge of mathematical proofs and their implementation is expected; some elementary knowledge of special binary relations: preorders, partial orders, trees, etc.
Level: Graduate, advanced undergraduate, beginning undergraduate
Abstract: After defining basic semantical concepts for classical propositional logic we present four kind of calculi for this logic: tableaux, Gentzen style, natural deduction, and Hilbert style calculi. We prove the weak completeness theorem tableaux and Gentzen style calculi and the strong completeness theorem for natural deduction, and Hilbert style calculi demonstrating also difference between constructive and non-constructive methods of proofs. Then after short introduction to intuitionism we modify Gentzen style, natural deduction, and Hilbert style calculi and methods of proof to obtain intuitionistic claculi and relational semantics for intuitionistic logic. Time permitting, we discuss also intuitionistic tableaux.
Language: EN