1. Logic and Proofs

Logic gives mathematics and computer science a precise language. In that language, "true", "false", "for all" and "therefore" each have exactly one meaning. This chapter starts with propositions and the connectives that combine them, extends them with predicates and quantifiers, and then uses rules of inference and standard proof techniques to build arguments that are guaranteed to be correct. Every later chapter relies on these tools. The same ideas also appear in everyday programming, in boolean conditions, assertions, database queries, type systems and SAT solvers.

<a id="11-propositional-logic"></a>

1.1 Propositional Logic

Propositional logic treats whole statements as atomic units that are either true or false, and studies how connectives combine them into larger statements.

Propositions and Truth Values

Why. Natural language is ambiguous. "The system is secure" means different things to different people. Before we can reason rigorously, we need statements whose truth is not open to interpretation.

What. A proposition is a declarative sentence that is either true or false, but not both. Its truth value is written T/F (or 1/0). Propositions are usually named with propositional variables such as p, q, r.

• An atomic proposition cannot be broken into smaller propositions ("7 is prime").
• A compound proposition is built from others using connectives ("7 is prime and 7 is odd").

Propositional logic assumes bivalence: every proposition has exactly one of the two truth values, even if we do not yet know which one.

Sentence	Proposition?	Reason
"7 is prime."	Yes (T)	Declarative, definite truth value
"2 + 2 = 5."	Yes (F)	False propositions are still propositions
"Every even integer greater than 2 is a sum of two primes."	Yes (unknown)	Goldbach's conjecture: the truth value exists but has not been determined
"x + 1 = 3."	No	Truth depends on x (this is a predicate, see 1.2)
"Close the door."	No	Command, not a statement
"Is it raining?"	No	Question
"This sentence is false."	No	Paradox: neither value can be assigned consistently

Analogy. A proposition behaves like a boolean constant in a program. Once it is evaluated, it is fixed. A sentence with an unbound variable is more like a function that has not been called yet.

# Propositions: fixed truth values
p = 7 % 2 == 1          # "7 is odd"   -> True
q = 2 + 2 == 5          # "2 + 2 = 5"  -> False

# Not a proposition: the truth value depends on x (a predicate, see 1.2)
def x_plus_one_is_three(x):
    return x + 1 == 3

x_plus_one_is_three(2)  # True  -- only after choosing x do we get a proposition
x_plus_one_is_three(5)  # False

Key takeaways

• A proposition is a declarative sentence with exactly one truth value, either T or F.
• Not knowing the truth value does not stop a sentence from being a proposition. Depending on a free variable does.
• Questions, commands, and self-referential paradoxes are not propositions.
• Compound propositions are built from atomic ones with connectives.

Practice

1. (Beginner) Classify each as a proposition or not, and give the truth value where possible: "1 + 1 = 10", "Delete this file.", "There are infinitely many primes.", "x > 0".
2. (Intermediate) Explain why "Tomorrow it will rain" can be treated as a proposition, while "It is raining here" cannot be treated as one without more context. What extra information turns the second into a proposition?
3. (Interview) Is the sentence "This statement is false" a proposition? Relate your answer to why a function def f(): return not f() cannot produce a boolean. Hint: try assigning T, then F, and follow the consequences.

Logical Connectives

Why. Real conditions are rarely atomic. "The user is logged in and is not banned" combines two simpler facts. Connectives are the operators that build compound propositions, in the same way that + and * build arithmetic expressions.

What. The standard connectives, with their counterparts in code:

Symbol	Name	Read as	True exactly when	Python	C / Java / JS
¬p	Negation	not p	p is false	not p	!p
p ∧ q	Conjunction	p and q	both are true	p and q	p && q
p ∨ q	Disjunction	p or q	at least one is true	p or q	p || q
p ⊕ q	Exclusive or	p xor q	exactly one is true	p != q	p != q
p → q	Conditional	if p then q	not (p true and q false)	(not p) or q	!p || q
p ↔ q	Biconditional	p if and only if q	both have the same value	p == q	p == q

Inclusive vs exclusive or. In logic, "or" is inclusive: p ∨ q is true when both are true. English often means the exclusive version ("soup or salad comes with the meal"). When you need exactly one, use ⊕.

Precedence. From tightest to loosest binding: ¬, ∧, ∨, →, ↔. So:

¬p ∧ q ∨ r → s      parses as      ((¬p ∧ q) ∨ r) → s

By convention → associates to the right (p → q → r means p → (q → r)), but explicit parentheses are always clearer.

def NOT(p):        return not p
def AND(p, q):     return p and q
def OR(p, q):      return p or q
def XOR(p, q):     return p != q          # on booleans, "different" means exactly one is true
def IMPLIES(p, q): return (not p) or q    # false only for p=True, q=False
def IFF(p, q):     return p == q

# Short-circuiting: Python stops evaluating as soon as the result is known
def expensive():
    print("evaluated")
    return True

False and expensive()   # prints nothing: False ∧ anything is False
True or expensive()     # prints nothing: True ∨ anything is True

Key takeaways

• ¬, ∧, ∨, ⊕, →, ↔ are the core connectives. Each one is fully defined by its truth table.
• Logical "or" is inclusive. Use ⊕ for "exactly one".
• Precedence is ¬ > ∧ > ∨ > → > ↔. Add parentheses whenever there could be doubt.
• Most languages have no implication operator. Write p → q as !p || q.

Practice

1. (Beginner) Let p = "it is sunny" and q = "I go running". Write in English: ¬p ∧ q, p → q, ¬(p ∨ q).
2. (Intermediate) Fully parenthesize p ∨ ¬q ∧ r → p ↔ q according to standard precedence.
3. (Interview) Python has no implication operator, yet p <= q correctly computes p → q for booleans. Explain why. Hint: in Python, False < True. Compare the four cases with the truth table of →.

Truth Tables

Why. A compound proposition can have many variables, and intuition about it is unreliable. A truth table is a mechanical, exhaustive procedure: it lists every possible assignment of truth values and the resulting value of the formula. Nothing is left to judgment.

How.

1. List the variables. With n variables there are 2ⁿ rows.
2. Enumerate the assignments systematically, for example by counting in binary from all-T down to all-F.
3. Add one column per subformula, working from the innermost outward.
4. The final column is the value of the whole formula.

Example: (p ∨ q) ∧ ¬(p ∧ q)

p	q	p ∨ q	p ∧ q	¬(p ∧ q)	(p ∨ q) ∧ ¬(p ∧ q)
T	T	T	T	F	F
T	F	T	F	T	T
F	T	T	F	T	T
F	F	F	F	T	F

The final column matches p ⊕ q, so this formula is one way to express exclusive or using only ∧, ∨, ¬.

from itertools import product

def truth_table(variables, formula):
    """Print the truth table of formula, a function taking len(variables) booleans."""
    print(" | ".join(variables) + " | result")
    for values in product([True, False], repeat=len(variables)):  # all 2^n assignments
        cells = ["T" if v else "F" for v in values]
        result = "T" if formula(*values) else "F"
        print(" | ".join(cells) + " | " + result)

truth_table(["p", "q"], lambda p, q: (p or q) and not (p and q))
# p | q | result
# T | T | F
# T | F | T
# F | T | T
# F | F | F

Cost. Truth tables grow exponentially. 10 variables need 1,024 rows, and 50 variables need about 10¹⁵. This exponential growth is why satisfiability (below) is a hard computational problem.

Key takeaways

• A truth table evaluates a formula under all 2ⁿ assignments of its n variables.
• Build intermediate columns for subformulas to avoid mistakes.
• Two formulas with identical final columns are logically equivalent.
• The method is complete but exponential, so it only scales to small formulas.

Practice

1. (Beginner) Build the truth table for p → (q ∨ ¬r). How many rows evaluate to F?
2. (Intermediate) A formula has 6 variables. How many rows does its truth table have? How many distinct boolean functions of 6 variables exist?
3. (Interview) Given two boolean expressions over n variables, describe an algorithm to decide whether they always produce the same result, and state its complexity. Hint: consider the truth table of their XOR. Is a better worst case likely? Look ahead to Satisfiability.

Conditional and Biconditional Statements

Why. "If ... then ..." is the shape of almost every mathematical theorem and every program requirement. Its truth table surprises most beginners, so it deserves careful study.

The conditional p → q. p is the hypothesis (antecedent) and q is the conclusion (consequent). The statement is false in only one situation: the hypothesis holds and the conclusion fails.

Analogy: a promise. "If you get an A, I will give you $10."

• You get an A and receive $10: promise kept (T).
• You get an A and do not receive $10: promise broken (F).
• You do not get an A: whatever happens, the promise was not broken (T).

The last case is called vacuous truth. A conditional with a false hypothesis is true.

The biconditional p ↔ q. True when p and q have the same truth value. It means (p → q) ∧ (q → p), and is read "p if and only if q" (often written "iff").

p	q	p → q	p ↔ q
T	T	T	T
T	F	F	F
F	T	T	F
F	F	T	T

English forms of p → q. All of the following mean the same thing:

Phrase	Note
if p, then q / p implies q	Standard form
q if p / q whenever p	Conclusion stated first
p only if q	Not the same as "q only if p". p cannot happen without q
p is sufficient for q	p alone guarantees q
q is necessary for p	Without q, no p
q unless ¬p	"q unless r" means ¬r → q

Biconditional phrases: "p if and only if q", "p is necessary and sufficient for q", "p exactly when q".

Note that → says nothing about causation. "If 2 + 2 = 4 then Paris is in France" is true, even though the two facts are unrelated.

# A policy as a conditional: "if a user is an admin, then they can delete posts"
users = [
    {"name": "ana",  "is_admin": True,  "can_delete": True},
    {"name": "ben",  "is_admin": False, "can_delete": False},
    {"name": "cleo", "is_admin": False, "can_delete": True},   # vacuously fine for the policy
]

policy_holds = all((not u["is_admin"]) or u["can_delete"] for u in users)  # p → q per user
print(policy_holds)  # True

# Stronger policy as a biconditional: "admin if and only if can delete"
iff_holds = all(u["is_admin"] == u["can_delete"] for u in users)
print(iff_holds)     # False: cleo can delete without being admin

Key takeaways

• p → q is false only when p is true and q is false.
• A false hypothesis makes the conditional vacuously true.
• "p only if q" means p → q. "p if q" means q → p.
• p ↔ q is equivalent to (p → q) ∧ (q → p) and holds when both sides match.

Practice

