Logic, quantifiers, and specifications

An application should allow an administrator to open a record, or allow its owner when the owner has approval. A developer writes (admin or owner) and approved. Another writes admin or (owner and approved). Both versions look plausible; an administrator without approval receives different answers. Which matches the requirement? You need to settle the meaning before inspecting the implementation.

Logic gives a language for that conversation. Its job here is to expose exactly which circumstances make a statement true, what its variables range over, and what evidence would establish or refute it. The same skills help read claims about algorithms and AI: “every input,” “there exists a model,” and “the model succeeds on this sample” describe different obligations. Changing one phrase can change the entire claim.

Retrieval check: explain why a function’s domain belongs in its definition and why one valid counterexample refutes a universal identity. Use Module 01 if either point is unclear. We assume ordinary classical, two-valued logic: each proposition under a specified interpretation is either true or false. Database nulls, exceptions, unknown information, and probabilistic uncertainty require additional modelling; they are not a third truth value silently inserted into these tables.

A proposition is a declarative statement with a definite truth value in the setting being discussed. “Seven is odd” is true. “Seven is even” is false. A false statement remains a proposition. “Please open the file” is a command, while “is the file open?” is a question. Neither is assigned a truth value in this propositional language. “The file is open” becomes a proposition once the file and observation time are fixed.

Letters such as $p$ and $q$ stand for propositions. A valuation assigns a truth value to each letter. The sentence represented by a formula and the current truth assignment are distinct: a formula may be true under one valuation and false under another. Evaluating a formula means applying the connective definitions to the assigned inputs. Proving two formulas equivalent means that they have the same output under every valuation.

Negation $\neg p$ reverses the truth value. Conjunction $p\land q$ is true exactly when both inputs are true. Disjunction $p\lor q$ is true when at least one input is true. Mathematical “or” is inclusive: the case in which both are true is allowed. An exclusive alternative needs its own expression, such as $(p\lor q)\land\neg(p\land q)$. English sometimes uses “or” exclusively, so a specification should remove that ambiguity rather than assume its intended meaning.

A truth table lists all possible valuations. With two distinct proposition letters there are four rows; with three there are eight. You do not need to know which row occurs in a particular application to establish an identity across the table. Conversely, inspecting only the row occurring today cannot establish that two rules will always agree. The missing rows may include the very circumstance a policy was written to handle.

Parentheses communicate structure. The administrator rule is $a\lor(o\land r)$, where $a$ means administrator, $o$ means owner, and $r$ means approved. Its outer connective is disjunction. The alternative $(a\lor o)\land r$ has an outer conjunction and requires approval in every successful case. Standard precedence gives negation before conjunction before disjunction, but explicit parentheses make requirements easier to review. A change in structure may change truth values even when the same letters appear.

Negation of a compound statement must account for every way it can fail. “Both checks pass” fails if either check fails; “at least one check passes” fails only if both checks fail. These give De Morgan’s laws:

Here $\equiv$ denotes logical equivalence between formulas, rather than the equality of two numbers. Verify the four rows, then explain the laws in words. This connects the mechanical check to their meaning.

In Python, Boolean not, and, and or agree with these definitions when their inputs are Boolean values. Python also permits other objects: and and or can return an operand rather than a bool. For example, "ready" or "" returns "ready". Keep the logical model separate from those language details. A truth-table lab uses actual True and False inputs, so its correspondence is explicit.

The implication $p\Rightarrow q$ says that whenever the antecedent $p$ is true, the consequent $q$ must be true. It rules out exactly one situation: $p$ true with $q$ false. Thus its truth-table definition is $\neg p\lor q$. This is material implication. It does not assert that $p$ causes $q$, that the two events occur in chronological order, or that $p$ actually occurs. Those are additional claims that need their own models.

Consider “if a request is approved, it has a reviewer.” Let $p$ mean approved and $q$ mean has a reviewer. An unapproved request does not violate the rule regardless of whether it has a reviewer. The rule promises something only in the approved case. This explains the true rows with false antecedents. They are often called vacuously true. The word is a reminder that the promise was not activated, rather than a claim that a reviewer was found.

