Logic

logic is the study of valid inference: which conclusions are forced by which premises, independent of what the premises are about. 𐃏 it splits cleanly into a syntax (formulas, and rules for pushing them around) and a semantics (truth assignments, models), and the deepest theorems in the subject are exactly the ones that say when the two agree (Epp, Susanna S., 2019).

propositional logic#

connectives#

atomic propositions \(p, q, r\) are statements that are either true or false. compound propositions are built with the connectives \(\lnot\) (not), \(\land\) (and), \(\lor\) (or), \(\oplus\) (exclusive or), \(\to\) (implies), \(\leftrightarrow\) (iff). semantics by truth table:

the only row that ever surprises anyone: \(p \to q\) is true whenever \(p\) is false. 𐃏 “if pigs fly then i am the pope” is vacuously true. the implication is logically equivalent to \(\lnot p \lor q\), which is the form every SAT solver actually stores.

two equivalences worth memorising because they generate most simplification work:

• de morgan: \(\lnot(p \land q) \equiv \lnot p \lor \lnot q\) and \(\lnot(p \lor q) \equiv \lnot p \land \lnot q\)
• contrapositive: \(p \to q \equiv \lnot q \to \lnot p\) (but NOT \(\equiv q \to p\), the converse)

tautology, satisfiability, equivalence#

for a formula \(\varphi\) over \(n\) variables there are \(2^n\) truth assignments. \(\varphi\) is

• a tautology if every assignment makes it true (e.g. \(p \lor \lnot p\)),
• satisfiable if at least one does,
• a contradiction if none does (e.g. \(p \land \lnot p\)),

and \(\varphi \equiv \psi\) iff \(\varphi \leftrightarrow \psi\) is a tautology. the three notions interlock: \(\varphi\) is a tautology iff \(\lnot\varphi\) is unsatisfiable — which is why theorem proving and SAT solving are the same problem wearing different hats.

normal forms#

• DNF (disjunctive normal form): an OR of ANDs of literals. read it straight off the truth table — one conjunct per true row. for \(p \oplus q\): rows TF and FT give \((p \land \lnot q) \lor (\lnot p \land q)\).
• CNF (conjunctive normal form): an AND of ORs (clauses). one clause per false row, negating that row’s assignment. for \(p \oplus q\): rows TT and FF give \((\lnot p \lor \lnot q) \land (p \lor q)\).

every formula therefore has both a DNF and a CNF — but the truth-table construction can blow up exponentially. the tseitin transformation fixes this for CNF: by introducing one fresh variable per subformula it produces an equisatisfiable (not equivalent) CNF of linear size, which is why CNF is the universal input format for SAT solvers.

functional completeness#

a connective set is functionally complete if it can express every boolean function. \(\{\lnot, \land, \lor\}\) is complete — the DNF construction above builds any function from its truth table. NAND alone (\(p \uparrow q \equiv \lnot(p \land q)\)) is also complete:

\begin{align*} \lnot p &\equiv p \uparrow p \\ p \land q &\equiv \lnot(p \uparrow q) \equiv (p \uparrow q) \uparrow (p \uparrow q) \\ p \lor q &\equiv (p \uparrow p) \uparrow (q \uparrow q) \end{align*}

each right-hand side uses only \(\uparrow\), and together they simulate a complete set, so \(\{\uparrow\}\) is complete. 𐃏 NOR (\(\downarrow\)) is complete by the dual argument; \(\{\land, \lor\}\) without negation is not — it is monotone (flipping an input from F to T can never flip the output from T to F), so \(\lnot p\) is out of reach.

rules of inference#

semantics checks all \(2^n\) rows; deduction builds arguments row-free. an inference rule licenses a conclusion from premises; a proof is a chain of rule applications. the standard toolkit:

