Lògica intuïcionista. Teorema de Glivenko

Abstract

[en] Glivenko’s theorem says that the fact that a proposition is provable in classical logic is equivalent to the double negation of this proposition being provable in intuitionistic logic. We present the intuitionistic logic and introduce two syntactic calculus: the Hilbert calculus and the natural deduction calculus. We give as well two semantics for the intuitionistic logic. A relational one, based on Kripke models and an algebraic one, based on Heyting algebras. To conclude we give three different proofs of Glivenko’s theorem. A syntactic one, a semantic one based on Kripke models and a semantic one based on Heyting algebras.