An implication and its converse need not agree. Being divisible by four implies being even, but being even does not imply being divisible by four: six is a counterexample. The inverse is $\neg p\Rightarrow\neg q$. It need not agree with the original either. The contrapositive is $\neg q\Rightarrow\neg p$, and it is equivalent to the original. Expanding both as disjunctions gives $\neg p\lor q$ and $q\lor\neg p$, equal under every valuation.

The phrase “$p$ is sufficient for $q$” means $p\Rightarrow q$: knowing $p$ holds is enough to establish $q$ under the rule. “$q$ is necessary for $p$” means the same implication: $p$ cannot hold without $q$. A necessary condition may fail to be sufficient. A reviewer may be required for approval while a reviewer alone does not guarantee approval. Reversing the direction would introduce a stronger and possibly false policy.

“$p$ only if $q$” translates to $p\Rightarrow q$, because it makes $q$ necessary for $p$. “$p$ if $q$” translates to $q\Rightarrow p$, because it makes $q$ sufficient for $p$. “$p$ if and only if $q$” requires both directions and is written $p\Leftrightarrow q$. Its truth value is true exactly when the two inputs agree. A specification defining acceptance often needs equivalence, while a rule giving just one guarantee may need implication.

Two familiar reasoning patterns follow. From $p$ and $p\Rightarrow q$, conclude $q$; this is modus ponens. From $\neg q$ and $p\Rightarrow q$, conclude $\neg p$; this is modus tollens. Knowing $q$ alone does not let you conclude $p$, and knowing $\neg p$ alone does not let you conclude $\neg q$. Each invalid pattern can be exposed by a row of the implication table.

Suppose passing a particular check guarantees a valid record. Observing a valid record does not prove that the check ran: another process may have validated it. Observing that the check did not run does not prove the record invalid. These are logical limitations independent of how reliable the implementation is. When reading an AI result, a sufficient condition in a theorem must not be silently converted into a necessary explanation of observed success.

A predicate is a statement template whose truth value depends on its inputs. “$x$ is even” is not a closed proposition until $x$ is supplied or bound by a quantifier. Write $P(x)$ and declare a domain, such as $x\in\mathbb{Z}$. The same notation with real inputs would require an explicit meaning for “even”; familiar integer words do not automatically extend to all number systems.

A variable appearing outside a binding operation is free. Substituting $x=6$ in $P(x)$ creates a definite statement. Another way to close the formula is to quantify it. The universal statement $\forall x\in D,\ P(x)$ means that every element of the declared domain satisfies the predicate. The existential statement $\exists x\in D,\ P(x)$ means that at least one element does. These symbols describe obligations, not loops whose execution proves every possible domain.

To establish an existential statement constructively, exhibit a witness and show that it lies in the domain and satisfies the predicate. To refute a universal statement, exhibit a counterexample with the same two obligations. Domain membership matters in both cases. A negative integer cannot refute a claim restricted to nonnegative integers, and a fractional solution cannot witness existence in the integers.

For a finite domain, universality can be checked by inspecting every member and existence by searching until a witness appears. Over an infinite domain, a finite successful search cannot settle universality. An existential statement can still be settled by one valid witness even when the domain is infinite. This asymmetry is useful: finding an integer solution establishes existence, while not finding one in a particular range does not establish nonexistence over all integers.

The truth of a universal statement over an empty domain is true under this logic. There is no member that violates it. An existential statement over that domain is false because there is no possible witness. Python’s all([]) and any([]) follow exactly these conventions. An empty catalogue passing a universal quality rule does not demonstrate that any useful records exist. If existence is part of a requirement, state it as a separate conjunct.

Domain-restricted statements can be expanded into statements over a larger universe. “Every approved request has a reviewer” is $\forall r,\ A(r)\Rightarrow H(r)$. “Some approved request has a reviewer” is $\exists r,\ A(r)\land H(r)$. Restriction behaves differently for universals and existentials. Using implication in the second expression would allow an unapproved request to witness the statement merely because its antecedent is false.

Constants and function inputs also need scope. The predicate $x>t$ can be quantified over $x$ while leaving threshold $t$ free. Then $\forall x\in D,\ x>t$ is a statement depending on the selected threshold. A training claim with a fixed dataset or a fixed model similarly depends on those choices unless it quantifies over them. “For this model” and “for every model” should not be treated as stylistic variants.

