Propositions, quantifiers, and precise specifications

Prerequisites: Basic arithmetic and the distinction between a claim and an example.

Learning objectives

• Translate implications and quantifiers into precise requirements.
• Negate a quantified statement correctly.
• Find counterexamples to invalid logical equivalences.

Truth depends on a specified world

A proposition is a statement that has a truth value under an interpretation. Let A mean “the caller is authenticated” and O mean “the caller owns this document.” A read permission could require A AND O. Its truth table accepts only the case where both inputs are true. A different policy, A OR O, admits three of the four assignments. One word changes the behavior of the system.

Implication P implies Q, written P -> Q, rules out the case P is true and Q is false. It does not assert P, and it does not assert that P caused Q. “If a request succeeds, its token was valid” is compatible with many valid requests failing. Reversing that implication would require a separate justification. The contrapositive, NOT Q -> NOT P, is equivalent to the original implication; the converse Q -> P is not.

Quantifiers expose hidden requirements

Suppose U is a set of users and D is a set of documents. Write CanRead(u,d) for a predicate. The statement “every user can read some document” is for every u in U, there exists d in D: CanRead(u,d). The document may depend on the user. Swapping the quantifiers says there is one document readable by every user. That is a stronger and different requirement.

Take users Ada and Bo, and documents X and Y. Ada can read only X; Bo can read only Y. The first statement holds, while the second fails. This small model is a complete counterexample to the proposed equivalence. You do not need a large production incident to reject faulty logic.

To negate a universal statement, find an existential counterexample. NOT(for every x, P(x)) becomes “there exists x with NOT P(x).” Negating an existential statement yields a universal negative. Therefore the negation of “every user can read some document” is “some user cannot read any document,” not “every user cannot read any document.”

Specifications need domains

Always state the domain. “Every account has a recovery contact” might quantify over active accounts, all historical accounts, or accounts except service accounts. An empty domain makes a universal statement true and an existential statement false. This matters for checks over empty collections. A program that verifies all submitted proofs may accept an empty submission unless the specification separately requires at least one proof. Precision connects logic to executable validation.

Practice problem

An upload service has sets of users U and files F. Define Owns(u,f), Public(f), and Reads(u,f). Formalize these requirements: owners may read their files; every file has at least one owner; no private file is readable by a non-owner. Negate the second requirement. Construct a two-user, two-file model showing why “every file has an owner” does not imply “one user owns every file.” State whether the first requirement guarantees that every user has a readable file.

Worked solution

Use universal quantification for policy rules: for every u,f, Owns(u,f) implies Reads(u,f). File ownership is for every f there exists u with Owns(u,f). Private access is for every u,f, (Reads(u,f) AND NOT Public(f)) implies Owns(u,f). The ownership requirement fails exactly when there exists a file f such that every user u does not own f. Let Ada own only X and Bo own only Y; each file has an owner but there is no common owner. The first requirement is conditional and does not guarantee any ownership, so a user owning no files may have no readable files. Grade the domain, quantifier order, and implication direction separately.

Check your understanding

Which statement negates “every request eventually receives some response”?

• Every request receives no response.
• Some request never receives a response.
• Some response has no request.

Explanation

Negating the universal quantifier produces one request for which the existential response claim fails.

A policy says Successful(r) implies Authorized(r). Which conclusion is valid?

• An authorized request must succeed.
• An unsuccessful request was unauthorized.
• An unauthorized request cannot succeed.

Explanation

The third statement is the contrapositive. The other answers are the converse and inverse, neither of which follows.

Primary reading

• Mathematics for Computer Science: MIT OpenCourseWare

Open the study and save your work →