1. (Beginner) Determine the truth value: "If 2 + 2 = 5, then the Moon is made of cheese." "If 2 + 2 = 4, then 3 is even."
2. (Intermediate) Write each as p → q, identifying p and q: "You can access the server only if you use the VPN." "A passing CI run is necessary for a merge." "The build fails unless all tests pass."
3. (Interview) A requirement says: "The alarm sounds only if the door is open." A test observes the door open and the alarm silent. Does this violate the requirement? Hint: decide carefully which statement is the hypothesis before checking the truth table.

Converse, Inverse, and Contrapositive

Why. Many reasoning errors come from silently replacing a conditional with a related statement that is not equivalent to it. Knowing which variations are safe tells you when such a substitution is allowed.

What. For a conditional p → q:

Name	Form	Equivalent to p → q?
Original	p → q	—
Converse	q → p	No
Inverse	¬p → ¬q	No
Contrapositive	¬q → ¬p	Yes

The converse and the inverse are equivalent to each other, because the inverse is the contrapositive of the converse.

   original:     p → q    <== equivalent ==>    ¬q → ¬p   :contrapositive
                   |                               |
                (swap)                          (swap)
                   |                               |
   converse:     q → p    <== equivalent ==>    ¬p → ¬q   :inverse

Example: "If it is raining, the ground is wet."

• Converse: "If the ground is wet, it is raining." (False: a sprinkler could be on.)
• Inverse: "If it is not raining, the ground is not wet." (False for the same reason.)
• Contrapositive: "If the ground is not wet, it is not raining." (True whenever the original is.)

from itertools import product

implies = lambda a, b: (not a) or b
rows = list(product([True, False], repeat=2))

original       = [implies(p, q)         for p, q in rows]
converse       = [implies(q, p)         for p, q in rows]
inverse        = [implies(not p, not q) for p, q in rows]
contrapositive = [implies(not q, not p) for p, q in rows]

print(original == contrapositive)  # True
print(converse == inverse)         # True
print(original == converse)        # False: differs on the row p=F, q=T

Key takeaways

• The contrapositive ¬q → ¬p is logically equivalent to p → q.
• The converse q → p and the inverse ¬p → ¬q are not equivalent to the original, but they are equivalent to each other.
• Assuming the converse of a true statement is one of the most common logical errors.
• Proof by contrapositive (1.4) relies directly on this equivalence.

Practice

1. (Beginner) Write the converse, inverse, and contrapositive of "If n is divisible by 6, then n is divisible by 3." Which of the four are true for all integers n?
2. (Intermediate) Give an example of a true conditional whose converse is also true. What does that tell you about the biconditional?
3. (Interview) A code reviewer reads: "Every valid session token matches the regex ^[a-f0-9]{64}$, so the check if regex.match(token): grant_access() is correct." Identify the logical flaw. Hint: write the known fact as p → q and compare it with the conditional the code actually implements.

Tautologies and Contradictions

Why. Some formulas are true or false purely because of their logical form, whatever their variables mean. These formulas are the "laws" of logic, and they are the basis of valid reasoning.

What.

Kind	Definition	Example
Tautology	True under every assignment	p ∨ ¬p
Contradiction	False under every assignment	p ∧ ¬p
Contingency	True under some assignments, false under others	p → q

Two dual facts connect them:

• F is a tautology if and only if ¬F is a contradiction.
• F is a contradiction if and only if it is unsatisfiable, meaning no assignment makes it true.

Example: ((p → q) ∧ p) → q is a tautology. It is the formal content of modus ponens (1.3).

p	q	p → q	(p → q) ∧ p	((p → q) ∧ p) → q
T	T	T	T	T
T	F	F	F	T
F	T	T	F	T
F	F	T	F	T

In code. A condition that is a tautology makes its else branch dead code. A condition that is a contradiction makes its if branch dead code. Linters warn about these ("condition is always true").

from itertools import product

def classify(n_vars, formula):
    results = {formula(*vals) for vals in product([True, False], repeat=n_vars)}
    if results == {True}:
        return "tautology"
    if results == {False}:
        return "contradiction"
    return "contingency"

implies = lambda a, b: (not a) or b
print(classify(2, lambda p, q: implies(implies(p, q) and p, q)))  # tautology
print(classify(1, lambda p: p and not p))                          # contradiction
print(classify(2, lambda p, q: implies(p, q)))                     # contingency

Key takeaways

• A tautology is always true, a contradiction is always false, and a contingency is neither.
• The negation of a tautology is a contradiction, and vice versa.
• Valid inference rules correspond to tautologies of the form (premises) → conclusion.
• In code, tautological or contradictory conditions signal dead branches or bugs.

Practice

1. (Beginner) Classify: p → ¬p, (p ∧ q) ∧ ¬(p ∨ q), (p → q) ∨ (q → p).
2. (Intermediate) Show that (p → q) ∧ (q → r) → (p → r) is a tautology using a truth table with 8 rows.
3. (Interview) You have a fast function is_satisfiable(formula). How would you use it to test whether a formula is a tautology? Hint: a formula is a tautology if no assignment makes it false.

Logical Equivalence

Why. We often want to replace a formula with a simpler or more convenient one without changing its meaning. In code, that is a safe refactoring of a condition. Logical equivalence is the guarantee that such a replacement is safe.

What. Formulas A and B are logically equivalent, written A ≡ B, if they have the same truth value under every assignment. Equivalently, A ↔ B is a tautology.

Note the difference: ↔ is a connective inside a formula, while ≡ is a claim about two formulas.

Example: p → q ≡ ¬p ∨ q

p	q	p → q	¬p	¬p ∨ q
T	T	T	F	T
T	F	F	F	F
F	T	T	T	T
F	F	T	T	T

The two final columns are identical, so the formulas are equivalent.

There are two ways to prove an equivalence:

1. Truth table: compare final columns (mechanical, exponential).
2. Algebraic rewriting: apply known laws step by step (see the next topic).

from itertools import product

def equivalent(n_vars, f, g):
    """True iff f and g agree on every assignment."""
    return all(f(*v) == g(*v) for v in product([True, False], repeat=n_vars))

print(equivalent(2, lambda p, q: not (p and q), lambda p, q: (not p) or (not q)))  # True  (De Morgan)
print(equivalent(2, lambda p, q: not (p and q), lambda p, q: (not p) and (not q))) # False (common mistake)

// Refactoring a guard with De Morgan: ¬(a ∧ b) ≡ ¬a ∨ ¬b
// Before
if (!(user.isActive && user.hasPaid)) { blockAccess(); }
// After: same behavior, reads as "inactive or unpaid"
if (!user.isActive || !user.hasPaid) { blockAccess(); }

Key takeaways

• A ≡ B means A and B agree on all assignments, i.e. A ↔ B is a tautology.
• ≡ is a statement about formulas, and ↔ is a connective inside a formula.
• Equivalence can be shown by truth tables or by chains of known laws.
• Equivalent conditions can be swapped in code without changing behavior.

Practice

1. (Beginner) Verify with a truth table that ¬(p ∨ q) ≡ ¬p ∧ ¬q.
2. (Intermediate) Decide whether each pair is equivalent: p → (q → r) vs (p ∧ q) → r; (p → q) → r vs p → (q → r). Give a distinguishing assignment where they differ.
3. (Interview) Two engineers wrote different feature-flag conditions over 40 boolean settings. How would you determine whether the conditions are equivalent without enumerating 2⁴⁰ cases by hand? Hint: build a single formula that is satisfiable exactly when the two conditions disagree.

Laws of Propositional Logic

Why. Truth tables do not scale. A small set of proven equivalences lets us transform formulas algebraically, the same way we simplify 2x + 3x to 5x.

What. The standard laws (each can be verified by truth table):

Law	Form(s)
Identity	p ∧ T ≡ p, p ∨ F ≡ p
Domination	p ∨ T ≡ T, p ∧ F ≡ F
Idempotent	p ∨ p ≡ p, p ∧ p ≡ p
Double negation	¬(¬p) ≡ p
Commutative	p ∨ q ≡ q ∨ p, p ∧ q ≡ q ∧ p
Associative	(p ∨ q) ∨ r ≡ p ∨ (q ∨ r), same for ∧
Distributive	p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r), p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
De Morgan	¬(p ∧ q) ≡ ¬p ∨ ¬q, ¬(p ∨ q) ≡ ¬p ∧ ¬q
Absorption	p ∨ (p ∧ q) ≡ p, p ∧ (p ∨ q) ≡ p
Negation (complement)	p ∨ ¬p ≡ T, p ∧ ¬p ≡ F
Conditional	p → q ≡ ¬p ∨ q
Contrapositive	p → q ≡ ¬q → ¬p
Biconditional	p ↔ q ≡ (p → q) ∧ (q → p)
Exportation	(p ∧ q) → r ≡ p → (q → r)

Duality. Swapping ∧/∨ and T/F in any law gives another law. This is why most laws come in pairs.

Worked simplification: ¬(p ∨ (¬p ∧ q))

¬(p ∨ (¬p ∧ q))
≡ ¬p ∧ ¬(¬p ∧ q)          De Morgan
≡ ¬p ∧ (¬¬p ∨ ¬q)         De Morgan
≡ ¬p ∧ (p ∨ ¬q)           Double negation
≡ (¬p ∧ p) ∨ (¬p ∧ ¬q)    Distributive
≡ F ∨ (¬p ∧ ¬q)           Negation
≡ ¬p ∧ ¬q                 Identity

Proving a tautology algebraically: (p ∧ q) → (p ∨ q)

(p ∧ q) → (p ∨ q)
≡ ¬(p ∧ q) ∨ (p ∨ q)      Conditional
≡ (¬p ∨ ¬q) ∨ (p ∨ q)     De Morgan
≡ (¬p ∨ p) ∨ (¬q ∨ q)     Associative + commutative
≡ T ∨ T                   Negation
≡ T                       Domination

Computer algebra systems apply these laws automatically:

from sympy import symbols
from sympy.logic.boolalg import simplify_logic

p, q = symbols("p q")
print(simplify_logic(~(p | (~p & q))))   # ~p & ~q   (matches the manual derivation)
print(simplify_logic((p & q) >> (p | q)))  # True      (">>" is implication in SymPy)

Key takeaways

• About a dozen laws suffice for most algebraic manipulation of formulas.
• De Morgan, distributive, and conditional laws are the most frequently used.
• Laws come in dual pairs (swap ∧/∨ and T/F).
• Justify each rewriting step by naming the law used.

Practice

1. (Beginner) Simplify (p ∧ q) ∨ (p ∧ ¬q) using the laws, naming each step.
2. (Intermediate) Show algebraically that ¬(p → q) ≡ p ∧ ¬q, and that (p → q) ∧ (p → r) ≡ p → (q ∧ r).
3. (Interview) Simplify this Python guard and justify each step: if not (user is None or not user.active): ... Hint: apply De Morgan, then double negation.

Normal Forms (CNF and DNF)

