1. Mathematical Logic and Proof Techniques

Introduction and Context

Mathematical logic provides the language and discipline through which statements are represented, evaluated, and combined. In computer science, logic is not confined to theoretical mathematics. It underlies programming-language semantics, database queries, digital circuits, software verification, artificial intelligence, formal specification, security analysis, and algorithm design. Proof techniques, in turn, provide reliable methods for establishing that a claim is true rather than merely plausible.

A computer system ultimately manipulates symbols according to precise rules. Ambiguity, which may be tolerable in ordinary communication, is dangerous in software and hardware. Logic helps replace informal reasoning with statements whose meaning and conditions can be examined systematically. Proof techniques then allow a computer scientist to demonstrate properties such as algorithm termination, program correctness, security guarantees, and the validity of a data transformation.

This chapter develops propositional logic and predicate logic, explains quantifiers and inference, and introduces several central proof methods: direct proof, proof by contraposition, contradiction, cases, construction, mathematical induction, and invariant-based reasoning. It concludes by connecting these methods to formal specification and professional computing practice.

Learning Objectives

After completing this chapter, the reader should be able to:

1. Distinguish propositions from non-propositions and represent compound propositions using logical connectives.

2. Construct and interpret truth tables, logical equivalences, and satisfiability conditions.

3. Explain predicates, domains, free and bound variables, and the scope of quantifiers.

4. Translate between natural-language statements and symbolic predicate logic.

5. Apply valid inference rules to derive conclusions from premises.

6. Select an appropriate proof technique for a mathematical or computational claim.

7. Use induction and loop invariants to reason about recursively defined objects and iterative algorithms.

8. Express computational requirements using formal specifications and evaluate their limitations.

The Language of Propositions

A proposition is a declarative sentence that has exactly one truth value: true or false. “7 is prime” is a proposition and is true; “9 is less than 4” is a proposition and is false. Questions, commands, and expressions whose truth depends on an unspecified variable are not propositions by themselves. For example, “Close the application” is an instruction, while “x is greater than 5” becomes a proposition only after a value is assigned to x or a quantifier is supplied.

Simple propositions are commonly denoted by letters such as p, q, and r. Compound propositions are formed using logical connectives. The principal connectives are:

• Negation, ¬p, meaning “not p.”
• Conjunction, p ∧ q, meaning “p and q.”
• Disjunction, p ∨ q, meaning “p or q,” usually inclusive or.
• Exclusive disjunction, p ⊕ q, true when exactly one of p and q is true.
• Implication, p → q, meaning “if p, then q.”
• Biconditional, p ↔ q, meaning “p if and only if q.”

The truth of a compound proposition is determined by the truth values of its components and the connective used. Conjunction is true only when both components are true. Inclusive disjunction is false only when both components are false. Implication is false only in the case where p is true and q is false. This last point is often initially counterintuitive. The expression p → q does not assert that p is true; it asserts that whenever p occurs, q must occur. Consequently, an implication with a false antecedent is true under the standard material interpretation.

The converse of p → q is q → p. The inverse is ¬p → ¬q. The contrapositive is ¬q → ¬p. An implication is logically equivalent to its contrapositive, but generally not to its converse or inverse. For example, “If a number is divisible by 4, then it is even” is true. Its contrapositive, “If a number is not even, then it is not divisible by 4,” is also true. The converse, “If a number is even, then it is divisible by 4,” is false.

Truth Tables and Logical Equivalence

A truth table lists every possible assignment of truth values to the component propositions. With n distinct propositions, a complete table has 2^n rows. Truth tables are useful for checking equivalence, identifying tautologies, and exposing invalid reasoning.

A tautology is true under every valuation, such as p ∨ ¬p. A contradiction is false under every valuation, such as p ∧ ¬p. A contingent proposition is true under some valuations and false under others. Two propositions are logically equivalent, written P ≡ Q, if they have the same truth value under every valuation.

Important equivalences include:

• Double negation: ¬(¬p) ≡ p.
• De Morgan’s laws: ¬(p ∧ q) ≡ ¬p ∨ ¬q, and ¬(p ∨ q) ≡ ¬p ∧ ¬q.
• Implication: p → q ≡ ¬p ∨ q.
• Biconditional: p ↔ q ≡ (p → q) ∧ (q → p).
• Commutative laws: p ∧ q ≡ q ∧ p and p ∨ q ≡ q ∨ p.
• Distributive laws: p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r), with a dual law for disjunction.

Equivalence is more than a symbolic convenience. It permits a specification to be transformed into a form suitable for implementation, optimization, or automated reasoning without changing its meaning. For example, database query conditions may be rewritten using De Morgan’s laws, and Boolean circuits may be simplified by applying algebraic equivalences.

Predicate Logic and Quantification

Propositional logic treats complete statements as indivisible units. Predicate logic provides greater expressive power by representing objects, their properties, and relationships. A predicate such as Even(x) may be interpreted as “x is even.” It becomes a proposition when x is assigned a value or quantified.

A domain, or universe of discourse, specifies the objects under consideration. The predicate Even(x) has different implications when the domain is the integers, natural numbers, or programming-language values. A formula must therefore be interpreted relative to both a domain and an assignment of values to its variables.

The universal quantifier, ∀, means “for every,” while the existential quantifier, ∃, means “there exists.” Thus:

• ∀x P(x): P holds for every object x in the domain.
• ∃x P(x): P holds for at least one object x in the domain.

The statement ∀x (x + 0 = x) is true over the integers. The statement ∃x (x² = 2) is false over the integers but true over the real numbers. This illustrates why the domain is an essential part of a formal statement.

Quantifier order matters. The statement ∀x ∃y (y > x) over the integers says that every integer has a larger integer, which is true. The statement ∃y ∀x (y > x) says that there is one integer larger than every integer, which is false. Although the same symbols and predicate occur, changing their order changes the meaning.

Negating quantified statements requires changing the quantifier and negating the predicate:

• ¬∀x P(x) ≡ ∃x ¬P(x).
• ¬∃x P(x) ≡ ∀x ¬P(x).

A useful interpretation is that disproving a universal statement requires one counterexample, whereas proving an existential statement requires one witness. Conversely, proving a universal statement generally requires an argument covering an arbitrary object, and disproving an existential statement requires showing that no object satisfies the predicate.

Variables may be free or bound. A variable is bound when it lies within the scope of a quantifier; otherwise it is free. The formula P(x) has a free variable and is an open formula, while ∀x P(x) is a closed formula or sentence. Parentheses and scope are crucial. In ∀x(P(x) → ∃y R(x,y)), the variable x is bound by the universal quantifier and y by the existential quantifier. Poorly placed quantifiers are a major source of errors in formal specifications.

Inference: From Premises to Conclusions

An argument consists of premises and a conclusion. It is valid if there is no interpretation under which all premises are true and the conclusion is false. Validity concerns the structure of reasoning, not whether the premises happen to be factually true. An argument may be valid with false premises, although a sound argument must be both valid and based on true premises.

Common inference rules include:

• Modus ponens: from p and p → q, infer q.
• Modus tollens: from ¬q and p → q, infer ¬p.
• Hypothetical syllogism: from p → q and q → r, infer p → r.
• Disjunctive syllogism: from p ∨ q and ¬p, infer q.
• Conjunction: from p and q, infer p ∧ q.
• Simplification: from p ∧ q, infer p.
• Universal instantiation: from ∀x P(x), infer P(a) for an object a in the domain.
• Existential generalization: from P(a), infer ∃x P(x).

Two familiar invalid forms are affirming the consequent and denying the antecedent. From p → q and q, one cannot infer p; q may have another cause. From p → q and ¬p, one cannot infer ¬q; the implication does not say that q occurs only when p occurs. Recognizing these errors is important in debugging requirements, interpreting security alerts, and evaluating technical arguments.

A proof can be viewed as a sequence of justified statements beginning with assumptions and ending with the desired conclusion. In formal verification, inference rules may be applied by a human, a theorem prover, or a proof assistant. The underlying requirement remains the same: every step must preserve validity.

Choosing a Proof Technique

A mathematical statement often has the form “for every object satisfying condition A, condition B holds.” The most effective proof method depends on the logical structure of the claim and the available information.

