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.

In a lattice, joins and meets are the pairwise least upper bounds and greatest lower bounds.

The join of two elements of a lattice is their least upper bound. In a lattice of closed set families, it is the closure of their union.

The meet of two elements of a lattice is their greatest lower bound. For set families ordered by inclusion, it is their intersection whenever that intersection lies in the specified lattice.

A homomorphism between lattices preserves binary joins and meets: $f(x\vee y)=f(x)\vee f(y)$ and $f(x\wedge y)=f(x)\wedge f(y)$. It is order preserving, since $x\le y$ implies $x=x\wedge y$ and hence $f(x)=f(x)\wedge f(y)$. For a map into the two-element lattice, the inverse image of zero is a lattice ideal, and meet preservation says this ideal is prime: if a meet belongs to it, at least one factor does. Conversely the indicator of the complement of a prime lattice ideal preserves both operations. Preservation of distinguished top and bottom elements is an additional requirement for homomorphisms of bounded lattices.

A complete lattice is a partially ordered set in which every subset has a meet and a join, including the empty subset.

Every order-preserving function from a complete lattice to itself has a least and a greatest fixed point. More strongly, its set of fixed points is itself a complete lattice.

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

In a distributive lattice,

A Boolean algebra is a bounded distributive lattice in which every element has a complement. Its meet, join, and complement abstract conjunction, disjunction, and negation.

Every proper lattice ideal of a Boolean algebra extends to a prime lattice ideal. More generally, an ideal disjoint from a lattice filter extends to a prime ideal still disjoint from that filter. This Boolean case of the Stone prime filter theorem is equivalent to the ultrafilter lemma over Zermelo–Fraenkel set theory and is weaker than the axiom of choice.

The lattice ideals of a Boolean algebra form a frame under inclusion. Meets are intersections and joins are ideals generated by unions. A complemented ideal is principal: if $I\vee J=B$ and $I\cap J=\{0\}$, choose $b\in I,c\in J$ with $b\vee c=1$; then $c=\neg b$ and $I=\downarrow b$. This ideal frame defines an extremally disconnected locale exactly when $B$ is complete.

A Boolean algebra in which every set-indexed family has a join and a meet. Double-negation Boolean algebra is an intuitionistic example, with joins formed by regularizing unions. Completeness makes truth values for quantifiers possible in a Boolean-valued inner universe over intuitionistic set theory.

Inside IZF, truth values are subsets of a singleton. Their double-negation-stable elements form a complete Boolean algebra: arbitrary meets are intersections and arbitrary joins are double-negation closures of unions. Negation gives Boolean complement. The join of $p$ and its complement is top although their ordinary union need not be top. The closure here is taken inside the fixed singleton; it does not assume that the class of all objects double-negatively belonging to an arbitrary set is itself a set.

A lattice filter is a nonempty upward-closed subset closed under finite meets. A proper filter omits the bottom element.

A lattice filter is a filter in an ordered set when that order is a lattice; directedness and upward closure then imply closure under finite meets.

A prime filter is a proper lattice filter $P$ such that $a\vee b\in P$ implies $a\in P$ or $b\in P$.

If a lattice filter $F$ and lattice ideal $I$ in a distributive lattice are disjoint, there is a prime filter of a distributive lattice containing $F$ and disjoint from $I$.

The Boolean prime ideal theorem is the Boolean-algebra version; distributivity gives this corresponding filter-extension statement.

A lattice ideal is a nonempty downward-closed subset closed under finite joins. It is the order-dual notion to a lattice filter.

A proper lattice ideal $I$ is prime if $x\wedge y\in I$ implies $x\in I$ or $y\in I$. Its complement is a prime filter of a distributive lattice when the lattice is distributive: downward closure of the ideal makes the complement upward closed, primeness makes it meet-closed, and join closure makes that filter prime. Equivalently, its complement indicator is a homomorphism of lattices to the two-element lattice. Given $b\nleqq a$ in a distributive lattice, maximize an ideal containing $a$ and avoiding $b$ using Zorn lemma. If $x,y$ lie outside it, the two enlarged ideals contain $b$, so $b\le i\vee x$ and $b\le j\vee y$ for some $i,j\in I$. Distributivity shows that $x\wedge y\in I$ would force $b\in I$, a contradiction. Thus this maximal avoiding ideal is prime and separates the two specified elements.

