Logic and Proof

Logic and Proof

Logic gives us a formal language to distinguish truth from falsehood. When you write an if statement, you are making a logical proposition. When a search engine ranks results, it applies logical rules. When a mathematician proves a theorem, they chain logical steps. Mastering discrete logic means mastering the art of precise, unambiguous reasoning.

Propositions

Logical Operators

Truth Tables

Truth tables exhaustively enumerate all possible input combinations and their resulting outputs. They are the primary tool for analyzing logical expressions.

Basic Truth Tables

Compound Example

Logical Equivalences

Two propositions are logically equivalent if they have identical truth tables — they are true in exactly the same cases.

Normal Forms

Validity and Satisfiability

Python Implementation

from itertools import product

def truth_table(propositions, expr_func, labels):
    """Generate a truth table for a logical expression."""
    n = len(propositions)
    header = " | ".join(labels) + " | Result"
    print(header)
    print("-" * len(header))

    for combo in product([True, False], repeat=n):
        vals = dict(zip(propositions, combo))
        result = expr_func(**vals)
        row = " | ".join(
            f"{vals[p]:^5}" for p in propositions
        ) + f" | {result:^6}"
        print(row)

# --- Basic Operators ---
def AND(p, q):   return p and q
def OR(p, q):    return p or q
def NOT(p):      return not p
def IMPLIES(p, q): return (not p) or q
def IFF(p, q):   return p == q

# --- Verify De Morgan's Laws ---
def verify_demorgan(n_tests=10000):
    import random
    for _ in range(n_tests):
        A = random.randint(0, 1)
        B = random.randint(0, 1)
        lhs_or = not (A or B)
        rhs_or = (not A) and (not B)
        lhs_and = not (A and B)
        rhs_and = (not A) or (not B)
        assert lhs_or == rhs_or, "De Morgan OR violated!"
        assert lhs_and == rhs_and, "De Morgan AND violated!"
    print("De Morgan's laws verified!")

# --- Tautology Checker (brute force) ---
def is_tautology(propositions, expr_func):
    """Check if expr is true for all truth assignments."""
    for combo in product([True, False], repeat=len(propositions)):
        vals = dict(zip(propositions, combo))
        if not expr_func(**vals):
            return False
    return True

# --- SAT Solver (simple DPLL-style) ---
def solve_dpll(clauses, assignment=None):
    """Simple DPLL satisfiability checker.
    clauses: list of tuples, each tuple is a clause (disjunction of literals).
              Literals are (variable_name, is_positive).
    """
    if assignment is None:
        assignment = {}

    # Simplify clauses based on current assignment
    simplified = []
    for clause in clauses:
        satisfied = False
        new_clause = []
        for (var, pos) in clause:
            if var in assignment:
                if assignment[var] == pos:
                    satisfied = True
                    break
            else:
                new_clause.append((var, pos))
        if not satisfied:
            simplified.append(new_clause)

    # Remove clauses that are subsets of others (not needed for correctness)

    # Check for empty clause (contradiction)
    if any(len(c) == 0 for c in simplified):
        return None

    # All clauses satisfied
    if len(simplified) == 0:
        return assignment

    # Unit propagation: if a clause has one literal, assign it
    for clause in simplified:
        if len(clause) == 1:
            var, pos = clause[0]
            if var not in assignment:
                new_assign = dict(assignment)
                new_assign[var] = pos
                return solve_dpll(simplified, new_assign)

    # Choose an unassigned variable and branch
    all_vars = set()
    for clause in simplified:
        for (var, _) in clause:
            all_vars.add(var)
    unassigned = [v for v in all_vars if v not in assignment]
    if not unassigned:
        return assignment

    var = unassigned[0]
    for val in [True, False]:
        new_assign = dict(assignment)
        new_assign[var] = val
        result = solve_dpll(simplified, new_assign)
        if result is not None:
            return result

    return None

# --- CNF Conversion ---
def to_cnf(p, q):
    """Convert P → Q to CNF and print."""
    # P → Q ≡ ¬P ∨ Q, which is already CNF
    print(f"  P → Q ≡ ¬P ∨ Q (CNF)")
    # Verify equivalence
    for pv, qv in product([True, False], repeat=2):
        impl = IMPLIES(pv, qv)
        cnf = OR(NOT(pv), qv)
        assert impl == cnf, f"CNF mismatch for P={pv}, Q={qv}"
    print("  Verified: P → Q ≡ ¬P ∨ Q")