Direct Proof

In a direct proof of A → B, assume A and derive B through definitions, known theorems, algebra, or valid inference. To prove that the sum of two even integers is even, let the integers be 2m and 2n. Their sum is 2(m+n), which is even. The proof works because it uses the definition of evenness directly.

For a universally quantified statement, the proof normally begins by choosing an arbitrary object in the domain. This avoids the mistake of proving the claim only for a convenient example.

Contrapositive Proof

Since A → B is equivalent to ¬B → ¬A, one may assume ¬B and derive ¬A. This is especially useful when the negation of the conclusion has a simpler structure. To prove that if n² is odd then n is odd, it is convenient to prove the contrapositive: if n is even, then n² is even.

Proof by Contradiction

To prove a statement P, assume ¬P and show that this assumption leads to a contradiction, often a statement of the form R ∧ ¬R. The method is powerful when the negation naturally produces incompatible cases or when the claim concerns impossibility. It must be used carefully: the contradiction must follow from the assumption together with accepted premises, not from an unnoticed assumption equivalent to the conclusion.

Proof by Cases

A proposition can sometimes be established by partitioning the possibilities. For an integer n, one may consider whether n is even or odd. The cases must be exhaustive, and the proof must establish the result in every case. Case analysis is common in algorithm proofs, where execution follows distinct branches.

Constructive Proof

A constructive proof of an existential statement provides an explicit witness and verifies that it satisfies the required property. To prove that there exists an even prime, one may provide 2 and show that it is both prime and even. Constructive arguments are particularly valuable in computer science because they often yield an algorithm for producing the object being asserted.

An existence proof that relies on contradiction may establish that an object exists without showing how to find it. This distinction matters in computability and algorithm design: mathematical existence does not automatically imply efficient construction.

Mathematical Induction

Induction proves a property P(n) for every natural number n. The standard form has two parts. First, prove the base case P(n₀). Second, assume P(k) for an arbitrary k ≥ n₀ and prove P(k+1). The assumption is the induction hypothesis. Together, these steps establish the result for all n ≥ n₀.

For example, to prove

1 + 2 + ··· + n = n(n+1)/2,

one verifies the formula at n = 1. Assuming it holds for k, add k+1 to both sides and simplify:

k(k+1)/2 + (k+1) = (k+1)(k+2)/2.

The inductive step therefore establishes the formula for k+1.

Strong induction assumes P(n₀), P(n₀+1), ..., P(k) in order to prove P(k+1). It is appropriate when the next case depends on several earlier cases, as in recursive decompositions or factorization arguments. Structural induction generalizes the same idea to recursively defined structures such as trees, expressions, and lists.

Induction is not a proof that the statement is true for a few initial values. The base case and inductive step are both essential. A common invalid approach verifies P(1), P(2), and P(3) and then assumes that all later values behave similarly.

Invariants and Algorithmic Reasoning

An invariant is a property that remains true throughout a process. In program verification, a loop invariant is a predicate that is true before the loop begins, remains true after each iteration, and, together with loop termination, helps establish the postcondition.

A standard loop-proof pattern is:

1. Initialization: show that the invariant holds before the first iteration.

2. Maintenance: assume it holds at the start of an iteration and show that the loop body preserves it.

3. Termination: use the invariant and the loop-exit condition to prove the desired result.

4. Termination argument: show that the loop eventually stops, often using a decreasing non-negative variant.

Consider a loop that scans an array to find its maximum. After processing the first i elements, a suitable invariant is that the recorded value equals the maximum of those i elements. Initialization holds after processing the first element. Maintenance follows because comparing the next element with the current maximum preserves the maximum property. When all elements have been processed, the invariant gives the postcondition.

Invariants also appear in distributed systems, cryptographic protocols, data structures, and model checking. A useful invariant is neither merely a description of the final result nor an unnecessarily strong assertion. It must be strong enough to support the conclusion and weak enough to be preserved by every operation.

Formal Specification in Computer Science

Formal specification expresses required behavior using mathematically precise statements. A specification may define preconditions, postconditions, invariants, state transitions, or temporal properties.