Why. Many algorithms, including SAT solvers, circuit synthesizers and theorem provers, need formulas in a predictable, uniform shape. Normal forms supply that shape, and every formula can be converted into them.

Vocabulary.

• A literal is a variable or its negation: p, ¬q.
• A clause is a disjunction of literals: (p ∨ ¬q ∨ r).
• A term is a conjunction of literals: (p ∧ ¬q ∧ r).

Form	Shape	Example	Easy to check
DNF (disjunctive normal form)	OR of ANDs	(p ∧ ¬q) ∨ (¬p ∧ q)	Satisfiability: one consistent term suffices
CNF (conjunctive normal form)	AND of ORs	(p ∨ q) ∧ (¬p ∨ ¬q)	Validity: every clause must contain some x and ¬x

From a truth table.

• DNF: for each row where the formula is T, write a term that matches that row exactly (a minterm), then OR them together.
• CNF: for each row where the formula is F, write a clause that rules out that row (a maxterm), then AND them together.

Example for p ⊕ q (true on rows TF and FT, false on TT and FF):

DNF: (p ∧ ¬q) ∨ (¬p ∧ q)        one term per TRUE row
CNF: (¬p ∨ ¬q) ∧ (p ∨ q)        clause (¬p ∨ ¬q) rules out TT; (p ∨ q) rules out FF

Algebraic conversion.

1. Eliminate ↔ and → using the biconditional and conditional laws.
2. Push negations inward with De Morgan and double negation, until ¬ applies only to variables (negation normal form).
3. Distribute: ∨ over ∧ for CNF, or ∧ over ∨ for DNF.

Example: ¬(p → q) ∨ r

¬(p → q) ∨ r
≡ ¬(¬p ∨ q) ∨ r            Conditional
≡ (p ∧ ¬q) ∨ r             De Morgan + double negation   <- already DNF
≡ (p ∨ r) ∧ (¬q ∨ r)       Distribute ∨ over ∧           <- CNF

Size warning. Distribution can blow up exponentially. For example, (a₁ ∧ b₁) ∨ ... ∨ (aₙ ∧ bₙ) has 2ⁿ clauses in CNF. The Tseitin transformation avoids this by introducing helper variables. It produces a CNF of linear size that is equisatisfiable (satisfiable exactly when the original is), though not equivalent.

from itertools import product

def to_dnf(variables, formula):
    """Build a DNF string from the truth table: one minterm per true row."""
    terms = []
    for values in product([True, False], repeat=len(variables)):
        if formula(*values):                                     # keep only rows where it is true
            literals = [v if val else "¬" + v for v, val in zip(variables, values)]
            terms.append("(" + " ∧ ".join(literals) + ")")
    return " ∨ ".join(terms) if terms else "F"                   # no true rows: contradiction

def to_cnf(variables, formula):
    """Build a CNF string from the truth table: one clause per false row."""
    clauses = []
    for values in product([True, False], repeat=len(variables)):
        if not formula(*values):
            literals = ["¬" + v if val else v for v, val in zip(variables, values)]  # flip each literal
            clauses.append("(" + " ∨ ".join(literals) + ")")
    return " ∧ ".join(clauses) if clauses else "T"

print(to_dnf(["p", "q"], lambda p, q: p != q))  # (p ∧ ¬q) ∨ (¬p ∧ q)
print(to_cnf(["p", "q"], lambda p, q: p != q))  # (¬p ∨ ¬q) ∧ (p ∨ q)

Key takeaways

• DNF is an OR of ANDs and CNF is an AND of ORs. Every formula has both forms.
• DNF comes from the true rows of the truth table, and CNF from the false rows.
• To convert algebraically, eliminate →/↔, push ¬ inward, then distribute.
• Naive conversion can be exponential. Tseitin gives a linear-size equisatisfiable CNF.

Practice

1. (Beginner) Convert p ↔ q to both DNF and CNF.
2. (Intermediate) Convert (p ∨ q) → r to CNF algebraically, naming each law used.
3. (Interview) SAT solvers take CNF input. Satisfiability of a DNF formula can be checked in linear time. Why does "convert to DNF, then check" not solve SAT efficiently? Hint: think about the size of the DNF relative to the original CNF.

Satisfiability

Why. Many practical problems reduce to one question: "Is there an assignment that makes all these constraints true?" Scheduling, package dependency resolution, hardware verification, test generation and Sudoku can all be phrased this way.

What. A formula is satisfiable if at least one assignment makes it true. That assignment is a model or witness. Otherwise the formula is unsatisfiable. SAT ties together several earlier ideas:

• F is a tautology if and only if ¬F is unsatisfiable.
• F ≡ G if and only if F ⊕ G is unsatisfiable.
• An argument is valid if and only if premises ∧ ¬conclusion is unsatisfiable.

Complexity. SAT was the first problem proven NP-complete (Cook–Levin theorem, 1971). No known algorithm solves every instance in polynomial time.

Variant	Clause restriction	Complexity
2-SAT	At most 2 literals per clause	Polynomial (implication graph + SCCs)
Horn-SAT	At most 1 positive literal per clause	Polynomial (unit propagation)
3-SAT	At most 3 literals per clause	NP-complete
General CNF-SAT	Any clauses	NP-complete

Modern CDCL solvers handle instances with millions of variables in practice. They build on the DPLL algorithm:

• Unit propagation: a clause with a single unassigned literal forces that literal.
• Branching: pick a variable, try T, and backtrack to F on conflict.

def dpll(clauses, assignment=None):
    """Clauses are lists of non-zero ints (DIMACS style): k means x_k, -k means ¬x_k.
    Returns a satisfying assignment {var: bool} or None if unsatisfiable."""
    if assignment is None:
        assignment = {}
    simplified = []
    for clause in clauses:
        if any(assignment.get(abs(l)) == (l > 0) for l in clause):
            continue                                   # clause already satisfied
        remaining = [l for l in clause if abs(l) not in assignment]
        if not remaining:
            return None                                # every literal false: conflict
        simplified.append(remaining)
    if not simplified:
        return assignment                              # all clauses satisfied
    for clause in simplified:                          # unit propagation
        if len(clause) == 1:
            lit = clause[0]
            return dpll(simplified, {**assignment, abs(lit): lit > 0})
    var = abs(simplified[0][0])                        # branch on an unassigned variable
    for value in (True, False):
        result = dpll(simplified, {**assignment, var: value})
        if result is not None:
            return result
    return None                                        # both branches failed

# (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3) ∧ ¬x3
print(dpll([[1, 2], [-1, 3], [-2, -3], [-3]]))  # {3: False, 1: False, 2: True}
print(dpll([[1], [-1]]))                         # None (x1 ∧ ¬x1)

Encoding constraints. "Exactly one of a, b, c" in CNF is "at least one" plus "no two":

(a ∨ b ∨ c) ∧ (¬a ∨ ¬b) ∧ (¬a ∨ ¬c) ∧ (¬b ∨ ¬c)

Key takeaways

• Satisfiable means at least one assignment makes the formula true.
• Validity, equivalence, and argument checking all reduce to (un)satisfiability.
• SAT is NP-complete in general, but 2-SAT and Horn-SAT are polynomial.
• DPLL/CDCL solvers use unit propagation and backtracking, and are very effective in practice.

Practice

1. (Beginner) Is (p ∨ q) ∧ (¬p ∨ q) ∧ (p ∨ ¬q) ∧ (¬p ∨ ¬q) satisfiable? Justify without a full truth table.
2. (Intermediate) Encode "at most one of a, b, c, d is true" in CNF. How many clauses does the pairwise encoding need for n variables?
3. (Interview) A package manager must install app, which needs lib >= 2 or compat. lib 2 conflicts with ssl 1, and compat requires ssl 1. Model this as a SAT instance. Hint: one boolean variable per (package, version), with clauses for "requires", "conflicts", and "only one version per package".

<a id="12-predicate-logic"></a>

1.2 Predicate Logic

Propositional logic cannot look inside a statement. Predicate logic adds variables, predicates, and quantifiers, so that we can make claims about "all" or "some" objects in a collection.

Predicates and Domains

Why. Consider: "All humans are mortal. Socrates is human. Therefore Socrates is mortal." In propositional logic these are three unrelated propositions p, q, r, and nothing connects them. The argument is valid because of the internal structure (human, mortal, Socrates), so we need a logic that can express that structure.

What.

• A predicate P(x) is a statement containing variables. It becomes a proposition once every variable is given a value. P(x) is called the propositional function evaluated at x.
• The domain (universe of discourse) is the set of values the variables may take.
• Predicates can take several arguments: L(x, y): "x < y" is a 2-place predicate.
• The truth set of P is {x ∈ D | P(x) is true}.

Analogy. A predicate is a function that returns a boolean. The domain is its parameter type.

The domain matters. The same predicate can behave differently over different domains:

Predicate	Domain	Is it true for every x?
x² ≥ x	Integers ℤ	Yes
x² ≥ x	Reals ℝ	No (x = 0.5)
x² = 2 has a solution	Rationals ℚ	No
x² = 2 has a solution	Reals ℝ	Yes (x = √2)

def P(x):                  # P(x): "x squared is at least x"
    return x * x >= x

print(P(3), P(-2), P(0))   # True True True  -- each call yields a proposition
print(P(0.5))              # False: 0.25 >= 0.5 fails, so the claim fails over the reals

def L(x, y):               # 2-place predicate L(x, y): "x < y"
    return x < y

truth_set = {x for x in range(-10, 11) if x * x == 4}
print(truth_set)           # {-2, 2}: truth set of "x² = 4" over the integers -10..10

Key takeaways

• A predicate is a statement with variables. Assigning the variables yields a proposition.
• The domain must always be specified, because truth can change with it.
• Predicates can have any number of arguments.
• The truth set collects the domain elements that satisfy the predicate.

Practice

1. (Beginner) Let P(x): "x² > 10" over the integers. Find the truth values of P(3), P(-4), P(0).
2. (Intermediate) Give the truth set of Q(x): "x² = x" over ℕ, ℤ, and ℝ. Then find a predicate whose truth set is empty over ℝ but non-empty over ℂ.
3. (Interview) In SQL, SELECT * FROM users WHERE age >= 18 AND country = 'IT' returns a truth set. Identify the predicate, its domain, and its arguments. How does NULL complicate the "two truth values" assumption? Hint: SQL uses three-valued logic. Look up what NULL = NULL evaluates to.

Universal and Existential Quantifiers

Why. Predicates let us talk about individual objects. Quantifiers let us talk about collections of objects: "every user has an email" or "some request timed out".

What.

