Mathematical Logic and Proof Techniques

Introduction

Mathematical logic provides the language and discipline needed to reason precisely about computer programs, algorithms, data structures, software specifications, and digital systems. A computer executes formal instructions, but determining whether those instructions are correct requires arguments that are independent of particular test cases. Logic supplies the rules for constructing such arguments; proof techniques supply reusable methods for establishing that a claim is true.

In computer science, logic is used to specify program behavior, verify algorithms, analyze complexity, design circuits, reason about databases, and prove properties of security protocols. For example, testing may show that a sorting algorithm works on many inputs, whereas a proof can establish that it works for every input satisfying stated assumptions.

This chapter develops propositions, logical connectives, predicates, quantifiers, inference rules, and several central proof techniques: direct proof, constructive proof, proof by contraposition, proof by contradiction, and mathematical induction. It also examines common fallacies and applies formal reasoning to a computational claim.

Learning Objectives

By the end of this chapter, you should be able to:

1. Distinguish propositions from non-propositions and represent compound propositions symbolically.
2. Construct and interpret truth tables, logical equivalences, and implications.
3. Use predicates and quantifiers correctly, including negation of quantified statements.
4. Apply valid inference rules to derive conclusions from premises.
5. Construct direct, constructive, contrapositive, contradiction, and inductive proofs.
6. Identify invalid arguments and common logical fallacies.
7. Use proof techniques to verify a computational claim and communicate assumptions clearly.

1. Propositions and Logical Connectives

A proposition is a declarative statement that is either true or false, but not both. The truth value of a proposition is commonly denoted by T or F.

Examples include:

• “7 is a prime number.” This is true.
• “10 < 4.” This is false.
• “The program terminates on input x.” This may be a proposition if the program and input are specified precisely.

Questions, commands, and expressions containing unspecified variables are not propositions. “Is the server available?” is a question. “Close the file” is a command. “x + 2 = 5” is an open sentence until a value or domain for x is supplied.

A proposition represented by a letter such as p or q is called an atomic proposition. Larger propositions are formed using logical connectives.

The conjunction p ∧ q is true only when both p and q are true. The inclusive disjunction p ∨ q is true when at least one of p and q is true. In ordinary mathematical logic, “or” is normally inclusive unless explicitly stated otherwise.

The implication p → q is false only when p is true and q is false. It is often read as “p is sufficient for q” or “q is necessary for p.” Its reverse, q → p, is the converse and is not generally equivalent to p → q. The proposition ¬p → ¬q is the inverse. The contrapositive is ¬q → ¬p, and it is logically equivalent to p → q.

Truth tables

A truth table lists the truth value of a compound proposition for every possible combination of its components.

The implication row in which p is false may initially seem unintuitive. In formal logic, p → q asserts that no case occurs in which p is true and q is false. If p is false, that prohibited case has not occurred, so the implication is true. This convention is essential in mathematics and computer science, especially when a precondition is not satisfied.

A proposition that is true for every possible assignment of truth values is a tautology. A proposition that is always false is a contradiction. A proposition that is true for some assignments and false for others is contingent.

Two propositions are logically equivalent, written p ≡ q, if they have the same truth value for every assignment. Important equivalences include:

These are De Morgan’s laws. Other useful laws are:

The first equivalence is particularly useful because it transforms implication into a combination of negation and disjunction.

Worked example: simplifying a specification

Suppose a system requirement is “The request is rejected if it is unauthenticated or malformed.” Let a mean “the request is authenticated” and m mean “the request is well formed.” Rejection is represented by:

By De Morgan’s law:

Thus, rejection is equivalent to saying that it is not the case that the request is both authenticated and well formed. This reformulation can help when implementing a security check, although implementation must still reflect the intended policy and not merely a syntactic transformation.

2. Predicates and Quantifiers

A predicate is a statement involving one or more variables whose truth depends on the values assigned to those variables. For example, P(x): “x is even” is a predicate over the integers. Once x is assigned a value, P(x) becomes a proposition.