For practical specifications, write a short domain declaration alongside each predicate: requests in this catalogue, reviewers registered at this time, integer positions from zero through length minus one. This prevents a true statement about a small catalogue being read as a promise about future entries. It also explains what a stored Boolean table represents and which omitted cases remain outside its scope.

Many requirements relate two kinds of objects. Write $R(r,v)$ for “reviewer $v$ is approved to review request $r$,” with request domain $D$ and reviewer domain $V$. The statement $\forall r\in D\ \exists v\in V,\ R(r,v)$ means each request has at least one suitable reviewer. The chosen reviewer may depend on the request. It does not require a single person able to handle them all.

In $\exists v\in V\ \forall r\in D,\ R(r,v)$, one reviewer is selected before considering all requests. That reviewer must work for every request. This statement is generally stronger. If it holds, each request can use the common reviewer, so the first statement holds. The converse can fail when different requests require different reviewers. Nested quantifiers expose exactly which choices may depend on earlier choices.

Order can also change statements over infinite domains. On integers, $\forall x\exists y,\ y=x+1$ is true: given $x$, choose $y=x+1$. The reversed $\exists y\forall x,\ y=x+1$ is false. If one $y$ worked for every $x$, it would equal one when $x=0$ and two when $x=1$, an impossibility. This is an argument over the declared infinite domain, rather than an extrapolation from sampled integers.

Two universal quantifiers can swap order when the predicate and fixed domains stay the same: both orders require every pair to satisfy it. Two existential quantifiers can also swap, since both seek one successful pair. These observations do not license arbitrary reordering of mixed quantifiers. If a domain depends on an earlier variable, inspect that dependence before applying any swapping rule.

Negation of a universal is existential negation, and negation of an existential is universal negation:

The first says a universal rule fails because some member violates it. The second says existence fails because every candidate fails. Apply these rules from the outside in, preserving order. Negating $\forall r\exists v\ R(r,v)$ gives $\exists r\forall v\ \neg R(r,v)$: there is a request with no suitable reviewer. It does not say all requests lack all reviewers, which would be a much stronger statement.

Quantified implications also need connective negation. Since $\neg(p\Rightarrow q)\equiv p\land\neg q$, negating “every approved request has a reviewer” gives “there exists an approved request without a reviewer.” The approval condition remains positive. Simply putting “not” into the conclusion while leaving the universal quantifier unchanged fails to describe all ways the original rule could be false.

Scope can be made visible by parentheses and by speaking the formula aloud. In $\forall x\in D,\ (P(x)\Rightarrow Q(x))$, both uses of $x$ are bound. Writing an existential inside an implication changes what depends on the antecedent, so do not remove parentheses as cosmetic punctuation. Renaming a bound variable consistently does not change meaning; changing its domain or moving a quantifier does.

A program contract connects an allowed starting state to a promised finishing state. A precondition states what must be true before a call. A postcondition states what the result must satisfy when the call finishes under that precondition. “If the precondition holds and the program terminates, then the postcondition holds” is a partial-correctness claim. A total-correctness claim additionally establishes termination for every allowed input. Formal proofs of those obligations come in Module 04.

The precondition should describe real assumptions rather than hide troublesome valid cases. For an integer division operation, a nonzero divisor is appropriate. For a search returning the first occurrence of a target in a finite list, it would be misleading to require that the first element is already the target just to avoid analysing the loop. A narrower domain can be legitimate, but its restriction should match the operation the caller needs.

Suppose a search returns an integer $j$ on list $a$ of length $n$ with target $t$. A precise postcondition is:

The first branch means absence; the second means the returned position is valid, matches, and has no earlier match. Requiring $a_j=t$ alone would not establish first occurrence and would not describe absence. Domain restrictions also prevent out-of-range indexing from being treated as a meaningful mathematical test. In executable code, use short-circuit guards before indexing.