each rule is sound: whenever the premises are true, the conclusion is true (check with a truth table — modus ponens is the tautology \(((p \to q) \land p) \to q\), machine-verified below). the two classic fallacies are the rules that are not here: affirming the consequent (\(q,\; p \to q \;\therefore\; p\)) and denying the antecedent (\(\lnot p,\; p \to q \;\therefore\; \lnot q\)) — both fail on the row \(p = \mathrm{F}, q = \mathrm{T}\).

first-order logic#

propositional logic cannot even say “all men are mortal” — its atoms have no insides. first-order logic (FOL) adds:

• terms: variables, constants, function applications \(f(x, c)\)
• predicates: \(P(x)\), \(x < y\) — atomic formulas about terms
• quantifiers: \(\forall x\) (for all), \(\exists x\) (there exists)

models and satisfaction#

a formula on its own is neither true nor false; truth is relative to a model (structure) \(\mathcal{M} = (D, I)\): a non-empty domain \(D\) plus an interpretation \(I\) assigning meanings to the constant, function and predicate symbols. write \(\mathcal{M} \models \varphi\) for “\(\varphi\) is true in \(\mathcal{M}\)”, defined by recursion on the formula (tarski’s definition): \(\mathcal{M} \models \forall x\, \varphi\) iff \(\varphi\) holds for every choice of \(x\) from \(D\), and so on.

the same sentence changes truth value as the model changes — that is the whole point:

• \(\forall x\, \exists y\; (y > x)\) — true over \(\mathbb{Z}\), true over \(\mathbb{N}\), false over any finite ordered domain.
• \(\exists y\, \forall x\; (y \le x)\) — false over \(\mathbb{Z}\) (no least integer), true over \(\mathbb{N}\) (namely \(y = 0\)).

quantifier order matters: \(\forall x\, \exists y\; (y > x)\) (“everyone has someone above them”) is much weaker than \(\exists y\, \forall x\; (y > x)\) (“someone is above everyone” — false in any model with order irreflexive, since \(y > y\) fails). negation pushes through quantifiers by the FOL de morgan laws:

\begin{equation} \lnot \forall x\, \varphi \;\equiv\; \exists x\, \lnot\varphi, \qquad \lnot \exists x\, \varphi \;\equiv\; \forall x\, \lnot\varphi. \end{equation}

a sentence is valid if true in every model (\(\models \varphi\)), satisfiable if true in some model. unlike the propositional case there is no truth-table check — the space of models is infinite — and by church and turing, validity of FOL sentences is undecidable.

soundness and completeness#

fix a proof system (natural deduction, say) and write \(\Gamma \vdash \varphi\) for “\(\varphi\) is derivable from assumptions \(\Gamma\)”, and \(\Gamma \models \varphi\) for “every model of \(\Gamma\) is a model of \(\varphi\)”. the two headline theorems:

• soundness: \(\Gamma \vdash \varphi \implies \Gamma \models \varphi\). the calculus proves nothing false. proved by induction on derivations — each rule preserves truth.
• completeness (gödel, 1929): \(\Gamma \models \varphi \implies \Gamma \vdash \varphi\), for first-order logic. every semantic consequence has a formal proof.¹

a corollary of completeness worth its own line: compactness — if every finite subset of \(\Gamma\) has a model, so does \(\Gamma\) (any proof of a contradiction would use only finitely many assumptions). compactness powers non-standard analysis and half of model theory.

proof techniques#

the working mathematician’s compiler targets. to prove \(p \to q\) (Velleman, Daniel J., 2006):

