Description

Intuitionistic logic has a historical significance but there is much more
than that. There are many applications and insights to be obtained
nowadays and intuitionistic logic is also the best if not the only full
flight  alternative to classical logic as a contentful system of
reasoning. We intend to give an elementary overview of intuitionistic
propositional calculus IPC:

- The BHK (Brouwer-Heyting-Kolmogorov interpretation)
- Proof systems (Hilbert type, natural deduction, sequent systems,
formulas-as-types)
- Kripke semantics with completeness and FMP
- Translations of classical propositional calculus CPC into IPC and of IPC
into S4 and other modal logics, Glivenko's theorem 
- Disjunction properties
- algebraic, topological, categorical semantics
- universal models and Jankov formulas
- interpolation and uniform interpolation
- completeness and incompleteness in predicate logic
- intermediate logics
- intuitionistic modal logics
- substitutions, Ruitenburg's and Ghilardi's theorems.