An assertion is a statement expected to hold at a specified program point. It can be used as executable feedback during development. An assertion after a function call may check part of a postcondition; an assertion inside a loop may check a proposed invariant on the particular execution. Passing these checks is useful evidence but does not prove the invariant for every execution. A formal argument must cover all states reachable under the assumptions.

A predicate about state needs an observation point. “Everything before position $i$ has been checked” might hold at the start of an iteration, while “position $i$ has also been checked” may hold at the end. Moving an assertion across an update without adjusting its statement can introduce an off-by-one error. The relationship between the predicate, the index domain, and the line of code is part of its meaning.

Not all software conditions belong in assert. Python can disable assertions in optimised mode, so explicit input validation should use ordinary conditionals and exceptions when a caller must receive a reliable rejection. This distinction does not change logical semantics; it changes whether a statement is enforced by a particular runtime configuration. Our labs use assertions to catch internal disagreement and explicit code where an input-domain check is part of the contract.

Specifications can describe implications without requiring their antecedents ever to occur. “If training finishes, save a report” says nothing about whether training finishes. “If a record is accepted, its checksum is valid” says nothing about whether valid records are accepted. To specify exact acceptance, write an equivalence. To specify completion, add a termination obligation. To specify at least one accepted record, add existence. Separating the promises makes a review more precise.

A contract also identifies what is intentionally outside the model. A finite Boolean approval table says nothing about who may edit the table, when permissions expire, or how identity is verified. Those questions need additional state and predicates. Precision about one small rule is useful without being a complete security design. Likewise a theorem about a fixed data-generating assumption does not settle whether an actual dataset satisfies that assumption.

A propositional formula is satisfiable if at least one valuation makes it true. It is valid, or a tautology, if every valuation makes it true. It is unsatisfiable if no valuation makes it true. A formula can be satisfiable without being valid: $p\land q$ succeeds in one of its four rows and fails in three. A contradiction such as $p\land\neg p$ succeeds in none.

These words describe different quantifiers over the valuations. For a fixed formula with finitely many proposition letters, its complete truth table is finite. Exhausting that table can establish validity for the propositional formula, because every valuation in its domain was checked. It can also establish satisfiability by finding one row, or unsatisfiability by finding no successful row after complete enumeration.

This is stronger than checking a few integer inputs for an unrestricted arithmetic identity. The distinction concerns whether the entire declared domain has been exhausted, not whether a computer was used. An infinite integer domain cannot be exhausted by checking a finite interval. A finite catalogue can be exhausted, but its conclusion concerns that catalogue unless a separate argument connects it to a larger setting.

Logical consequence means that every valuation satisfying the premises also satisfies the conclusion. Premises $p$ and $p\Rightarrow q$ entail $q$, since a row making both premises true cannot make $q$ false. If the premises are inconsistent, there is no satisfying row, so the entailment is vacuously true in classical logic. That does not make an inconsistent specification useful: no implementation can satisfy all its demands simultaneously.

When checking a specification, ask both whether its constraints are satisfiable and whether the desired conclusion follows. “Approved records must be reviewed” and “no record may be reviewed,” combined with “some record is approved,” are inconsistent. Dropping the existence requirement makes them satisfiable by approving nothing. That repair may violate the product requirement even though the logical rules no longer contradict one another.

Finite model checking treats a defined finite collection of objects and states as a model. It can identify a state or pair of objects that violates a requirement. A returned counterexample is often more informative than a Boolean failure: it tells you which domain values trigger the disagreement. Preserve the witness, reproduce it, explain the relevant formula, and decide whether the code or the intended rule needs correction.

Enumeration has practical limits. A table with $m$ independent Boolean inputs contains $2^m$ valuations. Exhaustive checking is excellent for a small rule but rapidly expensive as inputs increase. More advanced solving methods can exploit structure; they still need a faithful specification. Sampling is useful for larger systems, but it must be reported as sampling rather than a complete validity check. Probability of passing a sampled test is also a different claim from universal truth.

In an AI setting, “every tested input was classified correctly” quantifies over the test collection. “Every possible future input will be classified correctly” quantifies over another, usually much larger domain. The second does not follow from the first merely by changing the word “tested.” Statistical arguments can support probabilistic conclusions under sampling assumptions; later modules will study those assumptions. Logic makes the gap visible before statistics tries to quantify it.