• direct: assume \(p\), chain forward to \(q\). example: if \(m, n\) are even then \(m + n\) is even. \(m = 2a\), \(n = 2b\), so \(m + n = 2(a + b)\). done.
• contrapositive: prove \(\lnot q \to \lnot p\) instead — logically the same statement, often structurally easier. example: if \(n^2\) is even then \(n\) is even. contrapositive: \(n\) odd \(\implies n^2\) odd. \(n = 2k+1 \implies n^2 = 2(2k^2 + 2k) + 1\). done. (the direct route from “\(n^2\) even” is awkward — you would have to factor \(n^2\).)
• contradiction: assume \(p \land \lnot q\), derive absurdity. example: \(\sqrt{2}\) is irrational. suppose \(\sqrt{2} = a/b\) in lowest terms. then \(a^2 = 2b^2\), so \(a^2\) is even, so \(a\) is even (previous bullet!), say \(a = 2c\). then \(4c^2 = 2b^2\), i.e. \(b^2 = 2c^2\), so \(b\) is even too — contradicting lowest terms.
• induction: to prove \(\forall n \ge n_0\; P(n)\): establish \(P(n_0)\) (base), and \(P(k) \to P(k+1)\) for arbitrary \(k \ge n_0\) (step). example: \(\sum_{i=1}^{n} i = n(n+1)/2\). base: \(n=1\), both sides \(1\). step: \(\sum_{i=1}^{k+1} i = k(k+1)/2 + (k+1) = (k+1)(k+2)/2\).
• strong induction: assume \(P(n_0), \dots, P(k)\) all hold in the step. example: every integer \(n \ge 2\) is a product of primes — if \(n\) is prime, done; else \(n = ab\) with \(2 \le a, b < n\), and both factor by the strong hypothesis.

the well-ordering principle#

WOP: every non-empty subset of \(\mathbb{N}\) has a least element. this is equivalent to induction, and it is the engine inside “minimal counterexample” proofs: to prove \(\forall n\, P(n)\), suppose the set of counterexamples \(C = \{n : \lnot P(n)\}\) is non-empty, take its least element \(m\) by WOP, and derive a contradiction — typically by manufacturing a smaller counterexample. 𐃏 one direction of the equivalence: assume induction, and let \(C \subseteq \mathbb{N}\) have no least element; let \(Q(n)\) say “no element of \(C\) is \(\le n\)”; then \(Q(0)\) holds (else \(0\) would be least in \(C\)) and \(Q(k) \to Q(k+1)\) (else \(k+1\) would be least), so by induction \(Q\) holds everywhere and \(C\) is empty.

SAT and resolution#

the problem#

SAT: given a CNF formula, decide whether some assignment satisfies it. this was the first problem ever proved NP-complete (the cook–levin theorem (Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford, 2009)) — every problem in NP reduces to it — yet modern conflict-driven solvers routinely dispatch industrial instances with millions of variables. the gap between worst case and practice is one of the standing embarrassments (or miracles) of the field.

resolution#

a single inference rule suffices for CNF refutation:

\begin{equation} \frac{C \lor p \qquad D \lor \lnot p}{C \lor D} \end{equation}

resolve two clauses on a complementary literal pair, keep the union of the rest. resolution is sound, and refutation-complete: a CNF set is unsatisfiable iff the empty clause \(\square\) is derivable from it by resolution.

worked example. show \(\{\,p \lor q,\;\; \lnot p \lor q,\;\; p \lor \lnot q,\;\; \lnot p \lor \lnot q\,\}\) is unsatisfiable (it demands every combination of values for \(p\) and \(q\) be avoided at once):

1. resolve \(p \lor q\) with \(\lnot p \lor q\) on \(p\): get \(q\).
2. resolve \(p \lor \lnot q\) with \(\lnot p \lor \lnot q\) on \(p\): get \(\lnot q\).
3. resolve \(q\) with \(\lnot q\): get \(\square\). unsatisfiable.

a DPLL-lite solver#

the DPLL algorithm (1962, still the skeleton of every modern solver) is depth-first search plus one crucial deduction: unit propagation — a clause reduced to a single literal forces that literal’s value, and the forcing cascades. below: a brute-force truth-table checker (to machine-verify modus ponens) and a miniature DPLL.

from itertools import product

# --- part 1: brute force over truth tables ---------------------------------
def brute(n_vars, formula):
    """return (tautology?, satisfiable?, #models) by trying all 2^n rows."""
    models = [v for v in product([False, True], repeat=n_vars) if formula(*v)]
    return len(models) == 2 ** n_vars, len(models) > 0, len(models)