Statement	Read as	True when	False when
∀x P(x)	for all x, P(x)	P(x) holds for every x in the domain	some x fails: a counterexample
∃x P(x)	there exists x such that P(x)	P(x) holds for at least one x: a witness	P(x) fails for every x
∃!x P(x)	there exists a unique x	exactly one x satisfies P	zero or at least two do

Finite domains. If D = {a₁, …, aₙ}, then

∀x P(x)  ≡  P(a₁) ∧ P(a₂) ∧ … ∧ P(aₙ)      (a big AND)
∃x P(x)  ≡  P(a₁) ∨ P(a₂) ∨ … ∨ P(aₙ)      (a big OR)

Empty domain. ∀x P(x) is vacuously true, because there is nothing to fail. ∃x P(x) is false, because there is nothing to witness it. This matches the identities of ∧ (empty AND = T) and ∨ (empty OR = F).

Restricted quantifiers. "For all positive x" and "for some positive x" translate differently:

∀x > 0, P(x)   ≡   ∀x (x > 0 → P(x))     universal pairs with →
∃x > 0, P(x)   ≡   ∃x (x > 0 ∧ P(x))     existential pairs with ∧

Mixing these up is a classic error. ∃x (Student(x) → Smart(x)) is true as soon as any non-student exists, so it does not say what was intended.

Precedence. Quantifiers bind more tightly than all connectives. ∀x P(x) ∨ Q(x) means (∀x P(x)) ∨ Q(x).

D = [1, 2, 3, 4]

print(all(x < 5 for x in D))               # ∀x (x < 5)                  -> True
print(any(x % 3 == 0 for x in D))          # ∃x (3 divides x)            -> True (witness: 3)
print(sum(1 for x in D if x % 2 == 0) == 1)  # ∃!x (x is even)          -> False (2 and 4)

print(all(x > 10 for x in []))             # ∀ over empty domain -> True (vacuous)
print(any(x > 10 for x in []))             # ∃ over empty domain -> False

# Restricted quantifier: "every even element is greater than 1"
print(all((x % 2 != 0) or (x > 1) for x in D))  # ∀x (Even(x) → x > 1) -> True

Key takeaways

• ∀ asserts something about every element, and one counterexample refutes it.
• ∃ asserts at least one element, and one witness proves it.
• Over finite domains, ∀ is a big AND and ∃ is a big OR. Python's all/any match them exactly, including on empty input.
• Pair ∀ with → and ∃ with ∧ when restricting the domain.

Practice

1. (Beginner) Over the domain {1, 2, 3, 4}, find the truth values of ∀x (x² ≤ 16), ∃x (x² = 9), and ∀x (x is prime).
2. (Intermediate) Explain why ∃x (Student(x) → Smart(x)) is a wrong translation of "Some student is smart", and give a domain where it is true but the English sentence is false.
3. (Interview) Why does all([]) return True in Python, and why is that the right design choice? Hint: think of all as a fold over and, starting from an identity element.

Nested Quantifiers

Why. Interesting statements usually involve several quantified variables: "every element has a larger element", or "for every ε there is a δ". The order of the quantifiers changes the meaning in ways that are easy to miss.

What. Quantifiers are read left to right, and each one is in the scope of those before it. A useful way to evaluate them is as a game:

• For ∀, an adversary picks the value and tries to make the statement fail.
• For ∃, you pick the value and try to make it hold.
• A later choice may depend on the earlier ones.

∀x ∃y (x + y = 0)   over ℤ:   adversary picks x, then you pick y = -x       -> TRUE
∃y ∀x (x + y = 0)   over ℤ:   you must pick one y before seeing x           -> FALSE

Analogy. "Everyone has a mother" (∀x ∃y Mother(y, x)) is very different from "There is someone who is everyone's mother" (∃y ∀x Mother(y, x)).

Quantifiers of the same type can be swapped freely: ∀x ∀y ≡ ∀y ∀x and ∃x ∃y ≡ ∃y ∃x. Quantifiers of different types generally cannot.

All two-variable combinations for L(x, y): "x likes y":

Formula	Meaning
∀x ∀y L(x, y)	Everyone likes everyone
∀x ∃y L(x, y)	Everyone likes someone (possibly different people)
∃y ∀x L(x, y)	There is one person whom everyone likes
∃x ∀y L(x, y)	Someone likes everyone
∀y ∃x L(x, y)	Everyone is liked by someone
∃x ∃y L(x, y)	Someone likes someone

One direction of swapping is always valid: ∃y ∀x P(x, y) → ∀x ∃y P(x, y). If one y works for every x, then each x has a y. The converse is false in general.

In code. Nested quantifiers are nested loops. ∀x ∃y becomes an all wrapping an any. Evaluating k nested quantifiers over a domain of size n costs O(nᵏ).

D = range(-5, 6)

# ∀x ∃y (x + y = 0): y may depend on x
print(all(any(x + y == 0 for y in D) for x in D))   # True

# ∃y ∀x (x + y = 0): a single y must work for all x
print(any(all(x + y == 0 for x in D) for y in D))   # False

# "A has no duplicates": ∀i ∀j (i ≠ j → A[i] ≠ A[j])
A = [3, 1, 4, 1, 5]
no_dups = all(i == j or A[i] != A[j] for i in range(len(A)) for j in range(len(A)))
print(no_dups)                                      # False: A[1] == A[3]

Key takeaways

• Quantifiers are read left to right, and later variables may depend on earlier ones.
• Swapping quantifiers of the same type is safe. Swapping ∀ and ∃ generally is not.
• ∃y ∀x implies ∀x ∃y, but not the reverse.
• In code, nested quantifiers become nested all/any loops.

Practice

1. (Beginner) Over ℤ, find the truth values of ∀x ∃y (y > x) and ∃y ∀x (y > x).
2. (Intermediate) Find the truth value of ∀x ∀y ∃z (z = (x + y) / 2) over ℤ and over ℝ. Explain the difference.
3. (Interview) Express "array A is sorted in non-decreasing order" with quantifiers in two ways: one with two index variables and one comparing only adjacent elements. Which gives the faster check, and why are they equivalent? Hint: the adjacent version needs transitivity of ≤.

Negating Quantified Statements

Why. To disprove a claim, or to write the failure condition of a check, you need its exact negation. Negating quantified statements by intuition goes wrong surprisingly often.

What. De Morgan's laws for quantifiers:

¬∀x P(x)  ≡  ∃x ¬P(x)       "not everything satisfies P" = "something fails P"
¬∃x P(x)  ≡  ∀x ¬P(x)       "nothing satisfies P"        = "everything fails P"

Over a finite domain, these are the ordinary De Morgan laws applied to the big AND and big OR.

Nested quantifiers: push ¬ inward one quantifier at a time, flipping each ∀ ↔ ∃, and negate the predicate at the end.

¬∀x ∃y (x + y = 0)
≡ ∃x ¬∃y (x + y = 0)
≡ ∃x ∀y (x + y ≠ 0)

Negating a restricted universal gives the shape of every counterexample:

¬∀x (P(x) → Q(x))  ≡  ∃x ¬(P(x) → Q(x))  ≡  ∃x (P(x) ∧ ¬Q(x))

A counterexample is an element that satisfies the hypothesis but violates the conclusion.

English claim	Correct negation	Common wrong negation
All birds can fly	Some bird cannot fly	No bird can fly
Some test failed	No test failed (all passed)	Some test passed
f is bounded: ∃M ∀x (|f(x)| ≤ M)	∀M ∃x (|f(x)| > M)	∃M ∀x (|f(x)| > M)

data = [3, 8, 1, 9]

# ¬∀x P(x) ≡ ∃x ¬P(x)
assert (not all(x > 2 for x in data)) == any(not (x > 2) for x in data)

# The useful part of the negation is the witness: the element that breaks the claim
witness = next((x for x in data if not x > 2), None)
print(witness)  # 1

Key takeaways

• ¬∀ ≡ ∃¬ and ¬∃ ≡ ∀¬.
• For nested quantifiers, flip every quantifier while pushing the negation inward.
• ¬∀x (P → Q) ≡ ∃x (P ∧ ¬Q): a counterexample satisfies the hypothesis and violates the conclusion.
• "Not all" is not the same as "none".

Practice

1. (Beginner) Negate and simplify so that no ¬ stands in front of a quantifier: ∀x (x² ≥ 0), ∃x (x² = -1).
2. (Intermediate) Negate the definition of continuity at 0: ∀ε > 0 ∃δ > 0 ∀x (|x| < δ → |f(x)| < ε). Remember the restricted quantifiers.
3. (Interview) A test asserts all(is_valid(r) for r in records) and fails. What does the negation tell you the failure message should contain to be useful? Hint: the negation is an existential statement. What object does it promise exists?

Bound and Free Variables

Why. In ∀x P(x, y), the x and the y play different roles. Telling them apart is necessary to know whether a formula is a proposition, and to substitute values without changing the meaning. Programming has the same issue with variable scope.

What.

• A variable occurrence is bound if it falls within the scope of a quantifier on that variable.
• Otherwise it is free.
• The scope of a quantifier is the subformula it applies to.
• A formula with no free variables is a closed formula (a sentence), and it is a proposition.
• A formula with free variables is a predicate on those variables.

The same name can be free in one place and bound in another:

∀x ( P(x, y) ∧ ∃y Q(x, y) ) ∨ R(x)
   └──── scope of ∀x ─────┘
               └── ∃y ──┘

x in P(x, y) and Q(x, y): bound by ∀x
x in R(x):                FREE (outside the scope of ∀x)
y in P(x, y):             FREE (not inside ∃y)
y in Q(x, y):             bound by ∃y

Renaming (α-equivalence). A bound variable can be renamed consistently without changing the meaning: ∀x P(x) ≡ ∀z P(z). Rename bound variables to avoid clashes like the one above:

∀w ( P(w, y) ∧ ∃v Q(w, v) ) ∨ R(x)       same meaning; now each name plays one role

Free variables (y and the last x) must not be renamed. They are the formula's parameters, and renaming them changes what the formula says.

Analogy. Bound variables are like function parameters and local variables, whose names do not matter outside the function. Free variables are like globals or closure captures, whose values come from the surrounding context.

y = 10                            # outer context supplies the free variable y

def f(x):                         # x is bound (a parameter): renaming it changes nothing
    return x + y                  # y is free in the body: its value comes from outside

g = lambda x: (lambda y: x + y)   # inner y is bound by the inner lambda; x is free in it
print(f(1), g(1)(2))              # 11 3

Key takeaways

• Bound variables are inside the scope of a matching quantifier. Free variables are not.
• A formula is a proposition only if it has no free variables.
• Bound variables can be renamed consistently without changing the meaning.
• Rename bound variables before substituting, to avoid accidentally capturing a free variable.

Practice