The set from which a variable is drawn is its domain. Domain specification is essential. The predicate x² ≥ 0 is true over the real numbers, while a predicate involving divisibility may conventionally be defined over the integers.

The universal quantifier, ∀, means “for every” or “for all.” The existential quantifier, ∃, means “there exists at least one.” For a predicate P over domain D:

states that P(x) is true for every x in D, whereas

states that P(x) is true for at least one x in D.

The order of quantifiers matters. The statement

is true over the integers: for every integer x, one can choose y = x + 1. By contrast,

is false over the integers because no single integer is greater than every integer.

Negation changes a universal quantifier into an existential quantifier and vice versa:

For example, the negation of “Every submitted program passes the test” is not “Every submitted program fails the test.” It is “At least one submitted program does not pass the test.”

Free and bound variables

A variable is bound when it lies within the scope of a quantifier. It is free otherwise. A formula with free variables is generally a predicate, not a proposition. In formal specifications, unintended free variables can create ambiguity and should be eliminated by explicitly defining domains and quantification.

3. Inference and Valid Arguments

An argument consists of premises and a conclusion. It is valid when the conclusion must be true whenever all premises are true. Validity concerns structure, not whether the premises happen to be true in the real world. An argument is sound when it is valid and all its premises are true.

A central inference rule is modus ponens:

For example:

1. If a file is encrypted, unauthorized readers cannot interpret its contents.
2. This file is encrypted.
3. Therefore, unauthorized readers cannot interpret its contents.

Another valid rule is modus tollens:

Other useful rules include:

• Hypothetical syllogism: p → q and q → r imply p → r.
• Disjunctive syllogism: p ∨ q and ¬p imply q.
• Conjunction: p and q imply p ∧ q.
• Simplification: p ∧ q implies p.
• Universal instantiation: ∀x P(x) implies P(a), for an element a in the domain.
• Existential generalization: P(a) implies ∃x P(x), provided a belongs to the domain.

Validity and fallacies

Two frequent invalid patterns are:

Affirming the consequent

This is invalid. A system may be slow because of insufficient memory, but slowness does not prove insufficient memory.

Denying the antecedent

This is also invalid. If a number is divisible by 4, it is even; not being divisible by 4 does not imply that it is odd, since 6 is even but not divisible by 4.

A converse error occurs when p → q is treated as q → p. A circular argument assumes, directly or indirectly, the conclusion that it is supposed to prove. An argument from authority substitutes the status of a person for evidence. In technical work, a claim must be supported by definitions, data, or a valid derivation rather than confidence or reputation.

4. Methods of Proof

A proof is a logically connected sequence of statements establishing a conclusion from definitions, previously proved results, and accepted assumptions. A proof should make its domain, assumptions, and conclusion explicit.

Direct proof

To prove an implication p → q directly, assume p and derive q using valid steps.

Example. Prove that the sum of two even integers is even.

Let m and n be even integers. By definition, there exist integers a and b such that m = 2a and n = 2b. Therefore,

Since a + b is an integer, m + n is even. The proof depends on the definition of evenness and the closure of integers under addition.

Constructive proof

A constructive proof of an existential statement provides an explicit object and verifies its required property.

Example. Prove that there exists an integer whose square is 16. Choose x = 4. Then x² = 4² = 16, so the required integer exists. The example is simple, but the same method is important in algorithms: a constructive existence proof often yields a procedure for producing a solution.

For instance, to prove that every finite nonempty set of integers has a least element, one may constructively examine its elements and retain the smallest encountered value. The proof and the algorithm reflect the same finite-search principle.

Proof by contraposition

Because p → q is logically equivalent to ¬q → ¬p, an implication can be proved by assuming ¬q and deriving ¬p.

Example. Prove: if n² is even, then n is even.

The contrapositive is: if n is not even, then n² is not even. If n is odd, n = 2k + 1 for some integer k. Then

Thus n² is odd, so it is not even. Therefore the original implication is true.

Contraposition is especially effective when the negation of the conclusion has a simple structure.

Proof by contradiction

