Intuitionistic propositional logic

Intuitionistic propositional logic omits unrestricted excluded middle and interprets implication constructively.

A lattice is a partially ordered set in which every pair has a greatest lower bound, called its meet, and a least upper bound, called its join.

A distributive lattice is a lattice in which meet distributes over join and, equivalently, join distributes over meet.

A Heyting algebra is a bounded distributive lattice with an implication $a\Rightarrow b$ characterized by $x\le (a\Rightarrow b)$ exactly when $x\wedge a\le b$.

The Curry-Howard correspondence identifies propositions with types and proofs with typed programs; implication corresponds to a function type, conjunction to a product type, and falsity to the empty type.

A Kripke model is a poset of worlds with a persistent valuation of atoms. Conjunction and disjunction are forced pointwise, while $w⊩\alpha \to \beta$ exactly when every $v\ge w$ that forces $\alpha$ also forces $\beta$.

A proposition is derivable in intuitionistic propositional logic exactly when it is forced at every world of every intuitionistic Kripke model.

Filtration identifies worlds that force the same formulas in a fixed finite subformula-closed set. With order induced by inclusion of these finite theories, the quotient preserves forcing of every retained formula and has at most $2^n$ worlds for $n$ formulas.

The unravelling of a rooted Kripke model has finite increasing paths from the root as worlds, ordered by extension and labelled by their endpoints. It is tree-like and preserves forcing.

Every intuitionistically underivable proposition has a finite rooted Kripke countermodel. Filtration and witness pruning bound the model in terms of the number of subformulas.