Logic formulas

The usual first step (after rewriting $\leftrightarrow$) when converting to CNF or DNF.

True exactly when p and q have the same truth value.

The converse $q\to p$ and the inverse $\neg p\to \neg q$ are NOT equivalent to $p\to q$ (they are equivalent to each other).

Double negation: $\neg \neg p\equiv p$.

$\neg (p\leftrightarrow q)$ is the exclusive or $p\oplus q$: true exactly when $p$ and $q$ differ. The negation of an implication is a conjunction, never another implication.

Each of $\wedge$ and $\vee$ distributes over the other; used to reach CNF and DNF.

Moves a conjunction in the premise into a chain of implications.

Check any of these by rewriting both sides with $p\to q\equiv \neg p\vee q$. Note the second line: a conjunctive premise splits into an OR, not an AND.

$\phi \models \psi$ means every assignment making $\phi$ true also makes $\psi$ true. With several premises: ${\phi }_1,\dots ,{\phi }_k\models \psi$ exactly when $({\phi }_1\wedge \cdots \wedge {\phi }_k)\to \psi$ is a tautology.

The basis of proof by contradiction and of resolution refutation.

A minterm is true exactly on its row; a maxterm is false exactly on its row. In the maxterm, a variable that is T in the row appears negated and one that is F appears plain (for the row $p=\mathrm{T},q=\mathrm{F}$ the maxterm is $\neg p\vee q$). A formula with no T rows has an empty DNF (a contradiction); one with no F rows has an empty CNF (a tautology).

Applies to two clauses holding a complementary pair of literals. The resolvent is entailed by its two parents (soundness). Resolution refutation is also complete for propositional logic: if a clause set is unsatisfiable, the empty clause can be derived from it.

Negation flips the quantifier and moves inside; apply De Morgan's laws to what remains.

When both P and Q contain x free, only these two distribute as equivalences.

Valid when $x$ does not occur free in $Q$ and the domain is non-empty.

Valid when $x$ does not occur free in $Q$ and the domain is non-empty. A quantifier moved out of the conclusion stays the same; one moved out of the premise FLIPS ($\forall$ becomes $\exists$ and vice versa), because the premise sits under a hidden negation: $P(x)\to Q\equiv \neg P(x)\vee Q$.

The converse of each is NOT valid.

The first needs the non-empty domain. None of the converses is valid: for example, with domain $\{1,2\}$, $P(1)$ true, $P(2)$ false and $Q(1)$ false, $\forall xP\to \forall xQ$ is true but $\forall x(P\to Q)$ is false.

Like quantifiers commute: $\forall x\forall y\equiv \forall y\forall x$ and $\exists x\exists y\equiv \exists y\exists x$.

Clauses must share no variable names (standardise apart); the empty clause again signals unsatisfiability of the clause set. Resolution together with factoring (unifying two literals inside one clause) is refutation-complete for first-order logic: an unsatisfiable clause set always yields the empty clause. If the set is satisfiable the search may never stop, since first-order entailment is only semi-decidable.