To prove a proposition P by contradiction, assume ¬P and derive a contradiction, such as a statement of the form R ∧ ¬R. The method relies on the principle that a proposition and its negation cannot both be true within a consistent logical system.

Example. Prove that √2 is irrational. Assume, for contradiction, that √2 = a/b where a and b are integers, b ≠ 0, and the fraction is in lowest terms. Squaring gives a² = 2b², so a² is even. Hence a is even; write a = 2k. Substitution gives 4k² = 2b², so b² = 2k², making b even. Both a and b are even, contradicting that a/b was in lowest terms. Therefore √2 is irrational.

Contradiction is powerful, but the assumed negation must be stated accurately. A proof can fail if it derives only an unlikely result rather than a genuine logical contradiction.

Proof by cases

If a domain can be divided into exhaustive cases, prove the conclusion separately in each case. For example, every integer is even or odd. To prove a property for all integers, one may handle the even and odd cases independently. The cases must cover every possibility and should not introduce hidden overlap problems.

5. Mathematical Induction

Mathematical induction proves a statement for every integer n ≥ n₀ by establishing:

1. Base case: the statement is true for n = n₀.
2. Inductive hypothesis: assume it is true for an arbitrary integer k ≥ n₀.
3. Inductive step: use that assumption to prove it is true for k + 1.

The conclusion follows because truth is transferred from the base case to each successive integer.

Worked example: sum of the first n positive integers

Prove that for every integer n ≥ 1,

Base case: When n = 1, the left side is 1 and the right side is 1(2)/2 = 1.

Inductive hypothesis: Assume for an arbitrary k ≥ 1 that

Inductive step: Add k + 1 to both sides:

Factor the right side:

This is the required formula with n = k + 1. Therefore the statement holds for all n ≥ 1.

Strong induction

In strong induction, the inductive step assumes the statement is true for every integer from n₀ through k, then proves it for k + 1. Strong induction is useful when the next case depends on several earlier cases rather than only the immediately preceding one.

For algorithm analysis, induction often proves loop invariants, recursive properties, and bounds on running time. The base case must correspond to the smallest input handled by the algorithm, and the induction step must reflect the actual recursive or iterative structure.

6. Logic in Program Verification

A program specification commonly uses:

• Precondition: what must be true before execution.
• Postcondition: what must be true after execution.
• Invariant: a property that remains true at selected points, especially throughout a loop.

Consider the following pseudocode for finding the maximum of a nonempty array A of length n:

m := A[0]
for i := 1 to n − 1 do
    if A[i] > m then
        m := A[i]
return m

A suitable loop invariant after processing positions 0 through i − 1 is:

m equals the maximum value among A[0], A[1], …, A[i − 1].

Initialization: Before the first iteration, i = 1 and m = A[0], so the invariant holds.

Maintenance: Assume the invariant holds at the start of an iteration. If A[i] > m, assignment makes m = A[i], the maximum of all processed values. Otherwise m already equals or exceeds A[i], so it remains the maximum. The invariant is preserved.

Termination: When the loop ends, i = n. The invariant states that m is the maximum of A[0] through A[n − 1]. Thus the postcondition is satisfied.

The proof also depends on the precondition that the array is nonempty. Without it, A[0] is undefined and the algorithm is not correct as written.

7. Applied Case: Verifying a Duplicate-Detection Claim

This is an illustrative case. A software team claims that the following algorithm correctly determines whether an array contains duplicate values:

for i := 0 to n − 1 do
    for j := i + 1 to n − 1 do
        if A[i] = A[j] then return true
return false

Background and problem

The algorithm must return true exactly when there exist indices i and j such that 0 ≤ i < j < n and A[i] = A[j]. The team needs a proof, not only test results.

Analysis

The algorithm examines every unordered pair of distinct positions exactly once. The outer loop chooses i, and the inner loop compares A[i] with every position j greater than i. Therefore every pair i < j is examined.

Correctness argument

If the algorithm returns true, it has found indices i < j with A[i] = A[j]. Hence a duplicate exists.