if __name__ == "__main__":
    print("=== Truth Table: P → Q ===")
    truth_table(["P", "Q"], IMPLIES, ["P", "Q"])

    print("\n=== Truth Table: P ↔ Q ===")
    truth_table(["P", "Q"], IFF, ["P", "Q"])

    print("\n=== De Morgan's Laws ===")
    verify_demorgan()

    print("\n=== Tautology Check ===")
    print(f"P ∨ ¬P is tautology: {is_tautology(['P'], lambda P: OR(P, NOT(P)))}")
    print(f"P ∧ ¬P is tautology: {is_tautology(['P'], lambda P: AND(P, NOT(P)))}")
    print(f"(P → Q) ↔ (¬Q → ¬P) is tautology: {is_tautology(['P', 'Q'], lambda P, Q: IFF(IMPLIES(P,Q), IMPLIES(NOT(Q), NOT(P))))}")

    print("\n=== CNF Conversion ===")
    to_cnf("P", "Q")

    print("\n=== SAT Solver ===")
    # (P ∨ Q) ∧ (¬P ∨ Q) ∧ (P ∨ ¬Q)
    clauses_sat = [
        [("P", True), ("Q", True)],
        [("P", False), ("Q", True)],
        [("P", True), ("Q", False)],
    ]
    result = solve_dpll(clauses_sat)
    print(f"SAT: {clauses_sat}")
    print(f"Satisfying assignment: {result}")

    # (P) ∧ (¬P) — unsatisfiable
    clauses_unsat = [
        [("P", True)],
        [("P", False)],
    ]
    result = solve_dpll(clauses_unsat)
    print(f"\nSAT: {clauses_unsat}")
    print(f"Result: {result}")

Applications in AI/ML

1. Logic Programming (Prolog)

Logic programming languages like Prolog encode knowledge as logical formulas and use unification and resolution to answer queries. A Prolog program is a set of Horn clauses (implications with a single consequent):

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

This directly encodes the logical rule: "X is an ancestor of Y if X is a parent of Y, or if X is a parent of Z and Z is an ancestor of Y."

2. Constraint Satisfaction Problems (CSPs)

Many AI problems are modeled as CSPs, where variables must satisfy logical constraints:

• Scheduling: Staff shifts must cover all hours, no person works two shifts at once
• Map coloring: Adjacent regions must have different colors
• Sudoku: Each row, column, and box contains each digit exactly once

CSP solvers use logical inference (arc consistency, forward checking) combined with search to find satisfying assignments.

3. Knowledge Representation and Reasoning

Description logics and OWL (Web Ontology Language) represent knowledge using logical constructs. Automated reasoners check consistency of ontologies and infer new facts:

• "All humans are mortal" + "Socrates is human" → "Socrates is mortal"
• OWL reasoners detect contradictions in biomedical ontologies with millions of axioms

4. Hardware Verification

SAT solvers and model checkers verify that digital circuits satisfy their specifications. A circuit with $n$ inputs can be modeled as a Boolean formula; satisfiability of its negation indicates a bug.

5. AI Planning (SATPlan)

The planning problem — finding a sequence of actions to reach a goal — can be encoded as SAT. Each action and time step generates Boolean variables, and constraints ensure action preconditions are met. Modern planners encode planning as SAT and use CDCL solvers to find plans efficiently.

6. Neural Network Verification

Verifying that a neural network's output is correct within input bounds (e.g., a self-driving car always stops at red) is formulated as a satisfiability problem over piecewise-linear functions.

Common Mistakes

Interview Questions

Q1: What is the truth table for the conditional? Why is "if False then True" true?

Q2: Prove that the conditional and biconditional are not equivalent.

Q3: Convert $\neg(P \to (Q \land \neg R))$ to CNF.

Q4: Explain the SAT problem and why it matters for computer science.

Q5: What is the difference between tautology, satisfiability, and validity?

Q6: How does De Morgan's law apply to programming?

# Instead of:
if not (age >= 18 and has_id):
    deny()

# Write:
if age < 18 or not has_id:
    deny()

Practice Problems

Problem 1: Truth Table Construction

Problem 2: Logical Equivalence

Problem 3: CNF Conversion

Problem 4: Satisfiability

Problem 5: Prove Using Logical Equivalences

Quick Reference

Cross-References

• Set Theory — set operations and De Morgan's laws in the set context — the logical operators and set operations share identical algebraic structure (AND ↔ Intersection, OR ↔ Union, NOT ↔ Complement)
• Boolean Algebra — Boolean algebra, switching circuits, and gate-level implementations of logical operators
• Combinatorics — counting techniques used in logical enumeration and proof by exhaustion
• Graph Theory — logical constraints in graph coloring and path problems
• Automata Theory — how logical formulas define regular languages and finite automata
• Information Theory — the connection between logical uncertainty and Shannon entropy
• Discrete Mathematics Applications — applied uses of logic in cryptography, coding theory, and verification