Propositional logic

A propositional theory is a set of propositional formulas, sometimes identified with its deductive closure. It is a consistent set of formulae when contradiction is not derivable from it. The completeness theorem for propositional logic identifies consistency with existence of a satisfying Boolean valuation.

A propositional type is a collection of propositional formulas to be jointly realized by a Boolean valuation. A valuation realizes it when every member is true and omits it when some member is false. For propositional omission arguments, the collection need not itself be consistent.

If a consistent propositional theory locally omits every member of a countable family of propositional types, it has a Boolean valuation omitting them all. One may also impose any finite condition consistent with the theory. Successively extend the condition by a negated member of the next type; local omission preserves consistency. The propositional compactness theorem then supplies the valuation. Countability of the ambient language and decidability of consistency are not needed for this argument.

Relative to a consistent propositional theory $T$, a nonprincipal propositional type has no formula consistent with $T$ that implies every member modulo $T$. Equivalently, for each finite condition $\theta$ consistent with $T$, some member $\sigma$ leaves $T\cup \{\theta ,\neg \sigma \}$ consistent. This is the local omission condition for the extended omitting types theorem for propositional logic.

A propositional formula is built from atomic propositions using logical connectives. Unlike a first-order formula, it has no quantifiers over individuals. A Boolean valuation interprets its atoms as truth values and evaluates its connectives recursively.

An implication is derivable from a theory precisely when its conclusion is derivable after adjoining its antecedent. Together with classical contradiction rules, this identifies failure to prove a proposition with consistency after adjoining its negation.

Classical propositional logic interprets propositions as true or false and validates principles such as the law of excluded middle and double-negation elimination.

The law of excluded middle asserts that every proposition $A$ satisfies $A\vee \neg A$.

Double-negation elimination is the inference from $\neg \neg A$ to $A$.

A Boolean valuation assigns each primitive proposition one of the truth values zero and one and extends recursively through the logical connectives.

A truth table lists a finite formula's value for every Boolean valuation of the finitely many primitive propositions that occur in it.

A proposition is a statement to which a logical truth value can be assigned.

A logical connective forms a compound proposition from one or more propositions.

Logical implication forms the proposition $A\to B$. In intuitionistic logic its proof consists of a construction that transforms any proof of $A$ into a proof of $B$.

The contrapositive of $A\to B$ is $\neg B\to \neg A$. In classical propositional logic an implication and its contrapositive are logically equivalent, so either can be proved in place of the other.

The conjunction $A\wedge B$ holds when both $A$ and $B$ hold.

The disjunction $A\vee B$ holds when at least one of $A$ and $B$ holds. Constructively, a proof records which disjunct holds and provides its proof.

Logical truth is the nullary connective that is always true.

Logical falsity is the nullary connective with no proof.

Natural deduction presents logic through introduction and elimination rules for each logical connective.

The rule with premises $C,D$ and conclusion $C$ retains the first derivation while allowing an unused second assumption. Under the Curry-Howard correspondence, the output term is the first premise term, with the enlarged context. This allows a lambda abstraction whose bound variable does not occur in its body.

From $A\to B$ and $A$, implication elimination derives $B$. Under the Curry-Howard correspondence, this is application: from lambda terms $f:A\to B$ and $a:A$ form $fa:B$.

The implication introduction rule discharges a temporary assumption $A$ from a derivation of $B$, producing $A\to B$. Under the Curry-Howard correspondence, a body $t:B$ under $a:A$ gives the lambda abstraction $\lambda a^A.t:A\to B$. Unused assumptions may also be discharged.

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

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

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

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

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.

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

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

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.

If $\Gamma ⊢t$, every valuation that satisfies all formulae in $\Gamma$ also satisfies $t$.

For a set of formulae $\Gamma$ and a formula $\phi$,Together with the soundness theorem for propositional logic, this says that semantic consequence and syntactic provability coincide. Equivalently, every consistent set of formulae has a satisfying Boolean valuation.

Assign a primitive proposition true exactly when it belongs to a maximal consistent set. An induction on formulas proves that truth agrees with membership: maximal consistency gives the negation dichotomy, and deductive closure gives the implication truth table. This builds a model of every consistent propositional theory.

Consistency is preserved under unions of chains because proofs use finitely many assumptions. A maximal consistent extension then gives a valuation through its truth lemma, proving propositional completeness.

When the primitive propositions are not countable, replace sequential enumeration of the formulae by Zorn lemma. The union of a chain of consistent extensions is consistent because every formal proof is finite, so every consistent theory extends to a maximal consistent set in propositional logic. Declaring an atom true exactly when it belongs to that maximal set and proving the truth lemma by structural induction produces a model.

There is an algorithm deciding whether any finite propositional formula is a theorem. A formula contains only finitely many atoms, so a finite truth table decides whether it is valid; the completeness theorem for propositional logic identifies validity with provability.

A set $S$ of formulae is deductively closed whenEquivalently, $S$ equals its deductive closure $\mathrm{Cn}(S)$.

A set $S$ is syntactically consistent when $S/⊢\perp$. Equivalently in classical logic, there is no formula $\phi$ for which both $S⊢\phi$ and $S⊢\neg \phi$.

A set $S$ is finitary when it is deductively equivalent to some finite set $F$: both $S⊢F$ and $F⊢S$.

Ifare deductively closed, then each $T_i$ is consistent and their union is consistent and deductively closed. The union is not finitary. Each conclusion follows from the finite character of formal proofs.

A consistent set $T$ is maximal consistent when no proper extension is consistent. It is deductively closed and decides every formula: exactly one of $t$ and $\neg t$ belongs to $T$. Therefore $v(t)=1$ exactly when $t\in T$ defines a model of $T$.

A set of propositions has a model exactly when every finite subset has a model. Syntactically, a contradiction uses only finitely many assumptions, and every consistent set extends by Zorn lemma to a maximal consistent set in propositional logic.

With atoms $p_{x,y}$, finitary propositions can enforce that the true pairs form an injective partial function. If the codomain is infinite, they cannot enforce that every $x$ has a value: adjoining every $\neg p_{x_0,y}$ remains finitely satisfiable, so compactness produces a model omitting $x_0$.