Conversely, suppose a duplicate exists. Then there are positions r and s with r < s and A[r] = A[s]. Since the nested loops examine the pair (r, s), they eventually test this equality and return true. Therefore, if the algorithm returns false, no duplicate pair exists.

Thus the algorithm is correct under the assumption that array indexing and equality comparison behave as specified.

Complexity observation

The number of comparisons is

for an input of length n. Therefore the worst-case running time is Θ(n²), assuming each equality comparison takes constant time. The formula applies to the comparison count; actual elapsed time may differ because of memory, language, hardware, and early termination.

Outcome and learning points

The proof separates two directions: returning true implies a duplicate, and a duplicate implies returning true. This two-way structure is typical of correctness proofs. It also shows that correctness and efficiency are different claims: an algorithm may be correct but slower than an alternative using a hash set, whose expected running time is often Θ(n) under standard hashing assumptions and whose worst-case behavior depends on the hash-table implementation.

8. Limitations, Assumptions, and Responsible Reasoning

Formal proofs are only as reliable as their definitions and assumptions. A proof about an ideal integer model may not directly establish correctness under fixed-width machine arithmetic, where overflow is possible. A proof assuming exact equality may not apply to floating-point calculations, where rounding and representation error matter. A proof about a sequential program may not apply to concurrent execution, where interleavings and race conditions introduce additional behaviors.

In software and AI systems, formal reasoning should therefore document:

• the input domain and exceptional cases;
• preconditions, postconditions, and environmental assumptions;
• the meaning of equality, ordering, and arithmetic operations;
• termination assumptions and resource limits;
• whether probabilistic or approximate behavior is being analyzed.

Formal verification can establish that a system satisfies a specification, but it cannot determine whether the specification expresses the right social, safety, privacy, or business goal. Ethical review, testing, threat modeling, and stakeholder analysis remain necessary. For high-impact systems, a proof of implementation correctness does not by itself justify deployment.

Best Practices for Mathematical and Computational Proofs

1. Define every variable, domain, and assumption before reasoning.
2. Distinguish implication from equivalence; proving one direction is not enough for “if and only if.”
3. Use counterexamples to disprove universal claims.
4. Check boundary cases, including empty inputs and the smallest permitted values.
5. Separate correctness, termination, and complexity arguments.
6. Avoid relying on examples as evidence of a universal statement.
7. State whether arithmetic is mathematical integer arithmetic or machine arithmetic.
8. In induction, prove the base case and connect the exact inductive hypothesis to the next case.
9. In quantified statements, verify the order and scope of quantifiers.
10. Communicate proofs in a sequence that another reader can independently verify.

Chapter Summary

Mathematical logic gives computer science a precise framework for representing and evaluating claims. Propositions have truth values, while predicates become propositions when variables are assigned values or quantified. Connectives form compound statements, and truth tables establish tautologies, contradictions, and logical equivalences. Implication is directional; its contrapositive is equivalent, but its converse and inverse generally are not.

Quantifiers express universal and existential claims, and their order can change meaning. Negating a quantified statement reverses the quantifier and negates the predicate. Valid inference rules, including modus ponens and modus tollens, support reliable derivations, whereas affirming the consequent and denying the antecedent are common fallacies.

Direct proof, constructive proof, contraposition, contradiction, proof by cases, and induction provide complementary strategies. Induction is especially valuable for recursive algorithms, loop invariants, and claims indexed by the integers. Program verification uses preconditions, postconditions, and invariants to prove that an implementation meets its specification. Finally, every proof depends on explicit assumptions, and correctness must be distinguished from efficiency, safety, and suitability for deployment.

Key Terms

Proposition: A declarative statement that is either true or false.

Predicate: A statement involving variables whose truth depends on assigned values.

Domain: The set of values from which quantified variables are drawn.

Negation: The logical operation that reverses a proposition’s truth value.

Conjunction: A compound proposition formed with “and.”

Disjunction: A compound proposition formed with inclusive “or.”

Implication: A proposition of the form p → q.