Run the scripts with Python 3.11 or later, using python filename.py or py filename.py on Windows and python3 filename.py where needed. Download to one directory and run from a terminal. See the Python primer for setup. These labs require no packages. Predict the critical row before execution, preserve its inputs, and explain why the output follows from the formula. Each lab explanation earns up to ten points: prediction 3, interpretation 4, and fault or variation analysis 3.

Forty minutes: first write the four valuations for two Boolean inputs. Predict the implication and converse columns, then run the script. It checks the contrapositive and both De Morgan laws in all rows. Explain why this complete enumeration proves their propositional equivalence, and why it does not prove an unrelated arithmetic theorem. Change the implication implementation to p and q; preserve a disagreeing valuation and repair it. The non-Boolean Python example at the end is a language distinction, not an extra truth value.

Download lab1_truth_tables.py

"""Enumerate Boolean valuations; establish only the displayed equivalences."""
from itertools import product


def implies(p, q):
    return (not p) or q


def main():
    print("p q | not p | p and q | p or q | p -> q | q -> p")
    for p, q in product((False, True), repeat=2):
        values = (p, q, not p, p and q, p or q, implies(p, q), implies(q, p))
        print(" ".join(str(int(v)) for v in values))
        assert implies(p, q) == implies(not q, not p)
        assert (not (p and q)) == ((not p) or (not q))
        assert (not (p or q)) == ((not p) and (not q))
    print("Contrapositive and both De Morgan laws: all 4 valuations agree.")
    print("Converse mismatch at p=False, q=True:", implies(False, True), implies(True, False))
    print("Python non-Boolean example: 'ready' or '' =", repr("ready" or ""))


if __name__ == "__main__":
    main()

p q | not p | p and q | p or q | p -> q | q -> p
0 0 1 0 0 1 1
0 1 1 0 1 1 0
1 0 0 0 1 0 1
1 1 0 1 1 1 1
Contrapositive and both De Morgan laws: all 4 valuations agree.
Converse mismatch at p=False, q=True: True False
Python non-Boolean example: 'ready' or '' = 'ready'

Forty minutes: use $P(x,y)$ meaning $y=x+1$. Predict the per-input witnesses and common witnesses over the two displayed catalogues. Reducing the second domain removes the witness for $x=1$; identify that failure before running. Explain the three empty-domain cases rather than memorising their outputs. Change the predicate to $y\ge x$ and predict whether the larger catalogue contains a common witness. State the domain in every conclusion; the script does not enumerate all integers.

Download lab2_quantifiers.py

"""Witnesses over an explicitly finite catalogue, including empty domains."""


def investigate(xs, ys):
    predicate = lambda x, y: y == x + 1
    per_x = {x: [y for y in ys if predicate(x, y)] for x in xs}
    common = [y for y in ys if all(predicate(x, y) for x in xs)]
    every_has_some = all(any(predicate(x, y) for y in ys) for x in xs)
    some_for_every = any(all(predicate(x, y) for x in xs) for y in ys)
    negation = any(all(not predicate(x, y) for y in ys) for x in xs)
    assert negation == (not every_has_some)
    return per_x, common, every_has_some, some_for_every


def main():
    xs = (-1, 0, 1)
    for ys in ((-2, -1, 0, 1, 2), (-1, 0, 1)):
        witnesses, common, forall_exists, exists_forall = investigate(xs, ys)
        print("X =", xs, "Y =", ys)
        print("Per-input witnesses:", witnesses)
        print("Common witnesses:", common)
        print("forall x exists y:", forall_exists, "exists y forall x:", exists_forall)
    for xs, ys in (((), (0,)), ((0,), ()), ((), ())):
        result = investigate(xs, ys)
        print("Empty case X =", xs, "Y =", ys, "results:", result[2:])
    print("These checks concern these catalogues, not all integers.")


if __name__ == "__main__":
    main()

