 Intuitionistic propositional logic

Intuitionistic propositional logic formalizes reasoning in which a proof of a logical disjunction supplies a proof of one disjunct, and a proof of an logical implication transforms proofs of its antecedent into proofs of its consequent. It has the usual introduction and elimination rules for conjunction, disjunction and implication, together with elimination from falsity, but does not adopt the unrestricted law of excluded middle or double-negation elimination.

A two-world Kripke model for intuitionistic propositional logic illustrates the difference. Let $w_0<w_1$, with $p$ forced only at $w_1$. At $w_0$, neither $p$ nor $\neg p$ is forced: $p$ is not available there, and its possible future truth prevents $\neg p$. Consequently $p\vee \neg p$ is not forced at $w_0$. This gives a semantic counterexample to unrestricted excluded middle, while preserving the persistence of intuitionistic Kripke forcing.