A Hoare triple has the form {P} C {Q}, meaning that if precondition P holds, execution of command C establishes postcondition Q, assuming the relevant execution model. For example:

{x ≥ 0} x := x + 1 {x > 0}

is valid under ordinary assignment semantics. For an assignment, the postcondition can be reasoned about by substituting the assigned expression into the desired postcondition. More complex programs can be verified by composing rules for sequencing, conditionals, and loops.

Formal specifications clarify requirements that natural language may leave ambiguous. A banking transfer might require that the sum of the two account balances is preserved, except for explicitly permitted fees. A concurrent data structure might require mutual exclusion, linearizability, or eventual response under stated assumptions. A database constraint may assert uniqueness, referential integrity, or a dependency between attributes.

Specifications do not automatically guarantee that an implementation is useful. A specification may be inconsistent, incomplete, too weak, or too costly to verify. For instance, a requirement that “the system responds quickly” is not formal until response time, workload, hardware assumptions, and exceptional conditions are defined. Formalization is therefore a requirements-engineering activity as well as a mathematical one.

An Illustrative Case: Verifying a Search Procedure

Background

Consider a software component that searches a sorted array A for a target value x. The component must return an index containing x when x is present, and otherwise report that x is absent.

Situation and Problem

A preliminary implementation repeatedly examines the middle of a candidate interval and discards the half that cannot contain x. The engineering team wants evidence that the implementation does not discard a valid location and that it terminates.

Analysis

Let the candidate interval at the start of an iteration be [L, R]. A natural invariant is:

“If x occurs in A, then it occurs at an index between L and R.”

The precondition establishes the invariant because the initial interval covers the entire array. If A[M] < x, sortedness implies that x cannot occur at an index at or below M, so replacing L with M+1 preserves the invariant. If A[M] > x, replacing R with M−1 is similarly safe. If A[M] = x, the required postcondition is achieved.

To prove termination, use the length R−L+1 as a variant. Whenever the loop does not return, the interval becomes strictly smaller. Since a non-negative integer cannot decrease indefinitely, the loop terminates.

Approach and Outcome

The complete specification can be expressed informally as follows:

• Precondition: A is sorted and L and R initially delimit the array.
• Invariant: any occurrence of x remains within [L, R].
• Variant: interval length R−L+1.
• Postcondition: either a valid index containing x is returned, or no index contains x.

The proof separates correctness from efficiency. The invariant establishes that the algorithm does not lose a possible answer; the termination variant establishes completion. A separate recurrence analysis establishes logarithmic worst-case search time for an interval of length n.

Learning Points

This case demonstrates that a proof is not merely an abstract exercise. The invariant exposes the precise information preserved by each iteration, while the variant addresses a different question: whether the procedure eventually stops. It also illustrates the importance of assumptions. Without sortedness, the interval-reduction arguments are invalid.

Applications, Risks, and Professional Practice

Logic is applied directly in Boolean circuit design, compiler optimization, access-control policies, SQL predicates, type systems, and automated planning. Predicate logic supports constraints such as “every employee assigned to a project must possess the required clearance” and “there exists an available server satisfying the workload and location requirements.” Temporal logic extends these ideas to statements about sequences of system states, such as “every request is eventually acknowledged” or “a locked resource is never simultaneously held by two processes.”

In security engineering, an invalid implication can produce an authorization flaw. A policy that confuses “only administrators may delete records” with “administrators may delete records” omits a necessary direction of implication. In safety-critical systems, proof obligations may concern failure modes, timing, and state transitions. In data governance, formal constraints help detect inconsistent records and clarify accountability.

Common mistakes include ignoring the domain of a quantified statement, changing quantifier order, treating implication as causation, using an example as a universal proof, omitting the induction base case, and proposing an invariant that is not preserved. Another error is proving a stronger claim than the implementation actually satisfies, or proving a weak claim that fails to guarantee the required behavior.

Automation changes the practical workflow but not the need for understanding. SAT solvers search for satisfying assignments, SMT solvers reason about richer theories such as arithmetic, model checkers explore state spaces, and interactive proof assistants check formally constructed proofs. AI-based tools can suggest invariants, generate proof drafts, or translate requirements, but their outputs require validation. A plausible proof suggestion is not evidence until its assumptions and every inference have been checked.