1. (Beginner) Identify every free and bound occurrence in ∃x (P(x) ∧ ∀y Q(x, y, z)).
2. (Intermediate) Rewrite ∀x (P(x) → ∃x Q(x)) so that no variable name is quantified twice. Is the result equivalent?
3. (Interview) Substituting y := x into ∃x (x > y) naively gives ∃x (x > x), which is false, although the original is true for every y over ℤ. Explain what went wrong and how compilers and theorem provers avoid it. Hint: search for "capture-avoiding substitution".

Translating English to Logic

Why. Specifications, requirements, and theorems start in natural language. Translating them precisely exposes ambiguity and makes them checkable, by a proof or by code.

How.

1. Fix the domain. A broad domain plus restricting predicates is often simplest.
2. Define predicates with explicit meaning, such as S(x): "x is a student".
3. Identify the quantifiers ("every", "some", "no", "only") and their order.
4. Apply the standard patterns, then reread the result as English to check it.

English	Logic
All A are B	∀x (A(x) → B(x))
Some A are B	∃x (A(x) ∧ B(x))
No A are B	∀x (A(x) → ¬B(x)) ≡ ¬∃x (A(x) ∧ B(x))
Not all A are B	∃x (A(x) ∧ ¬B(x))
Only A are B	∀x (B(x) → A(x))
Every A has some B-related y	∀x (A(x) → ∃y R(x, y))

Worked example: "Every student in the class has a friend in the class who has taken a programming course."

Domain: all people
C(x): x is in the class      F(x, y): x and y are friends      P(y): y took a programming course

∀x ( C(x) → ∃y ( C(y) ∧ F(x, y) ∧ P(y) ) )

Ambiguity check. "Everybody loves somebody" could mean ∀x ∃y L(x, y) or ∃y ∀x L(x, y). Choose deliberately, and state your reading.

The same discipline applies to data constraints. A foreign key is a nested quantified statement, and the query that finds violations is its negation:

# ∀o ∈ Orders ∃c ∈ Customers (o.customer_id = c.id)
customers = [{"id": 1}, {"id": 2}]
orders = [{"id": 10, "customer_id": 1}, {"id": 11, "customer_id": 7}]

customer_ids = {c["id"] for c in customers}
print(all(o["customer_id"] in customer_ids for o in orders))  # False

-- Negation: ∃o ∈ Orders ∀c ∈ Customers (o.customer_id ≠ c.id)
SELECT o.*
FROM orders o
WHERE NOT EXISTS (SELECT 1 FROM customers c WHERE c.id = o.customer_id);  -- returns order 11

Key takeaways

• Fix the domain and define predicates explicitly before translating.
• "All" pairs with →, "some" pairs with ∧, and "only A are B" reverses the direction of the implication.
• Ambiguous English often hides a quantifier-order choice. Resolve it explicitly.
• Integrity constraints are quantified formulas, and their violations are the negations.

Practice

1. (Beginner) Translate, with domain "all animals": "Every dog is a mammal." "Some mammals are not dogs." "No cat is a dog."
2. (Intermediate) Translate: "Only admins can delete posts." "Every user has exactly one primary email address." (Use ∃! or expand it into ∃ and ∀.)
3. (Interview) Translate "there is a server that can reach every database" and "every database is reachable from some server". Which one implies the other? Write a query or function that checks the stronger one. Hint: look at the quantifier order in each statement.

<a id="13-rules-of-inference"></a>

1.3 Rules of Inference

Rules of inference are small reasoning steps that have each been verified once and for all. Every valid argument, however long, can be built by chaining them.

Valid Arguments

Why. A truth table can check whether a single formula is a tautology. A mathematical argument, though, is a sequence of statements leading to a conclusion. We need a precise criterion for when the conclusion really follows from the premises.

What. An argument is a list of premises p₁, …, pₙ and a conclusion c, written p₁, …, pₙ ⊢ c or as:

p₁
p₂
…
pₙ
───
∴ c

The argument is valid if, whenever all premises are true, the conclusion is also true. Equivalently:

(p₁ ∧ p₂ ∧ … ∧ pₙ) → c    is a tautology

To refute validity, find a critical row: an assignment that makes every premise true and the conclusion false.

Validity vs soundness. Validity concerns form only. An argument is sound if it is valid and all its premises are actually true. Only a sound argument guarantees a true conclusion.

Argument	Valid?	Sound?
All cats can fly. Tom is a cat. ∴ Tom can fly.	Yes	No (false premise)
If n is even, n² is even. 4 is even. ∴ 16 is even.	Yes	Yes
If it rains, the street is wet. The street is wet. ∴ It rained.	No	No

A valid argument can have a false conclusion (when a premise is false). An invalid argument can have a true conclusion by luck.

from itertools import product

def is_valid(n_vars, premises, conclusion):
    """Return (True, None) if valid, else (False, critical_row)."""
    for values in product([True, False], repeat=n_vars):
        if all(p(*values) for p in premises) and not conclusion(*values):
            return False, values                 # premises all true, conclusion false
    return True, None

imp = lambda a, b: (not a) or b

# p → q, q → r  ⊢  p → r      (hypothetical syllogism)
print(is_valid(3, [lambda p, q, r: imp(p, q), lambda p, q, r: imp(q, r)],
                  lambda p, q, r: imp(p, r)))    # (True, None)

# p → q, q  ⊢  p              (affirming the consequent)
print(is_valid(2, [lambda p, q: imp(p, q), lambda p, q: q],
                  lambda p, q: p))               # (False, (False, True))

Key takeaways

• An argument is valid when the premises cannot all be true while the conclusion is false.
• Validity is equivalent to (premises) → conclusion being a tautology, or to premises ∧ ¬conclusion being unsatisfiable.
• A critical row (all premises T, conclusion F) proves invalidity.
• Sound means valid with true premises. Only soundness guarantees a true conclusion.

Practice

1. (Beginner) Use a truth table to decide whether p ∨ q, ¬p ⊢ q is valid.
2. (Intermediate) Decide validity and give a critical row if invalid: p → q, ¬p ⊢ ¬q; p → (q ∨ r), ¬q, ¬r ⊢ ¬p.
3. (Interview) "All 1,200 tests pass; if the code is correct, all tests pass; therefore the code is correct." Is this valid? Rewrite it as a valid argument, and say which premise you would then have to defend. Hint: the direction of the implication matters.

Modus Ponens and Modus Tollens

Why. Checking validity with truth tables is exponential. Instead, we build arguments from a small set of rules that are each known to be valid. Modus ponens and modus tollens are the two most important.

What.

Rule	Premises	Conclusion	Underlying tautology
Modus ponens (MP)	p → q, p	q	((p → q) ∧ p) → q
Modus tollens (MT)	p → q, ¬q	¬p	((p → q) ∧ ¬q) → ¬p
Conjunction	p, q	p ∧ q	(p ∧ q) → (p ∧ q)
Simplification	p ∧ q	p	(p ∧ q) → p
Addition	p	p ∨ q	p → (p ∨ q)

• Modus ponens ("mode that affirms"): the rule is known and its condition holds, so the result holds. This is forward reasoning.
• Modus tollens ("mode that denies"): the rule is known and its result is missing, so the condition did not hold. This is backward reasoning, and it is the logic of debugging.

Formal derivation. Each line is a premise or follows from earlier lines by a named rule.

Premises: p → q,  q → r,  ¬r.        Goal: ¬p

1. p → q        premise
2. q → r        premise
3. ¬r           premise
4. ¬q           MT 2, 3
5. ¬p           MT 1, 4

MT in debugging. "If the config loaded, the log contains ready. The log does not contain ready. Therefore the config did not load." This is valid. The opposite inference, seeing ready and concluding that the config loaded, is a fallacy (affirming the consequent) unless the converse rule is independently known.

In code. Rule engines and expert systems repeatedly apply modus ponens (forward chaining):

def forward_chain(facts, rules):
    """rules: list of (set_of_premises, conclusion). Apply modus ponens until nothing changes."""
    facts = set(facts)
    changed = True
    while changed:
        changed = False
        for premises, conclusion in rules:
            if premises <= facts and conclusion not in facts:  # all premises already known
                facts.add(conclusion)                          # modus ponens step
                changed = True
    return facts

rules = [
    ({"rain"}, "wet_ground"),
    ({"wet_ground", "freezing"}, "ice"),
    ({"ice"}, "slippery"),
]
print(forward_chain({"rain", "freezing"}, rules))
# {'rain', 'freezing', 'wet_ground', 'ice', 'slippery'}   (set order may vary)

Key takeaways

• MP: from p → q and p, infer q. MT: from p → q and ¬q, infer ¬p.
• Each rule of inference corresponds to a tautology, which is what makes it valid.
• Formal derivations cite a rule and line numbers for every step.
• Forward chaining in rule engines is repeated modus ponens.

Practice

1. (Beginner) Name the rule: from "If it snows, school closes" and "School is open", infer "It is not snowing".
2. (Intermediate) Derive s from the premises p ∧ q, p → r, r → s, citing a rule for each line.
3. (Interview) "If the cache is warm, responses take under 50 ms." A response took 200 ms. What can you conclude? What can you conclude if a response took 30 ms? Hint: one case is modus tollens. The other tempts you into a fallacy covered later in this subchapter.

Syllogisms

Why. Much reasoning chains conditions ("this leads to that, which leads to something else") or eliminates alternatives ("it is either A or B, and it is not A"). Syllogisms formalize both patterns.

What.

Rule	Premises	Conclusion	Intuition
Hypothetical syllogism	p → q, q → r	p → r	Implications chain (transitivity)
Disjunctive syllogism	p ∨ q, ¬p	q	Process of elimination
Constructive dilemma	p → q, r → s, p ∨ r	q ∨ s	Each alternative leads somewhere

Categorical syllogisms. Aristotle's syllogisms relate classes of things, for example "All M are P; all S are M; therefore all S are P". They are valid because class inclusion is transitive:

+------------------------- P: mortal --------+
|   +------------------ M: human --------+   |
|   |   +------- S: Greek -------+       |   |
|   |   |       * Socrates       |       |   |
|   |   +------------------------+       |   |
|   +------------------------------------+   |
+--------------------------------------------+

Implications as a graph. If each a → b is a directed edge, hypothetical syllogism says x → y is derivable exactly when y is reachable from x. This is the core idea behind the polynomial-time 2-SAT algorithm.

from collections import defaultdict, deque

def follows(implications, start, goal):
    """Is start → goal derivable by chaining (hypothetical syllogism)? BFS reachability."""
    graph = defaultdict(list)
    for a, b in implications:
        graph[a].append(b)
    seen, queue = {start}, deque([start])
    while queue:
        node = queue.popleft()
        if node == goal:
            return True
        for nxt in graph[node]:
            if nxt not in seen:
                seen.add(nxt)
                queue.append(nxt)
    return False

