We study the properties of Propositional Logic in both
classical and intuitionistic formulations. We formalize constructive proofs
of results known from proof theory and model theory. This includes
the studies of natural deduction systems, Gentzen's sequent calculi, and Hilbert
systems. We study 2 models for intuitionistic logic: Kripke structures and
Heyting algebras and their connection. We also study the decision procedures
of semantic tableaux for classical logic (Beth, Smullyan) and intuitionistic
logic (Kripke, Fitting). The intuitionistic tableau system give insights
to the process of finding countermodels, and a connection between the two
logics.
Models for Intuitionistic Propositional
Logic: proofs for Heyting algebras and Kripke models and their connection,
and their relation with the Fitting's tableau systems, the construction and
search for countermodels, and the connection between intuitionistic and
classical logics as suggested by the tableau rules.