Professional use of formal reasoning also involves ethics and governance. Engineers should state assumptions, preserve traceability from requirements to proofs and tests, distinguish verified properties from unverified ones, and communicate residual uncertainty. Formal verification can increase confidence, but it cannot compensate for an incorrect specification or guarantee properties that were never expressed. Independent review is particularly important where errors could affect safety, privacy, financial assets, or public services.

Best Practices for Logical Reasoning

A disciplined approach begins by defining the domain, symbols, assumptions, and desired conclusion. Translate ambiguous language before manipulating it. For quantified statements, mark the scope of every quantifier and test whether changing quantifier order changes the meaning. When proving an implication, decide whether direct reasoning or contraposition makes the dependencies clearer. For algorithms, identify both a correctness invariant and a termination measure. Finally, test formal claims against boundary cases and counterexamples before investing in a lengthy proof.

In collaborative software development, proofs and specifications should be treated as engineering artifacts. They should be versioned, reviewed, linked to requirements, and maintained when the implementation changes. The most valuable formal argument is one that is precise enough to detect defects and understandable enough to guide future work.

Current Directions

Contemporary formal methods increasingly combine theorem proving, model checking, symbolic execution, runtime verification, and automated constraint solving. Hardware verification routinely uses SAT and SMT techniques, while software projects apply deductive verification to critical kernels, compilers, cryptographic libraries, and concurrent algorithms. Research also addresses scalable verification of distributed systems, probabilistic programs, machine-learning components, and systems whose behavior includes uncertainty.

A significant emerging concern is the formal specification of AI-enabled systems. Conventional logic can express safety constraints, but learned models may be difficult to characterize completely. Current work therefore combines logical contracts, robustness properties, statistical guarantees, monitoring, and human oversight. The central lesson remains unchanged: confidence in a computational system depends on clearly stated properties, explicit assumptions, and evidence appropriate to the risk.

Chapter Summary

Mathematical logic supplies a precise language for representing facts, conditions, relationships, and requirements. Propositional logic uses connectives and truth assignments; predicate logic adds objects, predicates, domains, and quantifiers. Truth tables establish tautology, contradiction, and equivalence, while inference rules support valid movement from premises to conclusions. Quantifier scope and order are essential to meaning.

Proof techniques provide different routes to certainty. Direct proof follows definitions and assumptions; contraposition reverses and negates an implication; contradiction derives impossibility from a negated claim; cases divide an exhaustive set of possibilities; construction supplies an explicit witness; induction handles recursively or sequentially defined structures. In algorithmic reasoning, invariants establish preserved properties and variants establish termination. Formal specifications apply these ideas to programs, databases, security policies, and distributed systems. Their effectiveness depends on precise assumptions, correct modeling, and careful review.

Key Terms

Proposition: A declarative statement with exactly one truth value.

Predicate: A logical expression describing a property or relation that becomes a proposition after variables are interpreted.

Tautology: A proposition that is true under every valuation.

Contradiction: A proposition that is false under every valuation.

Logical equivalence: A relation in which two formulas have identical truth values under all interpretations.

Implication: A compound proposition of the form p → q, false only when p is true and q is false.

Contrapositive: The logically equivalent form ¬q → ¬p of p → q.

Domain: The set of objects over which variables and quantifiers range.

Universal quantifier: The symbol ∀, asserting that a predicate holds for every object in the domain.

Existential quantifier: The symbol ∃, asserting that a predicate holds for at least one object in the domain.

Free variable: A variable not governed by a quantifier within a formula.

Bound variable: A variable occurring within the scope of a quantifier.

Inference rule: A formally justified pattern for deriving a conclusion from premises.

Soundness: The property that a valid inference system derives only true conclusions from true premises.

Mathematical induction: A proof method using a base case and an inductive step to establish a property for all relevant natural numbers.

Invariant: A property that remains true throughout the execution or transformation of a process.

Variant: A well-founded measure that demonstrates progress toward termination.