imps = [("p", "q"), ("q", "r"), ("r", "s"), ("t", "q")]
print(follows(imps, "p", "s"))  # True:  p → q → r → s
print(follows(imps, "s", "p"))  # False: implications do not run backwards

Key takeaways

• Hypothetical syllogism chains implications: p → q, q → r give p → r.
• Disjunctive syllogism eliminates an alternative: p ∨ q, ¬p give q.
• Categorical syllogisms are valid exactly when they follow from transitivity of class inclusion.
• Chaining implications is reachability in a directed graph.

Practice

1. (Beginner) Derive p from p ∨ q, q → r, ¬r, naming each rule.
2. (Intermediate) Is "All A are B; some C are B; therefore some C are A" valid? If not, draw a diagram that serves as a counterexample.
3. (Interview) Given thousands of implications between feature flags (a → b means "enabling a requires b"), how would you efficiently answer many queries of the form "does enabling x force y?" Hint: precompute something on the implication graph. Consider strongly connected components and transitive closure.

Resolution

Why. Humans pick the right rule for each step by insight. A computer needs one uniform rule that it can apply mechanically. Resolution is that rule, and it is the basis of automated theorem provers, Prolog, and SAT solvers' clause learning.

What. For clauses (disjunctions of literals):

(p ∨ q)     (¬p ∨ r)
─────────────────────
       (q ∨ r)

p and ¬p cancel, and the remaining literals are combined into the resolvent. The rule is sound: if p is true, r must hold, and if p is false, q must hold.

Familiar rules are special cases:

Rule	As resolution
Modus ponens	{¬p, q} and {p} resolve to {q}
Modus tollens	{¬p, q} and {¬q} resolve to {¬p}
Disjunctive syllogism	{p, q} and {¬p} resolve to {q}

Refutation proofs. To show premises entail a conclusion c:

1. Convert the premises and ¬c to CNF (a set of clauses).
2. Resolve pairs repeatedly.
3. If the empty clause {} (a contradiction) appears, the premises entail c.

Resolution is refutation-complete for propositional logic: if the clause set is unsatisfiable, the empty clause will eventually be derived.

Example: from p → q, q → r, p, prove r.

Clauses: {¬p, q}  {¬q, r}  {p}  {¬r}   <- negated goal

{¬q, r}   {¬r}
      \   /
      {¬q}    {¬p, q}
          \   /
          {¬p}    {p}
              \   /
               { }      empty clause: contradiction, so r follows

from itertools import combinations

def resolve(c1, c2):
    """All resolvents of two clauses (frozensets of int literals; -k means ¬x_k)."""
    resolvents = []
    for lit in c1:
        if -lit in c2:
            new = (c1 - {lit}) | (c2 - {-lit})
            if not any(-l in new for l in new):     # discard tautologies like {x, ¬x}
                resolvents.append(frozenset(new))
    return resolvents

def entails(kb, query_clause):
    """Does kb entail query_clause? Add its negation and search for the empty clause."""
    clauses = {frozenset(c) for c in kb}
    clauses |= {frozenset([-lit]) for lit in query_clause}  # ¬(a ∨ b) = {¬a}, {¬b}
    while True:
        new = set()
        for c1, c2 in combinations(clauses, 2):
            for r in resolve(c1, c2):
                if not r:
                    return True                     # empty clause derived
                new.add(r)
        if new <= clauses:
            return False                            # saturated: no refutation exists
        clauses |= new

# p=1, q=2, r=3:  p → q, q → r, p  ⊢  r
print(entails([[-1, 2], [-2, 3], [1]], [3]))  # True
print(entails([[-1, 2], [-2, 3]], [3]))       # False (p is no longer a premise)

Key takeaways

• Resolution: from (p ∨ q) and (¬p ∨ r), infer (q ∨ r).
• It works on clauses, so the input must be in CNF.
• MP, MT, and disjunctive syllogism are special cases.
• Proof by refutation: add the negated goal and derive the empty clause. This is complete for propositional logic.

Practice

1. (Beginner) Find the resolvent of (p ∨ ¬q ∨ r) and (q ∨ s).
2. (Intermediate) Use resolution to show that (p ∨ q) ∧ (p ∨ ¬q) ∧ (¬p ∨ q) ∧ (¬p ∨ ¬q) is unsatisfiable.
3. (Interview) Why do resolution provers work by refutation (deriving {} from premises plus the negated goal) instead of deriving the goal directly? Hint: try deriving p ∨ q from the premise p using resolution alone.

Inference with Quantifiers

Why. The Socrates argument mixes a universal statement ("all humans are mortal") with a specific individual ("Socrates"). We need rules for moving between quantified statements and statements about particular elements.

What.

Rule	From	Infer	Condition
Universal instantiation (UI)	∀x P(x)	P(c)	c is any element of the domain
Universal generalization (UG)	P(c)	∀x P(x)	c is arbitrary: nothing special about it was assumed
Existential instantiation (EI)	∃x P(x)	P(c)	c is a fresh name, not used earlier
Existential generalization (EG)	P(c)	∃x P(x)	c is some element of the domain

Combining UI with MP gives universal modus ponens: from ∀x (P(x) → Q(x)) and P(a), infer Q(a).

Worked derivation. Premises: "A student in this class has not read the book" and "Everyone in this class passed the first exam". Conclusion: "Someone who passed the first exam has not read the book".

C(x): x is in the class    B(x): x read the book    P(x): x passed the first exam

1. ∃x (C(x) ∧ ¬B(x))      premise
2. C(a) ∧ ¬B(a)           EI from 1 (a is a fresh name)
3. C(a)                   simplification 2
4. ∀x (C(x) → P(x))       premise
5. C(a) → P(a)            UI from 4
6. P(a)                   MP 3, 5
7. ¬B(a)                  simplification 2
8. P(a) ∧ ¬B(a)           conjunction 6, 7
9. ∃x (P(x) ∧ ¬B(x))      EG from 8

Instantiate existentials (step 2) before universals (step 5). UI may be applied to any name, while EI requires a name that has not been used yet.

In code. Prolog is essentially an engine for universal modus ponens. A rule with variables is a universally quantified implication, and a query is answered by instantiating it.

% ∀X (human(X) → mortal(X))
mortal(X) :- human(X).

% fact
human(socrates).

% query: is mortal(socrates) derivable?   UI with X = socrates, then MP
?- mortal(socrates).
% true.

Key takeaways

• UI and EG move from general to specific and back without restrictions.
• UG requires a truly arbitrary element. EI requires a fresh name.
• Universal modus ponens (UI + MP) is the workhorse of quantified reasoning.
• Instantiate existentials before universals so that the names stay fresh.

Practice

1. (Beginner) Derive mortal(socrates) formally from ∀x (H(x) → M(x)) and H(socrates), citing each rule.
2. (Intermediate) Find the error in this derivation: (1) ∃x Even(x) premise; (2) ∃x Odd(x) premise; (3) Even(c) EI 1; (4) Odd(c) EI 2; (5) Even(c) ∧ Odd(c); (6) ∃x (Even(x) ∧ Odd(x)) EG 5.
3. (Interview) A property-based test checks sort(xs) == sort(sort(xs)) on 10,000 random lists. Why does this not justify universal generalization, while a pen-and-paper proof for an "arbitrary list xs" does? Hint: compare "arbitrary" with "randomly sampled", and think about what UG requires of c.

Common Fallacies

Why. A fallacy is an argument pattern that looks valid but is not. Fallacies show up in proofs, code reviews, and incident post-mortems, so learning to recognize them is as important as learning the valid rules.

What.

Fallacy	Form	Example	Why invalid
Affirming the consequent	p → q, q ⊢ p	If the service is down, the alert fires. The alert fired. ∴ The service is down.	Critical row p = F, q = T (alert can fire for other reasons)
Denying the antecedent	p → q, ¬p ⊢ ¬q	If you are a CS major, you know logic. You are not. ∴ You don't know logic.	Critical row p = F, q = T
Circular reasoning	Conclusion used as premise	"The function is correct because its output matches the spec, and the spec was generated from its output."	Nothing independent supports the conclusion
Hasty generalization	P(a₁), …, P(aₖ) ⊢ ∀x P(x)	n² + n + 41 is prime for n = 0..10, so it is prime for all n	Fails at n = 40
Quantifier swap	∀x ∃y P ⊢ ∃y ∀x P	Every user has a password ∴ there is one password every user has	Order of dependence changed
Undistributed middle	All A are B, all C are B ⊢ all A are C	All cats are mammals, all dogs are mammals ∴ all cats are dogs	Shared class B says nothing about A vs C

The first two are the converse and inverse errors from 1.1 in argument form. You can check them mechanically:

from itertools import product

def is_valid(n_vars, premises, conclusion):
    for values in product([True, False], repeat=n_vars):
        if all(p(*values) for p in premises) and not conclusion(*values):
            return False, values
    return True, None

imp = lambda a, b: (not a) or b

# Affirming the consequent: p → q, q ⊢ p
print(is_valid(2, [lambda p, q: imp(p, q), lambda p, q: q], lambda p, q: p))
# (False, (False, True))

# Denying the antecedent: p → q, ¬p ⊢ ¬q
print(is_valid(2, [lambda p, q: imp(p, q), lambda p, q: not p], lambda p, q: not q))
# (False, (False, True))

# Modus tollens, for contrast: p → q, ¬q ⊢ ¬p
print(is_valid(2, [lambda p, q: imp(p, q), lambda p, q: not q], lambda p, q: not p))
# (True, None)

Key takeaways

• Affirming the consequent and denying the antecedent are the most common formal fallacies.
• Both fail on the row p = F, q = T.
• Examples never prove a universal statement, and swapping quantifiers changes meaning.
• When in doubt, reduce the argument to its form and search for a critical row.

Practice

1. (Beginner) Name the fallacy: "If a number is divisible by 4, it is even. 6 is even. Therefore 6 is divisible by 4."
2. (Intermediate) "If the patch fixes the bug, the regression test passes. The test passes. So the patch fixes the bug." Name the fallacy, then add a premise that makes the argument valid.
3. (Interview) "Our alert fires whenever the service is down. The alert did not fire, so the service is up." Is this reasoning valid? If it is valid, what could still make the conclusion false in production? Hint: separate validity from soundness, and question how true the premise is.

<a id="14-proof-techniques"></a>

1.4 Proof Techniques

A proof is an argument that a reader can verify step by step and that establishes a statement beyond doubt. This subchapter covers the standard proof strategies and when to use each one.

Direct Proof