mp   = lambda p, q: ((not p or q) and p) <= q   # ((p -> q) and p) -> q
xor3 = lambda p, q, r: (p ^ q ^ r)              # parity on 3 bits

for name, n, f in [("modus ponens schema", 2, mp),
                   ("p xor q xor r", 3, xor3)]:
    taut, sat, k = brute(n, f)
    print(f"{name:22s} tautology={taut!s:5s} satisfiable={sat!s:5s} models={k}")

# --- part 2: DPLL-lite on CNF (clauses = frozensets of signed ints) ---------
def unit_propagate(clauses, assign):
    changed = True
    while changed:
        changed = False
        for c in clauses:
            if len(c) == 1:
                (lit,) = c
                assign[abs(lit)] = lit > 0
                clauses = simplify(clauses, lit)
                if clauses is None:
                    return None, assign
                changed = True
                break
    return clauses, assign

def simplify(clauses, lit):
    out = []
    for c in clauses:
        if lit in c:
            continue                      # clause satisfied
        if -lit in c:
            c = c - {-lit}                # literal falsified, drop it
            if not c:
                return None               # empty clause: conflict
        out.append(c)
    return out

def dpll(clauses, assign=None, depth=0):
    assign = dict(assign or {})
    clauses, assign = unit_propagate([frozenset(c) for c in clauses], assign)
    if clauses is None:
        print("  " * depth + "conflict (empty clause)")
        return None
    if not clauses:
        return assign                     # all clauses satisfied
    lit = min(min(abs(l) for l in c) for c in clauses)  # smallest unassigned var
    print("  " * depth + f"branch on x{lit}")
    for guess in (lit, -lit):
        s = simplify(clauses, guess)
        if s is not None:
            r = dpll(s, {**assign, abs(guess): guess > 0}, depth + 1)
            if r is not None:
                return r
    return None

# the 4-clause unsatisfiable set from the resolution example (1=p, 2=q)
unsat = [{1, 2}, {-1, 2}, {1, -2}, {-1, -2}]
print("\nDPLL on {p|q, ~p|q, p|~q, ~p|~q}:")
print("result:", dpll(unsat))

# a satisfiable instance: (p|q|r) & (~p|q) & (~q|r) & (~r|p)
sat_inst = [{1, 2, 3}, {-1, 2}, {-2, 3}, {-3, 1}]
print("\nDPLL on {p|q|r, ~p|q, ~q|r, ~r|p}:")
print("result:", dpll(sat_inst))

modus ponens schema    tautology=True  satisfiable=True  models=4
p xor q xor r          tautology=False satisfiable=True  models=4

DPLL on {p|q, ~p|q, p|~q, ~p|~q}:
branch on x1
  conflict (empty clause)
  conflict (empty clause)
result: None

DPLL on {p|q|r, ~p|q, ~q|r, ~r|p}:
branch on x1
result: {1: True, 2: True, 3: True}

read the traces: on the unsatisfiable set, guessing \(p\) either way triggers a unit-propagation cascade into the empty clause — the solver’s two conflicts mirror the two halves of the resolution tree above. on the satisfiable instance, one branch on \(p = \mathrm{T}\) lets propagation finish the job: the clauses \(\lnot p \lor q\) and \(\lnot q \lor r\) fire as units, yielding the model \(p = q = r = \mathrm{T}\).

see also#

• sets, functions and sequences — de morgan’s laws in their set-theoretic costume
• number theory — induction and WOP doing real work (euclid’s algorithm, unique factorisation)
• graph theory — where “minimal counterexample” proofs earn their keep
• classical algorithms — backtracking, DPLL’s family tree

References#

Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford (2009). Introduction to Algorithms, MIT Press.

Epp, Susanna S. (2019). Discrete Mathematics with Applications, Cengage Learning.

Velleman, Daniel J. (2006). How to Prove It: A Structured Approach, Cambridge University Press.