Logic & Propositions

A proposition is a declarative statement that is either true (T or 1) or false (F or 0) — never both, never neither. This is the law of excluded middle (every proposition is T or F) paired with the law of non-contradiction (no proposition is both T and F). Together, these two laws define the classical two-valued logic that underlies almost all of computer science.

Examples of valid propositions:

• "7 is a prime number" (T)
• "The number 4 is odd" (F)
• "Every Python list is mutable" (T)
• "This program terminates in under 1 second on all inputs" (T or F — we just might not know which)

Non-examples (not propositions):

• "What is the time?" — a question, not a declarative statement
• "Close the door." — a command
• "This statement is false." — the liar's paradox, neither T nor F in classical logic
• "x > 5" — not a proposition by itself because the truth value depends on x; this is a predicate, covered later

In logic, we use propositional variables — typically lowercase letters p, q, r, s — to stand for arbitrary propositions. This lets us study the structure of logical arguments independently of their content. The statement "p AND q" is valid regardless of whether p is about primes or planets.

# In Python, bool is literally a proposition type
p = True    # "7 is prime"
q = False   # "4 is odd"

# Every Boolean expression in a program IS a proposition
x = 10
proposition = (x > 5)   # evaluates to True
print(type(proposition))  # <class 'bool'>

Logical connectives are the "words" of logic — they combine simpler propositions into compound ones. There are five fundamental connectives:

1. Negation (NOT, ¬p) — flips the truth value. If p is T, ¬p is F, and vice versa. In code: !p or not p.

2. Conjunction (AND, p ∧ q) — true only when both p and q are true. This is the logical AND gate. In code: p && q or p and q. Think of it as a series circuit: both switches must be closed for current to flow.

3. Disjunction (OR, p ∨ q) — true when at least one of p or q is true (inclusive OR). In code: p || q or p or q. Think of it as a parallel circuit.

4. Implication (IF-THEN, p → q) — "if p then q". This is the most subtle connective. It is only false when p is true and q is false. Crucially, when p is false (the hypothesis is false), the implication is vacuously true regardless of q. Example: "If it rains, I carry an umbrella" is not violated on a sunny day when I don't carry an umbrella. The implication p → q is logically equivalent to ¬p ∨ q.

5. Biconditional (IFF, p ↔ q) — "p if and only if q". True exactly when p and q have the same truth value (both T or both F). This is logical equality. In code: p == q for booleans.

The precedence (binding strength, highest to lowest): ¬, ∧, ∨, →, ↔. So ¬p ∧ q → r means ((¬p) ∧ q) → r.

p, q = True, False

print(not p)        # ¬p  → False
print(p and q)      # p∧q → False
print(p or q)       # p∨q → True
print(not p or q)   # p→q (equivalent form) → False
print(p == q)       # p↔q → False

# Implication: vacuously true when antecedent is false
rain = False
umbrella = False
# "if rain then umbrella" — not violated!
implication = (not rain) or umbrella
print(implication)  # True — vacuous truth

A truth table exhaustively enumerates all possible truth-value assignments to the propositional variables in a formula and computes the formula's truth value under each assignment. It is a mechanical, algorithmic procedure — essentially brute-force verification.

For n propositional variables, there are 2ⁿ rows (all combinations of T/F assignments).

Constructing a truth table:

1. List all propositional variables as column headers.
2. Fill in all 2ⁿ combinations of T/F systematically (like binary counting).
3. Add columns for each sub-formula, building up to the full formula.

Example: p → q

The key row is (T, F) → F: this is the only way an implication fails.

Tautology, Contradiction, Satisfiability:

• A formula is a tautology if every row is T (e.g., p ∨ ¬p, called the law of excluded middle).
• A formula is a contradiction (or unsatisfiable) if every row is F (e.g., p ∧ ¬p).
• A formula is satisfiable if at least one row is T.

Satisfiability (SAT) is one of the most important problems in CS — the first problem proven NP-complete (Cook-Levin theorem, 1971). Modern SAT solvers check satisfiability for formulas with millions of variables and are used in chip verification.

from itertools import product

def truth_table(formula_fn, var_names):
    n = len(var_names)
    print(' | '.join(var_names) + ' | result')
    print('-' * (6 * n + 10))
    for values in product([True, False], repeat=n):
        result = formula_fn(*values)
        row = ' | '.join('T' if v else 'F' for v in values)
        print(f"{row} |   {'T' if result else 'F'}")