Why. Most theorems have the form "for all x, if P(x) then Q(x)". The most natural way to prove such a statement is to start from what you know and work toward what you want.

What. To prove ∀x (P(x) → Q(x)) directly:

1. Let x be an arbitrary element of the domain. This is what licenses universal generalization at the end.
2. Assume P(x).
3. Unfold definitions into algebraic facts.
4. Use algebra, known theorems, and inference rules to reach the definition of Q(x).
5. Conclude Q(x).

Definitions used constantly:

Term	Definition
n is even	n = 2k for some integer k
n is odd	n = 2k + 1 for some integer k
a divides b (a ∣ b)	b = a·k for some integer k (with a ≠ 0)
r is rational	r = a/b for integers a, b with b ≠ 0

Theorem. For all x in D, if P(x) then Q(x).
Proof.   Let x ∈ D be arbitrary and assume P(x).
         [unfold the definition of P]
         [algebra / known results]
         [repackage the result to match the definition of Q]
         Therefore Q(x).  ∎

Example 1. If n is odd, then n² is odd.

Proof. Let n be an odd integer, so n = 2k + 1 for some integer k. Then n² = 4k² + 4k + 1 = 2(2k² + 2k) + 1. Since 2k² + 2k is an integer, n² has the form 2m + 1, so it is odd. ∎

Example 2. The sum of two rational numbers is rational.

Proof. Let r = a/b and s = c/d with integers a, b, c, d and b, d ≠ 0. Then r + s = (ad + bc)/(bd). The numerator and denominator are integers, and bd ≠ 0 because neither factor is zero. So r + s is rational. ∎

Testing a claim on many cases before proving it is cheap and catches false conjectures early. It is not a proof:

# Sanity check, not a proof: test the claim on many odd n before investing in a proof
assert all((n * n) % 2 == 1 for n in range(-1001, 1002, 2))   # n = -1001, -999, ..., 1001

Key takeaways

• Direct proof: take an arbitrary element, assume the hypothesis, and derive the conclusion.
• Begin by unfolding definitions. End by re-packaging the result into the target definition.
• Use different variable names for independent objects (k and j, not k twice).
• Numeric checks build confidence but never replace a proof of a universal claim.

Practice

1. (Beginner) Prove directly: the sum of two even integers is even.
2. (Intermediate) Prove: if a ∣ b and b ∣ c, then a ∣ c.
3. (Interview) Prove: if a ∣ b and a ∣ c, then a ∣ (bx + cy) for all integers x, y. Why is this fact the key to the correctness of the Euclidean algorithm (Chapter 4)? Hint: write b and c as multiples of a, then factor.

Proof by Contrapositive

Why. Sometimes the hypothesis gives you very little to work with. Knowing that "n² is even" does not easily tell you anything about n itself. The negated conclusion may be much more concrete, and the contrapositive lets you start from it.

What. Since p → q ≡ ¬q → ¬p (1.1), proving ¬q → ¬p directly proves p → q.

Goal:       p  ─────────────►  q        (hard: p gives little to work with)
Rewrite:   ¬q  ─────────────► ¬p        (easier: ¬q gives a concrete form)

Example 1. If n² is even, then n is even.

Direct attempt: n² = 2k, so n = √(2k), which leads nowhere.

Contrapositive: if n is odd, then n² is odd. We proved exactly this in the previous topic. ∎

Example 2. If 3n + 2 is odd, then n is odd.

Contrapositive: suppose n is even, so n = 2k. Then 3n + 2 = 6k + 2 = 2(3k + 1), which is even. ∎

Example 3. For positive integers a, b: if ab > 100, then a > 10 or b > 10.

Contrapositive: suppose a ≤ 10 and b ≤ 10 (De Morgan on the conclusion). Then ab ≤ 10 · 10 = 100. ∎

Use contrapositive when...	Example signal
The conclusion's negation is a concrete form	"n is even" is easier to use than "n² is even"
The conclusion is a disjunction	¬(q₁ ∨ q₂) gives two facts, ¬q₁ ∧ ¬q₂
The hypothesis involves a "non-" property	"if x is irrational..." becomes "if x is rational..."

Key takeaways

• To prove p → q, prove ¬q → ¬p instead. The two are logically equivalent.
• This works well when ¬q is concrete and p is not.
• Use De Morgan when the conclusion is a disjunction or conjunction.
• Say explicitly that you are proving the contrapositive.

Practice

1. (Beginner) Prove by contrapositive: if n² is odd, then n is odd.
2. (Intermediate) Prove: for real numbers x, y, if x + y ≥ 2, then x ≥ 1 or y ≥ 1.
3. (Interview) A hash table has m buckets and stores n keys. Prove that if n > m, then some bucket holds at least two keys. Hint: assume every bucket holds at most one key, and count.

Proof by Contradiction

Why. Some statements have no obvious starting point: "√2 is irrational" or "there are infinitely many primes". Each says something does not exist or is not finite. Assuming the opposite gives you a concrete object to work with, and you then show that this object cannot exist.

What. To prove a statement s:

1. Assume ¬s.
2. Derive a contradiction r ∧ ¬r (any statement together with its negation).
3. Conclude s, because ¬s → F is equivalent to s.

For a conditional p → q, assume p ∧ ¬q and derive a contradiction.

Classic example. √2 is irrational.

Proof. Suppose, for contradiction, that √2 is rational. Then √2 = a/b with integers a, b, b ≠ 0, in lowest terms (no common factor other than 1). Squaring gives a² = 2b², so a² is even, and therefore a is even (proved by contrapositive above). Write a = 2c. Then 4c² = 2b², so b² = 2c², which makes b² and hence b even. Now a and b are both even, which contradicts lowest terms. Therefore √2 is irrational. ∎

Contrapositive vs contradiction.

	Contrapositive	Contradiction
Assume	¬q	p ∧ ¬q (or ¬s for any statement s)
Goal	Exactly ¬p	Any contradiction
Applies to	Conditionals	Any statement
Strength	Clear target	Flexible, but the target is unknown in advance

In computing. The undecidability of the halting problem (Chapter 13) is a proof by contradiction:

def halts(program, data):
    """HYPOTHETICAL: returns True iff program(data) eventually stops. Assume it exists."""
    ...

def paradox(program):
    if halts(program, program):   # if program would halt when run on itself...
        while True:               # ...then loop forever
            pass
    return                        # ...otherwise halt immediately

# Consider paradox(paradox):
#   it halts  <=>  halts(paradox, paradox) is False  <=>  it does not halt.
# Contradiction, so no correct `halts` function can exist.

Pitfall. If your "contradiction" actually comes from an algebra mistake, the argument proves nothing. Check that the contradiction depends on the assumption ¬s.

Key takeaways

• Assume the statement is false and derive an impossibility.
• This is especially useful for "not", "no", "irrational", and "infinitely many" statements.
• Unlike the contrapositive, the contradiction can be anything, which gives flexibility at the cost of a clear target.
• State the assumption explicitly ("Suppose, for contradiction, ...") and point out exactly where it fails.

Practice

1. (Beginner) Prove by contradiction that there is no largest integer.
2. (Intermediate) Prove that √3 is irrational. Where does the argument need "if 3 ∣ n² then 3 ∣ n", and how would you prove that lemma?
3. (Interview) Prove that in any group of n ≥ 2 people, at least two have the same number of friends within the group (friendship is mutual). Hint: the possible friend counts are 0, …, n − 1. Can 0 and n − 1 both occur?

Proof by Cases

Why. Sometimes no single argument covers every object at once, but the domain splits naturally into a few kinds, and each kind is easy to handle. For example, integers are even or odd, reals are negative, zero, or positive, and an integer has remainder 0, 1, or 2 mod 3.

What. Based on the equivalence

(p₁ ∨ p₂ ∨ … ∨ pₖ) → q   ≡   (p₁ → q) ∧ (p₂ → q) ∧ … ∧ (pₖ → q)

1. Split into cases p₁, …, pₖ that together cover every possibility.
2. Prove q in each case separately.

The cases do not need to be disjoint, but they must be exhaustive.

Example. For every integer n, n² mod 4 is 0 or 1.

• Case 1: n even, n = 2k. Then n² = 4k², so n² ≡ 0 (mod 4).
• Case 2: n odd, n = 2k + 1. Then n² = 4(k² + k) + 1, so n² ≡ 1 (mod 4).

The two cases cover all integers. ∎

WLOG ("without loss of generality"). If the cases are symmetric (for example, "x ≤ y" and "y ≤ x" are handled by identical reasoning with the roles swapped), prove one case and say "WLOG assume x ≤ y".

Exhaustive proof. When the domain is finite and small, checking every case is a proof, and a computer can do the checking:

# Exhaustive proof: claim "(n + 1)^3 >= 3^n for 1 <= n <= 4". Finite cases, all checked.
assert all((n + 1) ** 3 >= 3 ** n for n in range(1, 5))   # 8>=3, 27>=9, 64>=27, 125>=81

# Proof by cases mirrored in code: the match must cover every possible residue
def square_mod_4(n):
    match n % 2:            # every integer falls into exactly one case
        case 0:             # n = 2k   -> n² = 4k²         ≡ 0 (mod 4)
            return 0
        case 1:             # n = 2k+1 -> n² = 4(k²+k) + 1 ≡ 1 (mod 4)
            return 1

assert all(square_mod_4(n) == (n * n) % 4 for n in range(-1000, 1000))  # sanity check

Key takeaways

• Split the domain into exhaustive cases and prove the claim in each one.
• Missing a case invalidates the whole proof. Check for boundary cases such as zero, equality, and negatives.
• Use WLOG to collapse symmetric cases, and say why the symmetry holds.
• For finite domains, exhaustive checking (including by computer) is a valid proof.

Practice

1. (Beginner) Prove that max(a, b) + min(a, b) = a + b for all real a, b.
2. (Intermediate) Prove that n³ − n is divisible by 3 for every integer n, using the cases n mod 3 ∈ {0, 1, 2}.
3. (Interview) Prove that no integer of the form 4k + 3 can be written as a sum of two perfect squares. Hint: use the worked example above and list the possible values of a² + b² mod 4.

Existence and Uniqueness Proofs

Why. Many results claim that something exists ("this equation has a solution") or that exactly one such thing exists ("the solution is unique"). In code, existence is "the function returns something" and uniqueness is "the result is well defined, so any two correct implementations agree".

What.

• Existence ∃x P(x): produce a witness c and verify P(c) (constructive), or argue that one must exist (non-constructive, see the next topic).
• Uniqueness ∃!x P(x) needs two parts:
  1. Existence: some x satisfies P.
  2. Uniqueness: if P(y) and P(z), then y = z. (Equivalently, any y ≠ x fails P.)