Biconditional: A proposition asserting that two propositions imply each other.

Tautology: A proposition true under every assignment of truth values.

Contradiction: A proposition false under every assignment of truth values.

Logical equivalence: Equality of truth values for all assignments.

Universal quantifier: The symbol ∀, meaning “for every.”

Existential quantifier: The symbol ∃, meaning “there exists.”

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

Contrapositive: The proposition ¬q → ¬p associated with p → q.

Constructive proof: A proof that explicitly produces an object satisfying a property.

Mathematical induction: A proof method using a base case and an inductive step.

Loop invariant: A property preserved during successive loop iterations.

Precondition: A requirement that must hold before a computation begins.

Postcondition: A property guaranteed after a computation finishes.

Review Questions

Short Answer Questions

1. What distinguishes a proposition from a predicate?
2. State the contrapositive of p → q.
3. What is the difference between a valid argument and a sound argument?
4. State the two logical laws used to negate universal and existential quantifiers.
5. What are the three principal components of a proof by mathematical induction?

Long Answer Questions

1. Construct a truth table for (p ∧ q) → p and explain why the result is a tautology.
2. Explain De Morgan’s laws and illustrate each with a quantified or computational example.
3. Prove directly that the product of two odd integers is odd.
4. Prove by contraposition that if n² is odd, then n is odd, for an integer n.
5. Explain how loop invariants establish the correctness of an iterative algorithm.

Analytical / Application Questions

1. A system claims: “If a request is authorized, it is logged. This request is logged; therefore, it is authorized.” Identify the logical fallacy and provide a plausible alternative explanation.
2. Design a precondition, loop invariant, and postcondition for an algorithm that computes the sum of all elements in a nonempty integer array. Explain initialization, maintenance, and termination.
3. A developer claims that testing an algorithm on one million inputs proves it works for every input. Evaluate this claim using the distinction between empirical evidence, counterexamples, and formal proof.

Multiple Choice Questions with Answers

Question 1

Which statement is a proposition?

A. Close the application.

B. Is the value valid?

C. 17 is a prime number.

D. x + 1 = 4.

Correct Answer: C. 17 is a prime number.

Question 2

Which expression is logically equivalent to p → q?

A. p ∧ q

B. ¬p ∨ q

C. p ∨ ¬q

D. ¬p ∧ q

Correct Answer: B. ¬p ∨ q

Question 3

What is the contrapositive of p → q?

A. q → p

B. ¬p → ¬q

C. ¬q → ¬p

D. p → ¬q

Correct Answer: C. ¬q → ¬p

Question 4

Which argument form is valid?

A. p → q, q, therefore p

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

C. p → q, p, therefore q

D. p ∨ q, q, therefore ¬p

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

Question 5

What is the negation of ∀x P(x)?

A. ∀x ¬P(x)

B. ∃x ¬P(x)

C. ∃x P(x)

D. ¬∃x ¬P(x)

Correct Answer: B. ∃x ¬P(x)

Question 6

In a direct proof of p → q, what is normally assumed first?

A. ¬p

B. ¬q

C. p

D. q

Correct Answer: C. p

Question 7

What must be established in the base case of mathematical induction?

A. The statement is false for the smallest value.

B. The statement is true for the initial value.

C. The inductive hypothesis is unnecessary.

D. All later cases are tested experimentally.

Correct Answer: B. The statement is true for the initial value.

Question 8

For an array of length n, how many pair comparisons does the duplicate-detection algorithm make in the worst case?

A. n

B. n²

C. n(n − 1)/2

D. 2n

Correct Answer: C. n(n − 1)/2

Question 9

Which fallacy has the form p → q, q, therefore p?

A. Denying the antecedent

B. Affirming the consequent

C. Circular reasoning

D. Modus tollens

Correct Answer: B. Affirming the consequent

Question 10

What is the role of a loop invariant?

A. To guarantee that a program uses no memory

B. To state a property preserved during loop execution

C. To replace the program’s precondition

D. To prove every possible program terminates

Correct Answer: B. To state a property preserved during loop execution