# p → q  (implication)
truth_table(lambda p, q: (not p) or q, ['p', 'q'])

# Tautology: p ∨ ¬p
truth_table(lambda p: p or not p, ['p'])

Two formulas φ and ψ are logically equivalent (written φ ≡ ψ) if they have identical truth values for every possible assignment of their variables. Equivalence is verified by showing their truth tables are identical column-by-column, or by algebraic derivation using known laws.

Logical equivalences form an algebra — you can substitute equals for equals and simplify complex formulas, exactly as in high-school algebra. The key laws are:

Double Negation: ¬¬p ≡ p

De Morgan's Laws (among the most useful):

• ¬(p ∧ q) ≡ ¬p ∨ ¬q
• ¬(p ∨ q) ≡ ¬p ∧ ¬q

Intuition: "Not (raining AND cold)" = "Not raining OR not cold" — at least one condition fails.

Implication Elimination: p → q ≡ ¬p ∨ q (removes the → connective)

Contrapositive: p → q ≡ ¬q → ¬p (same truth table, different form)

Commutativity: p ∧ q ≡ q ∧ p; p ∨ q ≡ q ∨ p

Associativity: (p ∧ q) ∧ r ≡ p ∧ (q ∧ r)

Distributivity:

• p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
• p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)

Absorption: p ∧ (p ∨ q) ≡ p

Identity: p ∧ T ≡ p; p ∨ F ≡ p

Domination: p ∨ T ≡ T; p ∧ F ≡ F

These laws underpin Boolean algebra, which is isomorphic to propositional logic and directly describes how digital circuits work. Circuit simplification IS logical simplification — fewer gates, lower power consumption.

# Verify De Morgan's law computationally
from itertools import product

for p, q in product([True, False], repeat=2):
    lhs = not (p and q)        # ¬(p ∧ q)
    rhs = (not p) or (not q)   # ¬p ∨ ¬q
    assert lhs == rhs, f"De Morgan failed at p={p}, q={q}"

print("De Morgan's law verified for all inputs.")

# Contrapositive: p→q ≡ ¬q→¬p
for p, q in product([True, False], repeat=2):
    forward = (not p) or q          # p → q
    contra  = q or (not p)          # ¬q → ¬p (same!)
    assert forward == contra
print("Contrapositive equivalence verified.")

Any propositional formula can be converted to a canonical form — a standardized structure that makes automated reasoning easier. The two standard forms are:

Conjunctive Normal Form (CNF): A conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals (a variable or its negation).

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

Disjunctive Normal Form (DNF): A disjunction (OR) of terms, where each term is a conjunction (AND) of literals.

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

Why normal forms matter:

• SAT solvers accept input in CNF (DIMACS format is the universal standard).
• A formula in CNF is satisfiable if and only if every clause can be simultaneously satisfied — this structural insight powers DPLL and CDCL algorithms.
• Resolution, the core proof rule in automated theorem proving, works on clauses in CNF.
• Hardware synthesis tools convert Boolean expressions to CNF/DNF as an intermediate step.

Converting to CNF:

1. Eliminate ↔ and → using equivalences.
2. Push ¬ inward using De Morgan's laws until negation only touches variables (NNF = Negation Normal Form).
3. Distribute ∧ over ∨.

A useful insight: the truth table directly gives you CNF and DNF. Each row where the formula is F contributes a clause to the CNF (using the falsifying assignment). Each row where the formula is T contributes a minterm to the DNF.

# Convert a formula to CNF via truth table (minterm/maxterm method)
# Formula: p → q  i.e.  ¬p ∨ q
# Truth table:
# p=T,q=T: T   — satisfying
# p=T,q=F: F   — falsifying → clause: (¬p ∨ q)
# p=F,q=T: T
# p=F,q=F: T
# CNF: just one clause (¬p ∨ q)  — matches ¬p∨q, as expected!

# In the DIMACS CNF format used by SAT solvers:
# Variables are integers 1..n; negation is negative
# p→q  becomes  -1 2 0  (one clause: -p ∨ q)
cnf_clause = [-1, 2, 0]  # 0 terminates each clause
print("DIMACS clause for p→q:", cnf_clause)