∃!x P(x)   ≡   ∃x ( P(x) ∧ ∀y ( P(y) → y = x ) )

Example (existence). Some positive integer can be written as a sum of two positive cubes in two different ways.

Witness: 1729 = 1³ + 12³ = 9³ + 10³. ∎

Example (existence and uniqueness). If a ≠ 0, the equation ax + b = 0 has a unique real solution.

• Existence: x = −b/a works, since a(−b/a) + b = 0.
• Uniqueness: if ay + b = 0 and az + b = 0, then ay = az. Since a ≠ 0, dividing gives y = z. ∎

A computer search can find a witness. Once found, the witness is a complete existence proof:

from itertools import combinations_with_replacement

def smallest_two_way_cube_sum(limit):
    sums = {}
    for a, b in combinations_with_replacement(range(1, limit), 2):  # a <= b avoids duplicates
        sums.setdefault(a**3 + b**3, []).append((a, b))
    return min((n, pairs) for n, pairs in sums.items() if len(pairs) >= 2)

print(smallest_two_way_cube_sum(20))   # (1729, [(1, 12), (9, 10)])

Key takeaways

• Existence: exhibit a witness and verify it, or argue indirectly.
• Uniqueness: assume two objects satisfy the property and show that they are equal.
• ∃! always needs both parts. Uniqueness alone does not imply existence.
• A computer-found witness is a valid existence proof. Failing to find one proves nothing.

Practice

1. (Beginner) Prove there exists a prime p such that p + 2 and p + 4 are also prime.
2. (Intermediate) Prove there is a unique positive integer n such that n² − 1 is prime. (Factor first.)
3. (Interview) An array holds n − 1 distinct integers from 1..n. Prove that exactly one value is missing, and give an O(n) time, O(1) extra space algorithm to find it. Hint: existence and uniqueness come from counting. For the algorithm, compare the actual sum with an expected one.

Constructive vs Non-constructive Proofs

Why. Knowing that a solution exists and knowing how to find one are different things. For a programmer, the difference matters: a constructive proof is essentially an algorithm, while a non-constructive proof only tells you the search will not be empty.

What.

	Constructive	Non-constructive
Shows	A specific witness, or a method to compute it	That a witness must exist
Typical tools	Explicit formulas, algorithms, induction	Contradiction, pigeonhole, parity, case splits on unknown facts
Gives you	An algorithm	Existence only
Example	x = −b/a solves ax + b = 0	Some two of any 13 people share a birth month

Classic non-constructive proof. There exist irrational numbers a, b such that aᵇ is rational.

Consider √2^√2. It is either rational or irrational:

• If it is rational, take a = b = √2. Done.
• If it is irrational, take a = √2^√2 and b = √2. Then aᵇ = √2^(√2·√2) = √2² = 2, which is rational. Done.

One of the two cases must hold, but the proof never says which one.

A constructive alternative. Take a = √2 and b = log₂ 9 (which is irrational). Then aᵇ = 2^(½ · log₂ 9) = 2^(log₂ 3) = 3.

Constructive proofs as programs. "For every n there is a prime greater than n" has a constructive proof that is also an algorithm. It is slow, but correct:

from math import factorial

def prime_greater_than(n):
    """Constructive proof that a prime > n exists: the smallest factor > 1 of n! + 1."""
    m = factorial(n) + 1
    d = 2
    while m % d != 0:   # find the smallest divisor d > 1; the smallest such divisor is always prime
        d += 1
    return d            # d > n: every k in 2..n divides n!, so it leaves remainder 1 when dividing m

print([prime_greater_than(n) for n in range(1, 8)])   # [2, 3, 7, 5, 11, 7, 71]

(This connects to the Curry–Howard correspondence: in constructive logic, proofs are programs and propositions are types.)

Key takeaways

• Constructive proofs produce the witness. Non-constructive proofs only show that one must exist.
• Non-constructive proofs often come from contradiction, pigeonhole, or a case split on an undecided fact.
• A constructive proof is an algorithm, though not necessarily an efficient one.
• When the goal is to compute something, look for a constructive proof.

Practice

1. (Beginner) Classify as constructive or non-constructive: (a) "6 is a perfect number because 1 + 2 + 3 = 6"; (b) "among any 367 people, two share a birthday".
2. (Intermediate) Give a constructive proof that for every integer n ≥ 1 there are n consecutive composite integers. (Consider (n + 1)! + 2, …, (n + 1)! + (n + 1).)
3. (Interview) The pigeonhole principle shows that among any 5 integers, two have a difference divisible by 4. Turn this non-constructive argument into an O(n) algorithm that returns such a pair from a list of n ≥ 5 integers. Hint: the pigeonholes are remainders mod 4. Use a dictionary keyed by remainder.

Counterexamples

Why. Proving a universal claim can be hard, but disproving one is often easy: a single failure is enough. Looking for counterexamples first saves you from trying to prove false statements.

What. From 1.2: ¬∀x P(x) ≡ ∃x ¬P(x). A single x where P(x) fails disproves ∀x P(x). For a conditional ∀x (P(x) → Q(x)), the counterexample must satisfy P and violate Q.

Claim	Counterexample
Every positive integer is a sum of two squares	3
n² + n + 41 is prime for every n ≥ 0	n = 40: 1681 = 41²
If n² is divisible by 4, then n is divisible by 4	n = 2
(a + b)² = a² + b²	a = b = 1

Where to look. Try small values, 0, 1, negatives, equal arguments, empty inputs, and boundary values. In code, these are the edge cases for unit tests.

Limits.

• A counterexample disproves a universal claim. It cannot disprove an existential one.
• Not finding a counterexample does not prove the claim. Goldbach's conjecture has been checked to about 4·10¹⁸ and is still unproven.

Analogy. A failing test case is a counterexample to "this code is correct". Property-based testing tools (e.g. Hypothesis, QuickCheck) search for counterexamples automatically and shrink them to minimal ones.

def find_counterexample(prop, candidates):
    """Return the first candidate where prop fails, or None (which proves nothing)."""
    for x in candidates:
        if not prop(x):
            return x
    return None

def is_prime(m):
    return m > 1 and all(m % d for d in range(2, int(m ** 0.5) + 1))

print(find_counterexample(lambda n: is_prime(n * n + n + 41), range(100)))  # 40
print(find_counterexample(lambda n: n % 4 == 0 or (n * n) % 4 != 0, range(1, 50)))  # 2

Key takeaways

• One counterexample disproves a universal claim.
• For a conditional claim, the counterexample must satisfy the hypothesis and violate the conclusion.
• Search small and boundary cases first.
• Absence of counterexamples is evidence, not proof.

Practice

1. (Beginner) Disprove: "for all integers a, b, if a² = b² then a = b."
2. (Intermediate) Disprove: "2ⁿ − 1 is prime for every prime n." Find the smallest counterexample, by hand or with code.
3. (Interview) "The greedy algorithm (always take the largest coin that fits) gives the minimum number of coins for any coin system." Find a coin system and amount that disprove this. Hint: use three denominations, including 1, where a large coin "overshoots" and forces many small coins afterward.

Proof Strategy and Writing

Why. Knowing the techniques is not enough. You also need to choose a technique for a given statement and write the proof so that a reader can verify it. A proof is communication: if the reader cannot follow it, it has not done its job.

Choosing a technique.

Statement shape	First technique to try
∀x (P(x) → Q(x))	Direct proof; contrapositive if ¬Q is more concrete than P
"There is no...", "irrational", "infinitely many"	Contradiction
Domain splits naturally (parity, sign, remainder)	Cases
∃x P(x)	Construct a witness
∃!x P(x)	Existence plus uniqueness
p ↔ q	Prove p → q and q → p separately
∀n ≥ n₀ P(n) with recursive structure	Induction (Chapter 3)
You suspect it is false	Search for a counterexample

Process.

                 Read the statement carefully
                              │
          Unfold definitions; identify quantifiers and form
                              │
              Try small examples ── fails? ──► Counterexample: done
                              │ holds
                    What is its shape?
   ┌────────────┬─────────────┼──────────────┬───────────────┐
 p → q       ∃x P(x)      "no"/"not"     domain splits    ∀n ∈ ℕ
   │            │             │              │               │
 Direct /    Construct   Contradiction     Cases         Induction
 contrapos.   witness
                              │
          Write it up: assumptions, steps, justifications, ∎

Work forward from the hypotheses ("what do I know?") and backward from the goal ("what would suffice?") until the two meet in the middle.

Writing checklist.

• State the theorem and the technique: "We prove the contrapositive", "Suppose, for contradiction, ...".
• Introduce every variable with its type: "Let n be an integer".
• Use different names for independent objects.
• Justify each non-trivial step (definition, lemma, or algebra).
• Avoid "clearly" and "obviously" unless the step really is immediate.
• Mark the end of the proof with ∎ (or "QED").

Bad vs good. Claim: the sum of two odd integers is even.

BAD:   Let m = 2k + 1 and n = 2k + 1. Then m + n = 4k + 2 = 2(2k + 1), which is even.
       Flaw: reusing k forces m = n, so only the case of equal numbers was proved.

GOOD:  Let m and n be odd integers, so m = 2k + 1 and n = 2j + 1 for some integers k, j.
       Then m + n = 2k + 2j + 2 = 2(k + j + 1). Since k + j + 1 is an integer,
       m + n is even.  ∎

Common mistakes.

Mistake	Example
Assuming the conclusion	Starting from the equation you want to prove and "simplifying" it to 0 = 0
Proof by example	Checking n = 1, 2, 3 and declaring the claim true for all n
Missing cases	Proving for x > 0 and x < 0, forgetting x = 0
Hidden division by zero	Cancelling a factor (a − b) when a = b
Converse confusion	Proving q → p when p → q was asked

Key takeaways

• Let the logical form of the statement guide the choice of technique.
• Test examples first. They suggest both proofs and counterexamples.
• Work forward from the hypotheses and backward from the goal.
• Write for a skeptical reader: introduce variables, justify steps, and state the structure.

Practice

1. (Beginner) Find the error: "Let a = b. Then a² = ab, so a² − b² = ab − b², so (a + b)(a − b) = b(a − b), so a + b = b, so 2b = b, so 2 = 1."
2. (Intermediate) Prove that for every integer n, n is even if and only if n² is even. Choose the technique for each direction and say why.
3. (Interview) A colleague doubts that your loop while lo < hi: mid = (lo + hi) // 2; ... always terminates. Sketch a proof that would convince them. Hint: find a non-negative integer quantity that strictly decreases on every iteration, then use the fact that a strictly decreasing sequence of non-negative integers cannot go on forever (well-ordering, Chapter 3).

<a id="2-sets-functions-and-relations"></a>