Priestley duality is a dual equivalence between bounded distributive lattices and compact totally order-disconnected ordered topological spaces.

The Priestley dual space $\hat{L}$ of a bounded distributive lattice $L$ consists of its prime filters, ordered by inclusion and topologized by the sets $a^{\ast }=\{P:a\in P\}$ and their complements.

This construction yields a Priestley space: a compact ordered topological space in which suitable clopen upward-closed sets separate distinct comparable-order failures.

A clopen up-set is both clopen in the topology and upward closed in the order. The clopen up-sets of a Priestley space form a distributive lattice under intersection and union.

The Stone map sends an element $a$ of a distributive lattice to the clopen up-set $a^{\ast }=\{P:a\in P\}$ of its Priestley dual space. The Stone prime filter theorem makes this lattice homomorphism injective.

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$.

In a Heyting algebra, $a\to b$ is the greatest $x$ with $x\wedge a\le b$. Thus $x\le a\to b$ if and only if $x\wedge a\le b$. Every frame has this operation, obtained by taking the join of all such $x$. The open nucleus attached to $a$ is $x\mapsto a\to x$.

The pseudocomplement of $a$ is the greatest element disjoint from $a$. It need not satisfy $a\vee \neg a=1$. In a frame, double pseudocomplementation defines the Booleanization of a locale; its fixed elements are regular open elements.

Meets of subsheaves are pointwise intersections. Joins are J-closures of pointwise unions: a section lies in the join when its restrictions locally belong to some member, with the member allowed to vary. Implication consists of sections every restriction of which belongs to $D$ whenever it belongs to $A$; this gives $C\le (A\Rightarrow D)$ exactly when $C\cap A\le D$. Negation is implication into the initial subobject. Empty covers mean that the initial sheaf need not be pointwise empty.

An element $a$ of a Heyting algebra is regular when $\neg \neg a=a$. The regular elements form its Booleanization.

In a Heyting algebra, meet with a fixed element is left adjoint to Heyting implication, so it preserves joins:The dual distributive law follows from this one by the lattice absorption laws.

In the implicational fragments, assumptions correspond to typed variables, implication introduction to lambda abstraction, and implication elimination to function application. Typing derivations in the simply typed lambda calculus correspond inductively to natural-deduction proofs.

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$.

The forcing relation is the intuitionistic instance of Kripke semantics; persistence and the order on worlds determine its implication clause.

The Kripke forcing relation $w⊩A$ records that formula $A$ holds at world $w$. For intuitionistic implication, $w⊩A\to B$ exactly when every extension of $w$ that forces $A$ also forces $B$.

If $w\le v$ and $w⊩A$, then $v⊩A$. The proof is by structural induction on $A$.

A Kripke countermodel to a formula $A$ is a Kripke model for intuitionistic propositional logic containing a world $w$ such that $w⊮A$.

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.

The disjunction property says that if ${⊢}_{\mathrm{IPC}}A\vee B$, then ${⊢}_{\mathrm{IPC}}A$ or ${⊢}_{\mathrm{IPC}}B$.

This is the disjunction part of disjunction and existence properties, specialized to Intuitionistic propositional logic.

The implication-free fragment uses only conjunction, disjunction, truth, and falsity, with their intuitionistic natural-deduction rules.

An implication-free formula is provable exactly when every valuation into every bounded distributive lattice assigns it the top element.

The implicational fragment of intuitionistic propositional logic contains formulas built from atoms using only logical implication, with only implication introduction, implication elimination, and assumptions as proof rules.

The canonical worlds are deductively closed implicational theories ordered by inclusion. A world forces an atom exactly when the atom belongs to that theory. The truth lemma says that a world forces an implicational formula exactly when the formula belongs to the theory.

For implicational formulas $\Gamma$ and $\phi$,The reverse implication follows from the canonical Kripke model for implicational intuitionistic logic and its truth lemma.

If $\Gamma$ and $\phi$ are implicational and $\Gamma {⊢}_{\mathrm{IPC}}\phi$, then $\Gamma {⊢}_{\mathrm{IPC}(\to )}\phi$. Soundness for Kripke semantics followed by Kripke completeness of implicational intuitionistic logic proves the claim.