1.3 Predicate Logic: Objects, Quantifiers, and Program Specifications

Propositional logic treats a statement like "Administrator Alice passed MFA" as a single unit, but it cannot directly express something like "Every administrator must pass MFA." Predicate logic opens up the structure of formulas, introducing objects, properties, relations, and quantifiers.

Language, Structure, and Interpretation

A first-order language can include:

• Constant symbols: alice, serverA;
• Function symbols: owner, manager, used in terms such as owner(project);
• Predicate symbols: Admin, Owns, used in formulas such as Admin(x);
• Variables, logical connectives, and quantifiers.

The symbols themselves carry no inherent meaning. A structure (also known as an interpretation) is required to assign meaning:

1. Specify the domain of discourse, such as all users in a system;
2. Assign constants to specific objects;
3. Define how functions map objects;
4. Specify for which objects predicates are true.

The same formula can have different truth values under different interpretations. When writing specifications, the domain of quantifiers must be explicitly defined, never assume that "all" refers to all users, active users, or users within a particular tenant.

Standard first-order logic usually has a nonempty domain and interprets function symbols as total functions. If a project can lack an owner, owner(project) cannot silently be assumed to return a user; use a relation or an explicit unassigned object with defined rules. See Open Logic’s chapter on structures.

The examples below abbreviate quantification over named object categories such as users, resources, and orders. For a single overall domain, expand a user-restricted ∀u as ∀u(User(u) → ...), with similar guards for other categories. Such a subset can be empty even though the overall domain is nonempty.

Terms, Atomic Formulas, and Composite Formulas

A term refers to an object within the domain of discussion:

x
alice
owner(projectA)
manager(owner(projectA))

Predicates act on terms to form atomic formulas:

Admin(x)
Owns(alice, projectA)
CanDelete(user, project)

These can then be combined using logical connectives and quantifiers:

∀x (Admin(x) → HasMfa(x))
∃x (Admin(x) ∧ Locked(x))

The first statement means every administrator in the domain has passed MFA. The second indicates that at least one entity exists that is both an administrator and locked.

Free and Bound Variables

In:

∀x (Owns(x, p) → CanEdit(x, p))

x is bound by ∀x, while p is not constrained by any quantifier and is therefore a free variable. A formula containing free variables resembles a conditional that depends on parameters, only when all variables are bound does the formula become a sentence with a definite truth value.

Quantifiers only govern their own scope:

∀x Admin(x) → HasMfa(x)

Without parentheses, the parsing depends on syntactic conventions, and x might become a free variable in the second clause. Engineering specifications should be written as:

∀x (Admin(x) → HasMfa(x))

Quantifier Order Cannot Be Arbitrarily Swapped

∀u ∃r CanAccess(u, r)

Every user has access to at least one resource; different users may access different resources.

∃r ∀u CanAccess(u, r)

There exists a single resource that all users can access. This statement is significantly stronger.

Two users, each able to access only their own resource, distinguish the formulas. This Python 3 standard-library example directly enumerates finite sets:

users = ["u1", "u2"]
resources = ["r1", "r2"]
access = {("u1", "r1"), ("u2", "r2")}

def every_user_has_resource(users, resources):
    return all(any((u, r) in access for r in resources) for u in users)

def one_resource_for_all(users, resources):
    return any(all((u, r) in access for u in users) for r in resources)

print(every_user_has_resource(users, resources))  # True
print(one_resource_for_all(users, resources))    # False
print(all([]), any([]))                          # True False

all([]) is true because there is no counterexample; any([]) is false because there is no witness. “All administrators passed MFA” therefore holds when there are no administrators. If the business also requires an administrator to exist, add that existential requirement; an empty set will not report a staffing shortage.

This distinction appears similarly in software requirements, such as "every request has a trace ID":

∀request ∃traceId HasTrace(request, traceId)

Writing ∃traceId ∀request ... instead requires at least one ID associated with every request. The original existence statement guarantees neither exactly one ID per request nor distinct IDs across requests. Distributed tracing may intentionally share trace IDs among related requests; define the intended uniqueness scope separately.

Quantified Negations

De Morgan's laws have corresponding forms for quantifiers:

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

"The fact that not all nodes are healthy" means "at least one node is unhealthy," not "all nodes are unhealthy." This kind of error is common in alert queries and test assertions.

Expressing Existence and Uniqueness

"The existence of a single creator for each order" cannot be expressed merely as existence:

∀o ∃u CreatedBy(o, u)

It must also express that any two creators for the same order are actually the same:

∀o ∃u (
  CreatedBy(o, u)
  ∧ ∀v (CreatedBy(o, v) → v = u)
)

