Propositional Logic

Proof. Let $S=\{\phi \in \mathrm{Form}:P(\phi )\}$. The hypotheses say precisely that $S$ satisfies clauses (1)–(3) of the definition. Since $\mathrm{Form}$ is the smallest such set, $\mathrm{Form}\subseteq S$, and as $S\subseteq \mathrm{Form}$ by construction, $S=\mathrm{Form}$.∎

Proof. By structural induction. For an atom, $\top$ or $\perp$, the string has no parentheses and no proper non-empty initial segment at all, so both claims hold.

Suppose the claims hold for $\phi$ and $\psi$, and consider $\chi =(\phi \ast \psi )$ for a binary connective $\ast$. Its parenthesis count exceeds the combined counts of $\phi$ and $\psi$ by one of each kind, and those are balanced, so $\chi$ is balanced. A proper non-empty initial segment of $\chi$ has one of these forms: the single symbol $($; or $($ followed by a proper non-empty initial segment of $\phi$; or $($ followed by all of $\phi$; or that together with $\ast$; or that followed by a proper non-empty initial segment of $\psi$. In the first four cases the excess of left over right parentheses is at least $1$, using the induction hypothesis for $\phi$ in the second case and the balance of $\phi$ in the third and fourth. In the last case the excess is $1$ plus the excess in an initial segment of $\psi$, hence at least $2$. The unary case $(\neg \phi )$ is the same argument with fewer sub-cases.∎

Proof. A formula beginning with a symbol other than $($ is an atom, $\top$ or $\perp$, and those three cases are visibly disjoint. So suppose the formula begins with $($. The symbol immediately after it is either $\neg$ — in which case the formula can only have arisen from clause (2) — or the first symbol of a formula, in which case it arose from clause (3). That settles the shape.

For uniqueness of the constituents, suppose $(\phi \ast \psi )$ and $({\phi }^{\prime }{\ast }^{\prime }{\psi }^{\prime })$ are the same string. If $\phi \ne {\phi }^{\prime }$ then one is a proper non-empty initial segment of the other, say $\phi$ of ${\phi }^{\prime }$. By Lemma Parenthesis balance the left parentheses of $\phi$ then strictly outnumber its right ones — yet $\phi$ is itself a formula and so is balanced. That contradiction forces $\phi ={\phi }^{\prime }$. Deleting the common prefix $(\phi$ leaves $\ast \psi )$ and ${\ast }^{\prime }{\psi }^{\prime })$ equal as strings, so $\ast ={\ast }^{\prime }$ and then $\psi ={\psi }^{\prime }$.∎

Proof. Structural induction on $\phi$. The atomic case is the hypothesis, and $\top ,\perp$ are constant. If the claim holds for $\phi$ and $\psi$, then since $\mathrm{At}(\phi \ast \psi )=\mathrm{At}(\phi )\cup \mathrm{At}(\psi )$, the valuations agree on the atoms of each constituent, so they agree on the constituents' values, and the clauses of Definition Valuation and its extension compute the same value from the same inputs.∎

Proof. A truth function is a function from the $2^n$ -element set $\{0,1{\}}^n$ to the $2$ -element set $\{0,1\}$, and the number of functions from a set of size $a$ to a set of size $b$ is $b^a$. Hence the count is $2^{2^n}$; substituting $n=1$ and $n=2$ gives $4$ and $16$.∎

Proof. Let $f$ be an $n$ -ary truth function. If $f$ is identically $0$, the formula $p_1\wedge \neg p_1$ expresses it. Otherwise let $T=\{a\in \{0,1{\}}^n:f(a)=1\}$, a non-empty finite set. For $a=(a_1,\dots ,a_n)\in T$ put

and set ${\phi }_f={\bigvee }_{a\in T}{\chi }_a$. Every connective used is in $\{\neg ,\wedge ,\vee \}$.

For correctness, fix a valuation $v$ and let $b=(v(p_1),\dots ,v(p_n))$. By construction $v({\chi }_a)=1$ if and only if $v(p_i)=a_i$ for every $i$, that is, if and only if $a=b$. Hence $v({\phi }_f)=1$ iff some $a\in T$ equals $b$, iff $b\in T$, iff $f(b)=1$. So ${\phi }_f$ expresses $f$.∎

Proof. By Theorem Functional completeness of the standard set it is enough to rewrite every formula over $\{\neg ,\wedge ,\vee \}$ inside the smaller set, which we do by replacing offending subformulas innermost-first. For $\{\neg ,\wedge \}$ use $\phi \vee \psi \equiv \neg (\neg \phi \wedge \neg \psi )$; for $\{\neg ,\vee \}$ use $\phi \wedge \psi \equiv \neg (\neg \phi \vee \neg \psi )$; for $\{\neg ,\to \}$ use $\phi \vee \psi \equiv \neg \phi \to \psi$ together with $\phi \wedge \psi \equiv \neg (\phi \to \neg \psi )$. Each replacement preserves the truth function, as a two-row or four-row check confirms, and each strictly decreases the number of forbidden connectives, so the rewriting terminates.∎

Proof. It suffices to express $\neg$ and $\wedge$, by Corollary Smaller complete sets. Since $p\uparrow p=\neg (p\wedge p)=\neg p$, negation is available. Then

So both $\neg$ and $\wedge$ are expressible using $\uparrow$ alone. The argument for $\downarrow$ is dual: $p\downarrow p=\neg p$ and $(p\downarrow q)\downarrow (p\downarrow q)=p\vee q$, and $\{\neg ,\vee \}$ is complete.∎

Proof. Call a formula monotone if $v(\phi )\le w(\phi )$ whenever $v(p)\le w(p)$ for every atom $p$. Every atom is monotone, and if $\phi ,\psi$ are monotone then so are $\phi \wedge \psi$ and $\phi \vee \psi$, because $\min$ and $\max$ are non-decreasing in each argument. By Theorem Structural induction every formula over $\{\wedge ,\vee \}$ is monotone. But $\neg p$ is not: taking $v(p)=0\le 1=w(p)$ gives $v(\neg p)=1>0=w(\neg p)$.∎

Proof. Let $v_1$ be the valuation sending every atom to $1$. Each of the four connectives returns $1$ when both arguments are $1$: $\min (1,1)=\max (1,1)=1$, and $1\to 1$ and $1\leftrightarrow 1$ are both $1$. So by structural induction $v_1(\phi )=1$ for every formula $\phi$ over that set. Since $v_1(\neg p)=0$, negation is not among them.∎

Proof. ($\Rightarrow$) Let $v\models \Sigma$. If $v(\phi )=0$ then $v(\phi \to \psi )=1$ outright. If $v(\phi )=1$ then $v\models \Sigma \cup \{\phi \}$, so by hypothesis $v(\psi )=1$ and again $v(\phi \to \psi )=1$.

($\Leftarrow$) Let $v\models \Sigma \cup \{\phi \}$. Then $v\models \Sigma$, so $v(\phi \to \psi )=1$ by hypothesis; and $v(\phi )=1$, so the only way the implication can hold is $v(\psi )=1$.∎

Proof. The three properties are inherited pointwise from equality of the values $v(\phi )$. For the second claim, map each class to the truth function its members express; this is well defined and injective by the definition of $\equiv$, and surjective by Theorem Functional completeness of the standard set. Over $n$ atoms there are therefore exactly $2^{2^n}$ classes.∎

Proof. Induct on the rank of $\chi$ relative to the distinguished occurrence. If the occurrence is all of $\chi$, then $\chi =\phi \equiv \psi ={\chi }^{\prime }$ and there is nothing to prove. Otherwise $\chi$ has a principal connective and the occurrence lies inside one immediate constituent. Say $\chi ={\chi }_1\ast {\chi }_2$ with the occurrence inside ${\chi }_1$, and let ${\chi }_1^{\prime }$ be the corresponding replacement, so ${\chi }^{\prime }={\chi }_1^{\prime }\ast {\chi }_2$. By the induction hypothesis ${\chi }_1\equiv {\chi }_1^{\prime }$, so for every valuation $v$ we have $v({\chi }_1)=v({\chi }_1^{\prime })$, and then

where $\ast$ also denotes the truth function of the connective. The unary case is identical with one argument. Hence $\chi \equiv {\chi }^{\prime }$.∎

Proof. Fix a valuation $v$ and define a valuation $w$ on atoms by $w(p)=v(\sigma (p))$. A structural induction on $\phi$ shows $v({\phi }^{\sigma })=w(\phi )$: for an atom this is the definition of $w$; and for a compound formula, substitution commutes with the connective, so both sides are computed by the same truth function from equal arguments. Since $\phi$ is a tautology, $w(\phi )=1$, hence $v({\phi }^{\sigma })=1$. As $v$ was arbitrary, ${\phi }^{\sigma }$ is a tautology.∎

Proof. By Theorem Uniform substitution preserves tautologies it suffices to verify each as a biconditional between atoms, and each such verification is a truth table with at most $8$ rows. For instance $\neg (p\wedge q)$ and $\neg p\vee \neg q$ are both $0$ exactly on the row $p=q=1$; and $p\vee (q\wedge r)$ and $(p\vee q)\wedge (p\vee r)$ are both $1$ exactly when $p=1$ or $q=r=1$.∎

Proof. Write ${\phi }^{\neg }$ for the formula with every atom negated, and argue by structural induction that ${\phi }^d\equiv \neg ({\phi }^{\neg })$. For an atom $p$: $p^d=p$ and $\neg (\neg p)\equiv p$. For $\top$: ${\top }^d=\perp \equiv \neg \top$. For $\neg \alpha$: $(\neg \alpha {)}^d=\neg ({\alpha }^d)\equiv \neg \neg ({\alpha }^{\neg })\equiv \neg ((\neg \alpha {)}^{\neg })$ after one double negation. For $\alpha \wedge \beta$,

by De Morgan from Theorem The basic equivalences, and the $\vee$ case is symmetric.

For the consequences: if $\phi \equiv \psi$ then ${\phi }^{\neg }\equiv {\psi }^{\neg }$ (negating atoms is a uniform substitution, which preserves equality of truth functions by the argument of Theorem Uniform substitution preserves tautologies), so the negations are equivalent and hence so are the duals. And $\phi$ is a tautology iff ${\phi }^{\neg }$ is — since $v\mapsto 1-v$ is a bijection of valuations — iff $\neg ({\phi }^{\neg })$ is a contradiction, iff ${\phi }^d$ is.∎

Proof. (1) $v(\neg \phi )=1$ iff $v(\phi )=0$. So $\neg \phi$ has a model iff $\phi$ has a falsifying valuation, and $\phi$ is a tautology iff no such valuation exists. (2) is (1) applied to $\neg \phi$ together with $\neg \neg \phi \equiv \phi$. (3) By Lemma Relevance only the $2^n$ patterns on $\mathrm{At}(\phi )$ matter, and $\phi$ is true on all of them, none of them, or some but not all.∎

Proof. Suppose $\Sigma \models \phi$ and let $v\models \Sigma \cup \{\neg \phi \}$. Then $v\models \Sigma$, so $v(\phi )=1$; but $v(\neg \phi )=1$ gives $v(\phi )=0$, a contradiction, so no such $v$ exists. Conversely, suppose $\Sigma \cup \{\neg \phi \}$ is unsatisfiable and let $v\models \Sigma$. Then $v/\models \neg \phi$, i.e. $v(\phi )=1$. Hence every model of $\Sigma$ models $\phi$.∎

Proof. By Lemma Relevance it suffices to test valuations of $\mathrm{At}(\phi )$, of which there are $2^n$. Each evaluation is a single bottom-up pass over the parse tree, linear in the length of $\phi$. Return "satisfiable" at the first valuation giving $1$, and "unsatisfiable" if all fail.∎

Proof. Sketch. Membership in NP is immediate: a satisfying valuation is a certificate of size $n$, checkable in linear time by Proposition Brute force works, slowly applied to one valuation. For hardness one shows that every language decided by a nondeterministic Turing machine $M$ in time $p(n)$ reduces to SAT: introduce atoms $x_{i,j,s}$ meaning "at step $i$, tape cell $j$ holds symbol $s$ ", together with atoms for head position and state, and write down clauses asserting that the initial configuration is correct, that exactly one symbol occupies each cell at each step, that successive configurations are related by $M$ 's transition table, and that some configuration is accepting. The resulting formula is polynomial in $p(n)$ and is satisfiable exactly when $M$ accepts. Reducing arbitrary clauses to $3$ -literal clauses is the Tseitin-style splitting of Theorem Tseitin transformation below. This proof rests on the formal model of nondeterministic computation, which is outside this chapter.∎

Proof. Sketch. Read each two-literal clause ${\ell }_1\vee {\ell }_2$ as the pair of implications $\neg {\ell }_1\to {\ell }_2$ and $\neg {\ell }_2\to {\ell }_1$, and build the directed implication graph whose vertices are the $2n$ literals and whose edges are these implications. The graph is skew-symmetric: an edge $\ell \to m$ is present exactly when $\neg m\to \neg \ell$ is. One shows the clause set is unsatisfiable if and only if some atom $p$ has $p$ and $\neg p$ in the same strongly connected component, and Tarjan's algorithm finds the components in linear time. The argument that this criterion is correct uses the fact that within a component all literals must take the same value, which rests on graph theory rather than logic.∎

Proof. Let $\phi$ have atoms $p_1,\dots ,p_n$ and let $f$ be its truth function.

For DNF: if $f$ is identically $0$, take the term $p_1\wedge \neg p_1$. Otherwise the formula ${\bigvee }_{a:f(a)=1}{\chi }_a$ built in the proof of Theorem Functional completeness of the standard set is a disjunction of terms equivalent to $\phi$ — this is the full DNF, one term per satisfying row.

For CNF, apply the same construction to $\neg \phi$ to get a DNF $\delta \equiv \neg \phi$, so $\phi \equiv \neg \delta$. Pushing the negation inward with De Morgan from Theorem The basic equivalences turns the disjunction of terms into a conjunction of clauses: each term ${\ell }_1\wedge \cdots \wedge {\ell }_n$ becomes the clause ${\bar{\ell }}_1\vee \cdots \vee {\bar{\ell }}_n$, where $\bar{\ell }$ is the complement of $\ell$. The result is a CNF equivalent to $\phi$ with one clause per falsifying row of $\phi$.∎

Proof. Steps 1 and 2 first. Each application of the $\leftrightarrow$ or $\to$ rule strictly decreases the number of occurrences of $\leftrightarrow$ and $\to$ in the outermost position and introduces none of higher rank, so measuring by the multiset of ranks of remaining $\leftrightarrow$ and $\to$ occurrences gives a strictly decreasing well-founded measure; step 1 halts. In step 2, assign to each formula the measure $m(\phi )=\sum$ over occurrences of $\neg$ of the rank of the subformula it governs. De Morgan replaces one negation of rank $r$ by two of rank $r-1$, dropping the sum, and $\neg \neg \alpha ⇝\alpha$ removes two negations outright. Since $m$ is a natural number and strictly decreases, step 2 halts, and it can only halt when every $\neg$ governs a rank-$0$ subformula, i.e. an atom — that is NNF.

For step 3, define for an NNF formula the measure $c(\phi )$ = the number of terminal positions in the distributive expansion, by $c(\ell )=1$ for a literal, $c(\alpha \wedge \beta )=c(\alpha )+c(\beta )$, and $c(\alpha \vee \beta )=c(\alpha )c(\beta )$. Applying the distributive rule to $\alpha \vee (\beta \wedge \gamma )$ replaces a subformula of measure $c(\alpha )(c(\beta )+c(\gamma ))$ by one of measure $c(\alpha )c(\beta )+c(\alpha )c(\gamma )$ — equal. So $c$ alone does not decrease; instead use the pair $(c(\phi ),k(\phi ))$ ordered lexicographically, where $k$ counts occurrences of $\wedge$ that lie in the scope of some $\vee$. The rewrite leaves $c$ unchanged and strictly decreases $k$, since the rewritten $\wedge$ moves to the top of that subformula and no $\wedge$ enters the scope of a new $\vee$. Hence step 3 halts, and it halts only when no $\wedge$ is under a $\vee$ — which for an NNF formula means a conjunction of disjunctions of literals, i.e. CNF.∎

Proof. Let $\psi$ be a CNF equivalent to ${\phi }_n$. For each $a=(a_1,\dots ,a_n)\in \{1,2{\}}^n$ define the valuation $v_a$ that sets, in the $i$ -th pair, the variable selected by $a_i$ to $0$ and the other to $1$ — so $p_i\wedge q_i$ fails for every $i$ and $v_a({\phi }_n)=0$. Hence $v_a$ falsifies some clause $C_a$ of $\psi$.

We claim $C_a$ must contain, for every $i$, a literal made false by $v_a$ from the $i$ -th pair — indeed $C_a$ contains only literals false under $v_a$, and we claim it mentions all $n$ pairs. Suppose it omits pair $j$ entirely. Modify $v_a$ to $v^{\prime }$ by setting both $p_j$ and $q_j$ to $1$. This changes no literal of $C_a$, so $v^{\prime }$ still falsifies $C_a$ and hence $v^{\prime }(\psi )=0$; but $v^{\prime }(p_j\wedge q_j)=1$, so $v^{\prime }({\phi }_n)=1$, contradicting $\psi \equiv {\phi }_n$. So $C_a$ mentions every pair, and the literals it contains from pair $i$ are exactly those false under $v_a$, which identifies $a_i$. Therefore $a\mapsto C_a$ is injective, and $\psi$ has at least $|\{1,2{\}}^n|=2^n$ clauses.∎

Proof. Introduce a fresh atom $x_{\alpha }$ for each non-atomic subformula $\alpha$ of $\phi$. For each such $\alpha$ with principal connective $\ast$ and immediate constituents $\beta ,\gamma$, write down the CNF of the biconditional $x_{\alpha }\leftrightarrow (y_{\beta }\ast y_{\gamma })$, where $y_{\delta }$ is $\delta$ itself if $\delta$ is a literal and $x_{\delta }$ otherwise. Each such biconditional involves at most three atoms, so its CNF has at most four clauses of at most three literals — a constant per subformula. Let $T(\phi )$ be the conjunction of all of these together with the unit clause $x_{\phi }$.

If $v\models \phi$, extend $v$ by setting $x_{\alpha }:=v(\alpha )$ for each subformula; every biconditional then holds by construction and $x_{\phi }$ is true, so $T(\phi )$ is satisfiable. Conversely, if $w\models T(\phi )$, an induction on rank using the biconditionals shows $w(x_{\alpha })=w(\alpha )$ for every subformula $\alpha$; the clause $x_{\phi }$ then gives $w(\phi )=1$. Size and time are linear because $\phi$ has at most $|\phi |$ subformulas and each contributes a bounded number of clauses.∎

Proof. Let $C={\mathrm{Res}}_p(C_1,C_2)$ and let $v$ be a model of $C_1$ and $C_2$. Consider $v(p)$. If $v(p)=1$ then $v$ falsifies the literal $\neg p$, so to satisfy $C_2$ it must satisfy some literal of $C_2\setminus \{\neg p\}\subseteq C$. If $v(p)=0$ then $v$ falsifies $p$, so to satisfy $C_1$ it must satisfy some literal of $C_1\setminus \{p\}\subseteq C$. Either way $v(C)=1$.

Now suppose $S$ has a refutation. An induction along the derivation, using the case just proved at each resolution step, shows every clause in it is entailed by $S$. In particular $S\models \square$. But $\square$ is false under every valuation, so $S$ has no model.∎

Proof. Induct on the number $n$ of atoms occurring in $S$.

If $n=0$, the only clause available is $\square$ itself, and a clause set with no atoms is unsatisfiable only if $\square \in S$ — a refutation of length one.

Let $n\ge 1$, pick an atom $p$ of $S$, and form two clause sets. Let $S_1$ be obtained by deleting every clause containing $\neg p$ and deleting the literal $p$ from the clauses that remain; let $S_0$ be obtained symmetrically, deleting clauses containing $p$ and removing $\neg p$ from the rest. Both are clause sets over the remaining $n-1$ atoms. $S_1$ is exactly the residue of $S$ under the assumption $v(p)=1$, and $S_0$ the residue under $v(p)=0$; since $S$ is unsatisfiable, neither residue is satisfiable — a model of $S_1$ over the other atoms would extend, by setting $p$ to $1$, to a model of $S$, and likewise for $S_0$ with $p$ set to $0$.

By the induction hypothesis $S_1$ has a refutation $R_1$ and $S_0$ has a refutation $R_0$. Reinstate the deleted literals: replaying $R_1$ on the original clauses of $S$ yields a derivation from $S$ of either $\square$ — in which case we are done — or the unit clause $\{\neg p\}$, since the only literal that could have been dropped along the way is $\neg p$. Symmetrically $R_0$ yields from $S$ either $\square$ or $\{p\}$. In the remaining case we have derived both $\{p\}$ and $\{\neg p\}$ from $S$, and one further resolution step on $p$ produces $\square$. Concatenating the two replayed derivations and that final step is a refutation of $S$.∎

Proof. ($\Rightarrow$) A model of $\Sigma$ models each of its subsets.

($\Leftarrow$) Assume every finite subset of $\Sigma$ is satisfiable; call such a $\Sigma$ finitely satisfiable. Suppose first that the language is countable, with atoms $p_0,p_1,p_2,\dots$, and build a valuation one atom at a time. Set ${\Sigma }_0=\Sigma$, and having a finitely satisfiable ${\Sigma }_k$, define

The second branch is legitimate: if both ${\Sigma }_k\cup \{p_k\}$ and ${\Sigma }_k\cup \{\neg p_k\}$ failed to be finitely satisfiable, there would be finite $A,B\subseteq {\Sigma }_k$ with $A\cup \{p_k\}$ and $B\cup \{\neg p_k\}$ unsatisfiable. Then $A\cup B$ is a finite subset of ${\Sigma }_k$, hence has a model $w$; but $w(p_k)$ is either $1$, making $w$ a model of $A\cup \{p_k\}$, or $0$, making it a model of $B\cup \{\neg p_k\}$. Either way a contradiction. So ${\Sigma }_{k+1}$ is finitely satisfiable, and by induction every ${\Sigma }_k$ is.

Let ${\Sigma }_{\infty }={\bigcup }_k{\Sigma }_k$ and define $v(p_k)=1$ if $p_k\in {\Sigma }_{\infty }$ and $0$ otherwise. We claim $v\models \Sigma$. Let $\sigma \in \Sigma$ and let $p_{k_1},\dots ,p_{k_m}$ be its atoms, with $K$ larger than every $k_j$. The set $F=\{\sigma \}\cup \{{\ell }_k:k<K\}$, where ${\ell }_k$ is whichever of $p_k,\neg p_k$ was placed into ${\Sigma }_{k+1}$, is a finite subset of ${\Sigma }_K$ and so has a model $u$. Each ${\ell }_k\in F$ forces $u(p_k)=v(p_k)$ for all $k<K$, so $u$ and $v$ agree on $\mathrm{At}(\sigma )$, and Lemma Relevance gives $v(\sigma )=u(\sigma )=1$.