Formal specification: A mathematically precise description of required behavior or constraints.

Hoare triple: A specification form {P} C {Q}, relating a precondition, command, and postcondition.

Model checking: Automated exploration of a finite or symbolically represented state space to verify specified properties.

Review Questions

Short Answer Questions

1. What distinguishes a proposition from an open predicate?

2. State De Morgan’s laws for conjunction and disjunction.

3. Why are p → q and its contrapositive logically equivalent?

4. What is the difference between a free variable and a bound variable?

5. Name the three principal obligations in a loop-invariant proof.

Long Answer Questions

1. Explain propositional equivalence and show how truth tables can be used to establish it.

2. Discuss the meaning of universal and existential quantifiers, including the effect of quantifier order and negation.

3. Compare direct proof, contraposition, contradiction, and proof by cases, giving a suitable use for each.

4. Explain weak induction, strong induction, and structural induction, and distinguish their typical applications.

5. Describe how formal specifications and Hoare-style reasoning support software correctness while leaving some engineering limitations unresolved.

Analytical / Application Questions

1. A security rule states: “If a request is from an authenticated administrator, it may modify a record.” Explain why this rule does not by itself imply that every request capable of modifying a record is from an authenticated administrator. Express the stronger bidirectional requirement symbolically.

2. Design a loop invariant and a termination variant for an algorithm that computes the sum of the first n elements of an array. Explain initialization, maintenance, and termination.

3. Consider the statements ∀x∃y R(x,y) and ∃y∀x R(x,y). Construct an interpretation in which the first is true and the second is false, and explain the computational significance of the distinction.

22. Multiple Choice Questions with Answers

Question 1

Which statement is logically equivalent to p → q?

A. p ∧ q

B. ¬p ∨ q

C. p ∨ ¬q

D. ¬p ∧ q

Correct Answer: B. ¬p ∨ q

Question 2

What is required to disprove a universal statement ∀x P(x)?

A. A proof of P for one object

B. A proof that P is a tautology

C. A counterexample satisfying ¬P

D. A proof of ∃x P(x)

Correct Answer: C. A counterexample satisfying ¬P

Question 3

Which pair is logically equivalent under standard logic?

A. p → q and q → p

B. p → q and ¬p → ¬q

C. p → q and ¬q → ¬p

D. p ∨ q and p ∧ q

Correct Answer: C. p → q and ¬q → ¬p

Question 4

What does the statement ∀x∃y R(x,y) assert?

A. There is one y related to every x

B. For each x, at least one possibly different y is related to it

C. Every x is related to every y

D. There is no x related to any y

Correct Answer: B. For each x, at least one possibly different y is related to it

Question 5

Which inference is an instance of modus ponens?

A. p → q, q, therefore p

B. p → q, ¬p, therefore ¬q

C. p, p → q, therefore q

D. p ∨ q, q, therefore ¬p

Correct Answer: C. p, p → q, therefore q

Question 6

A proof assumes ¬P and derives both R and ¬R. Which technique is being used?

A. Direct proof

B. Proof by contradiction

C. Constructive proof

D. Strong induction

Correct Answer: B. Proof by contradiction

Question 7

In a loop-invariant proof, what does the maintenance step establish?

A. The loop has already terminated

B. The invariant holds before the first iteration

C. The loop body preserves the invariant

D. The postcondition is false

Correct Answer: C. The loop body preserves the invariant

Question 8

Which feature is essential for a valid mathematical induction proof?

A. Testing several numerical examples

B. A base case and a proof from an arbitrary case to the next case

C. A contradiction in every case

D. An existential witness only

Correct Answer: B. A base case and a proof from an arbitrary case to the next case

Question 9

Why is a decreasing non-negative loop measure useful?

A. It proves that the loop body is deterministic

B. It establishes that the loop eventually terminates

C. It replaces the need for an invariant

D. It proves that the input is sorted

Correct Answer: B. It establishes that the loop eventually terminates

Question 10

What assumption is essential in the binary-search case study for discarding half of the interval?

A. The array contains no duplicate values

B. The array is sorted

C. The target is positive

D. The interval has even length

Correct Answer: B. The array is sorted