The notation ∃!u may be used to represent "a unique u" if the document has already defined this notation.

Must distinguish ∀x(P → Q) from ∀x(P ∧ Q)

"All administrators have passed MFA" is typically written as:

∀x (Admin(x) → HasMfa(x))

Non-administrators make the antecedent false, but this does not affect the validity of the rule.

If instead written as:

∀x (Admin(x) ∧ HasMfa(x))

it requires every entity in the domain to be both an administrator and to have passed MFA, which changes the meaning entirely.

Existential quantifiers are often used in conjunction with conjunctions:

∃x (Admin(x) ∧ HasMfa(x))

If written as ∃x(Admin(x) → HasMfa(x)), the formula could easily be true if there's just one non-administrator in the domain, failing to express the intent of "there exists at least one administrator who uses MFA."

From Precondition to Postcondition

Program specifications can be expressed using predicates that describe the state:

Precondition: amount > 0 ∧ balance(account) >= amount

Execution: withdraw(account, amount)

Postcondition:
balance'(account) = balance(account) - amount

The prime symbol denotes the state after execution. It's also important to specify unchanged parts of the state (the frame condition) otherwise the specification only constrains changes to the balance and allows the method to arbitrarily modify other account properties.

Loop invariants are also predicates. For example, when computing the sum of the first i elements of an array:

0 <= i <= n
sum = Σ(k=0..i-1) a[k]

By proving that the invariant holds at initialization, is preserved in each iteration, and leads to the desired result upon termination, we can establish overall correctness from local steps. This topic will be expanded further in Chapters 3 and 4, covering formal proofs and induction.

Relationship with Type Systems Must Be Expressed with Caution

There is a deep connection between logic and types, for instance, the Curry–Howard correspondence treats certain types as propositions and programs as proofs. Generic quantification also often employs notations like ∀ and ∃. However, it is incorrect to state that "the essence of all type systems is first-order predicate logic." Different type systems incorporate higher-order types, dependent types, subtyping, effects, and runtime checks, each using distinct logics and semantics.

In typical programs, predicates are more commonly used for:

• API preconditions and postconditions;
• Database constraints and authorization policies;
• Static analysis, symbolic execution, and SMT queries;
• Model checking and verification of properties.

Database Query Reminder: Three-Valued Logic

“There is no administrator who has not passed MFA” can be written in classical logic as:

¬∃x (Admin(x) ∧ ¬HasMfa(x))

A typical SQL query corresponds to NOT EXISTS. However, SQL's NULL introduces UNKNOWN, NOT IN, and negation behaviors that may differ from classical binary logic. When translating formulas into query languages, it's essential to verify the database's null semantics.

Suppose is_admin is known and non-null, while unknown MFA status must not count as satisfying the rule. This complete query runs in PostgreSQL or DuckDB:

WITH users(user_id, is_admin, has_mfa) AS (
  VALUES ('admin-a', TRUE, CAST(NULL AS BOOLEAN)),
         ('member-b', FALSE, FALSE)
)
SELECT
  NOT EXISTS (
    SELECT 1 FROM users WHERE is_admin AND NOT has_mfa
  ) AS unchecked_claim,
  NOT EXISTS (
    SELECT 1 FROM users WHERE is_admin AND has_mfa IS NOT TRUE
  ) AS confirmed_claim;
-- unchecked_claim = TRUE, confirmed_claim = FALSE

The first column misses the UNKNOWN produced by NOT has_mfa on a null value, because WHERE keeps only TRUE. The second uses IS NOT TRUE to catch both FALSE and UNKNOWN, explicitly choosing a policy that unconfirmed status does not pass. This checks the table snapshot only; session validity and status provenance need separate constraints. See PostgreSQL’s comparison documentation.

The Limits of First-Order Logic Capabilities

Finite propositional formulas can be evaluated using truth tables. However, general first-order logic validity lacks a decision algorithm that guarantees termination and produces a yes/no answer for all inputs. In contrast, known enumerable finite domains, restricted fragments, or particular theories within SMT (Satisfiability Modulo Theories) problems may be decidable or effectively solvable in practice.

This explains why verification tools often require finite bounds, restricted quantifier shapes, or return unknown upon timeout. Formalization does not imply that any specification can be automatically solved.

Completion Check

Formalize the following rules for a multi-tenant project system:

1. Each project belongs to exactly one tenant.
2. A user can edit only projects within their own tenant.
3. Each project has at least one responsible person.
4. No user belongs to two tenants simultaneously.
5. Not all administrators can delete audit records.

For each rule, identify the discussion domain, free variables, and quantifier scope. Provide one counterexample for each quantifier ordering error.

References

• Open Logic Project
• SMT-LIB Standard