X = (-1, 0, 1) Y = (-2, -1, 0, 1, 2)
Per-input witnesses: {-1: [0], 0: [1], 1: [2]}
Common witnesses: []
forall x exists y: True exists y forall x: False
X = (-1, 0, 1) Y = (-1, 0, 1)
Per-input witnesses: {-1: [0], 0: [1], 1: []}
Common witnesses: []
forall x exists y: False exists y forall x: False
Empty case X = () Y = (0,) results: (True, True)
Empty case X = (0,) Y = () results: (False, False)
Empty case X = () Y = () results: (True, False)
These checks concern these catalogues, not all integers.

Forty minutes: compare the intended administrator exception with the faulty parenthesisation. Predict how many of the eight rows disagree, run the script, and explain why both disagreements have an administrator and no approval. The repair is checked on the complete Boolean domain. The final catalogue repeats the distinction between local and common reviewers; explain why it is another specification question rather than a failure of Boolean evaluation.

Download lab3_access_rule.py

"""Find all counterexamples to a changed parenthesisation of an access rule."""
from itertools import product


def intended(admin, owner, approved):
    return admin or (owner and approved)


def faulty(admin, owner, approved):
    return (admin or owner) and approved


def main():
    print("Rule: admin OR (owner AND approved)")
    mismatches = []
    for admin, owner, approved in product((False, True), repeat=3):
        want = intended(admin, owner, approved)
        got = faulty(admin, owner, approved)
        if want != got:
            mismatches.append((admin, owner, approved))
            print(f"admin={admin}, owner={owner}, approved={approved}: expected={want}, faulty={got}")
        repaired = admin or (owner and approved)
        assert repaired == want
    assert mismatches == [(True, False, False), (True, True, False)]
    print("Repair agrees on all 8 Boolean valuations.")
    requests = ("r1", "r2")
    reviewers = ("a", "b")
    approved_pairs = {("r1", "a"), ("r2", "b")}
    per_request = all(any((r, v) in approved_pairs for v in reviewers) for r in requests)
    one_for_all = any(all((r, v) in approved_pairs for r in requests) for v in reviewers)
    print("Every request has a reviewer:", per_request)
    print("One reviewer covers all requests:", one_for_all)


if __name__ == "__main__":
    main()

Rule: admin OR (owner AND approved)
admin=True, owner=False, approved=False: expected=True, faulty=False
admin=True, owner=True, approved=False: expected=True, faulty=False
Repair agrees on all 8 Boolean valuations.
Every request has a reviewer: True
One reviewer covers all requests: False

Exercises 1–12 take 110 planned minutes and earn five points each. Exercises 13–14 are optional and add 25 minutes. Show domains, intermediate logical steps, and the scope of your conclusion; the final Boolean value alone does not earn full credit.

The nine choices are checked automatically; the written explanation earns the remaining point after self-review. Read the feedback even when a choice is correct. A quiz score is evidence of the assessed skills, not a proof of every later claim.

Required, 15 minutes: in the open textbook linked by MIT Mathematics for Computer Science, read the propositions section’s truth tables and implication discussion. Compare its notation with ours and give your own false-antecedent example.

Required, 20 minutes: read the same textbook’s predicate-formulas discussion of universal and existential quantifiers and their negations. Select one mixed-quantifier statement, declare its domains, and describe which witness may depend on which variable. Later proof and induction sections are reserved for Module 04.

Optional: consult the official Python truth-value and Boolean operation documentation when explaining why and or or can return an operand. The lesson’s mathematical definitions and examples are original; the textbook and documentation support further study.

Connective definitions determine rows; rows determine equivalence, satisfiability, and validity. Quantifiers state which domain members must work and which witnesses may vary. A specification uses those statements to connect allowed inputs with promised results, while a counterexample identifies a failed promise. Complete finite checking establishes a claim over its finite model; an infinite claim needs a covering argument.

Exit task: write the administrator rule with parentheses; translate and negate a request–reviewer requirement; state a first-match contract; and explain the difference between all Boolean valuations and a finite range of integer tests. Use the course rubric of exercises 60, lab explanations 30, and quiz 10. Explain each answer after feedback rather than relying on your score alone.

Module 03 uses these logical rules to define sets, classify relations, and prove membership identities. Retrieve the meanings of “every pair,” “some witness,” and “not every” before studying relation properties. The course overview gives the availability of the next lesson.