Propositional logic is powerful but limited — it cannot express statements about objects or relationships. "Every natural number has a successor" cannot be stated with propositions alone. Predicate logic (also called first-order logic, FOL) extends propositional logic with:

Predicates — functions that return T or F for given objects. P(x) means "x has property P". Example: Prime(7) is T; Even(3) is F. Predicates can have multiple arguments: Greater(x, y) means x > y.

Domain of discourse — the set of objects the variables range over. Always state this explicitly! "∀x, P(x)" means different things if x ranges over integers vs. real numbers.

Universal Quantifier (∀): ∀x P(x) means "for ALL x in the domain, P(x) is true". To disprove it, you only need ONE counterexample.

Existential Quantifier (∃): ∃x P(x) means "there EXISTS at least one x in the domain such that P(x) is true". To prove it, you only need to exhibit ONE example.

Translating English:

• "All students passed" → ∀x (Student(x) → Passed(x))
• "Some student failed" → ∃x (Student(x) ∧ Failed(x))

Note the asymmetry: universal statements use →, existential statements use ∧. This is a common source of errors. "∀x (Student(x) ∧ Passed(x))" would wrongly claim everything in the domain is a student.

Negating Quantified Statements (De Morgan's for quantifiers):

• ¬(∀x P(x)) ≡ ∃x ¬P(x) — "Not all x satisfy P" ≡ "Some x does not satisfy P"
• ¬(∃x P(x)) ≡ ∀x ¬P(x) — "No x satisfies P" ≡ "All x fail to satisfy P"

These negation rules are essential for proof by contradiction and are used constantly in algorithm analysis ("there is no faster algorithm" ↔ "all algorithms are at least this slow").

# Python mirrors predicate logic naturally
domain = range(1, 11)  # {1, 2, ..., 10}

def prime(n):
    return n > 1 and all(n % i != 0 for i in range(2, n))

def even(n):
    return n % 2 == 0

# ∀x in domain: even(x) → False   (not all numbers 1-10 are even)
universal = all(even(x) for x in domain)
print(f"∀x Even(x): {universal}")  # False

# ∃x in domain: prime(x) ∧ even(x)   (is there an even prime?)
existential = any(prime(x) and even(x) for x in domain)
print(f"∃x (Prime(x) ∧ Even(x)): {existential}")  # True (x=2)

# Negation: ¬(∀x prime(x)) ≡ ∃x ¬prime(x)
not_all_prime = any(not prime(x) for x in domain)
print(f"∃x ¬Prime(x): {not_all_prime}")  # True

Quantifiers can be nested, and the order matters fundamentally when quantifiers of different types are mixed.

Same-type quantifiers are commutative:

• ∀x ∀y P(x,y) ≡ ∀y ∀x P(x,y)
• ∃x ∃y P(x,y) ≡ ∃y ∃x P(x,y)

Mixed-type quantifiers are NOT commutative — this is one of the most important and counterintuitive facts in logic:

• ∀x ∃y (y > x) — "For every number, there exists a larger one" — TRUE over the integers (just take y = x + 1)
• ∃y ∀x (y > x) — "There exists a number larger than all numbers" — FALSE over the integers

The difference: in ∀x ∃y, the witness y can depend on x. In ∃y ∀x, one fixed y must work for all x simultaneously.

Reading nested quantifiers systematically: scan left to right. Each ∀ means "for any choice an adversary makes"; each ∃ means "we get to choose (possibly depending on prior choices)".

Formal definition of a limit (from calculus, the classic example):

• lim_{x→a} f(x) = L is: ∀ε > 0, ∃δ > 0, ∀x (0 < |x - a| < δ → |f(x) - L| < ε)
• Reading this aloud: "for any (adversarial) ε, we can find δ, such that for any (adversarial) x close to a, f(x) is close to L."

This is why calculus students struggle with the ε-δ definition — it hides three nested quantifiers with two alternations. Once you see it as a quantifier expression, the game-theoretic reading (adversary picks ε, you respond with δ, adversary picks x) makes it tractable.

# Demonstrate quantifier non-commutativity computationally
domain = range(-5, 6)  # integers -5..5

# ∀x ∃y: y > x   (for every x, some y is larger)
all_have_larger = all(
    any(y > x for y in domain)
    for x in domain
)
print(f"∀x ∃y (y>x) over -5..5: {all_have_larger}")  # False! -5 works, but 5 fails

big_domain = range(-100, 101)
all_have_larger2 = all(
    any(y > x for y in big_domain)
    for x in big_domain
)
print(f"∀x ∃y (y>x) over -100..100: {all_have_larger2}")  # still False at x=100

# Over all integers (unbounded), it's True — but we can't iterate ℤ in code
# ∃y ∀x: y > x   (one y larger than everything)
one_larger_than_all = any(
    all(y > x for x in domain)
    for y in domain
)
print(f"∃y ∀x (y>x) over -5..5: {one_larger_than_all}")  # False

Logic gives us not just a language but also a proof system — rules for deriving new truths from existing ones. These are rules of inference: patterns of the form "given these premises, you may conclude this."

Modus Ponens (the most fundamental rule):

• Premises: p → q, and p
• Conclusion: q
• Reading: "If the rule holds and the condition is met, the conclusion follows."
• In code: every if statement uses this!

Modus Tollens (contrapositive reasoning):

• Premises: p → q, and ¬q
• Conclusion: ¬p
• Reading: "If the rule holds and the conclusion failed, the hypothesis must have failed too."

Hypothetical Syllogism (transitivity of implication):

• Premises: p → q, and q → r
• Conclusion: p → r

Disjunctive Syllogism:

• Premises: p ∨ q, and ¬p
• Conclusion: q

Resolution (the workhorse of automated theorem proving):

• Premises: p ∨ q, and ¬p ∨ r
• Conclusion: q ∨ r
• This rule, applied repeatedly to CNF clauses, is the basis for DPLL/CDCL SAT solvers and Prolog's execution model.

Soundness vs. Completeness:

• A proof system is sound if every derivable conclusion is actually true (no false conclusions from true premises).
• A proof system is complete if every true statement is derivable.
• First-order logic with standard rules is both sound and complete (Gödel's completeness theorem, 1929). But Gödel's incompleteness theorems (1931) show that any consistent system powerful enough to express arithmetic has true statements that are unprovable within the system — a profound limitation.

# Modus ponens as a Python function
def modus_ponens(p: bool, implication_p_q: bool) -> bool:
    """Given p and (p→q), return q.
    Note: implication is passed as a precomputed bool here.
    """
    # If p is True and p→q is True, q must be True
    # (because p→q is False only when p=T, q=F)
    if p and implication_p_q:
        return True  # q is True
    elif not p:
        return None  # q indeterminate from these premises alone
    else:  # p=T, implication=F means inconsistent premises
        raise ValueError("Inconsistent: p is True but p→q is False")

# Example: "If it is raining (p), the ground is wet (q)."
#           It is raining. Therefore: the ground is wet.
p = True
p_implies_q = True  # rule holds
q = modus_ponens(p, p_implies_q)
print(f"Ground is wet: {q}")  # True

The connection between logic and CS is not metaphorical — it is mathematically precise.

Boolean Circuits: Every logical formula over propositions corresponds directly to a combinational logic circuit. AND gates implement ∧, OR gates implement ∨, NOT gates implement ¬. The problem of minimizing circuit complexity (fewest gates) is exactly the problem of finding the simplest logically equivalent formula. The Karnaugh map is a visual tool for this simplification. The AND, OR, NOT basis is universal — every Boolean function can be computed. So is {NAND} alone — a single gate type suffices.

Type Systems (Curry-Howard Correspondence): In typed functional programming languages like Haskell or Coq, there is a startling isomorphism:

• A type corresponds to a proposition
• A program of that type corresponds to a proof of that proposition
• A -> B (function type) corresponds to A → B (implication)
• (A, B) (pair/tuple) corresponds to A ∧ B (conjunction)
• Either A B (sum type) corresponds to A ∨ B (disjunction)
• The empty type Void corresponds to ⊥ (contradiction)

Writing a program IS constructing a proof. A type error IS a logical inconsistency.

Databases: A SQL query SELECT * FROM users WHERE age >= 18 AND country = 'US' evaluates a predicate P(x) = Age(x) ≥ 18 ∧ Country(x) = 'US' over the domain of users. This is first-order logic directly. Relational algebra — the theory behind SQL — is a subset of first-order logic. Query optimization uses logical equivalences to rewrite predicates into more efficient forms.

Formal Verification: Tools like TLA+ (Leslie Lamport) and Alloy specify systems as logical formulas and use model checkers (essentially exhaustive truth-table evaluation over a bounded state space) to verify correctness. The Amazon and Microsoft distributed systems teams use TLA+ to prove properties of their protocols.

-- Curry-Howard: types are propositions, programs are proofs
-- In Haskell:

-- The type (a, b) is the proposition A ∧ B
-- A value of type (a, b) IS a proof of A ∧ B
conjunction_proof :: (Bool, Int)
conjunction_proof = (True, 42)  -- witness: both A and B hold

-- The type Either a b is the proposition A ∨ B
disjunction_proof :: Either String Int
disjunction_proof = Left "hello"  -- witness: A holds

-- The type a -> b is the proposition A → B
-- A function IS a proof of implication
implication_proof :: Bool -> Bool
implication_proof p = p || True  -- always True (proves p → T)

-- There is NO value of type Void (the empty type)
-- This corresponds to: contradiction has no proof
-- absurd :: Void -> a

The Boolean Satisfiability Problem (SAT) asks: given a propositional formula, does there exist an assignment of truth values to its variables that makes it true?

This is one of the most important problems in all of computer science. The Cook-Levin theorem (1971) proved that SAT is NP-complete — it was the first problem proven NP-complete, anchoring the entire NP-completeness theory. This means:

1. SAT is in NP: given a satisfying assignment, we can verify it in polynomial time.
2. SAT is NP-hard: every problem in NP can be reduced to SAT in polynomial time.

Since SAT is NP-complete, if we found a polynomial-time algorithm for SAT, we would prove P = NP and solve one of the Millennium Prize Problems (worth $1 million). Almost all complexity theorists believe P ≠ NP.

3-SAT is the special case where every clause has exactly 3 literals. It is still NP-complete (and often the canonical NP-complete problem used in reductions).

2-SAT, however, is solvable in polynomial time (O(n + m) via strongly connected components on an implication graph). This is a beautiful example of how a tiny structural restriction changes the complexity class drastically.

Modern SAT Solvers: Despite NP-completeness in the worst case, modern solvers (MiniSat, Glucose, Z3) handle formulas with millions of variables in practice using:

• DPLL algorithm (Davis-Putnam-Logemann-Loveland): backtracking search with unit propagation
• CDCL (Conflict-Driven Clause Learning): learn new clauses from conflicts to prune the search space

Intel and AMD use SAT solvers to verify that chip designs are bug-free before fabrication. The cost of a bug post-fabrication (Intel's 1994 FDIV bug: $475M recall) makes formal verification economically essential.

# Simple DPLL SAT solver for 3-CNF
# Formula: list of clauses; each clause: list of literals (int; neg = negation)
# Variable i represented as i, negation as -i

def dpll(clauses, assignment={}):
    # Unit propagation: if a clause has one unassigned literal, force it
    changed = True
    while changed:
        changed = False
        for clause in clauses:
            unassigned = [l for l in clause 
                          if abs(l) not in assignment]
            satisfied = any(
                (l > 0 and assignment.get(l) == True) or
                (l < 0 and assignment.get(-l) == False)
                for l in clause
            )
            if satisfied:
                continue
            if len(unassigned) == 0:
                return None  # conflict: empty clause
            if len(unassigned) == 1:
                lit = unassigned[0]
                assignment[abs(lit)] = (lit > 0)
                changed = True
    # Check: all clauses satisfied?
    if all(any((l > 0 and assignment.get(l)) or 
               (l < 0 and not assignment.get(-l, True))
               for l in clause) for clause in clauses):
        return assignment
    # Pick unassigned variable and branch
    all_vars = {abs(l) for clause in clauses for l in clause}
    unassigned_vars = all_vars - set(assignment.keys())
    if not unassigned_vars:
        return None
    var = next(iter(unassigned_vars))
    for val in [True, False]:
        new_assign = dict(assignment)
        new_assign[var] = val
        result = dpll(clauses, new_assign)
        if result is not None:
            return result
    return None  # unsatisfiable

# (p ∨ q) ∧ (¬p ∨ r) ∧ (¬q ∨ ¬r)
clauses = [[1, 2], [-1, 3], [-2, -3]]
print(dpll(clauses, {}))  # Some satisfying assignment