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

First-order logic can include:

• Constant symbols: alice, serverA;
• Function symbols: owner(project), manager(user);
• Predicate symbols: Admin(x), Owns(x, y);
• 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.

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 uses multi-factor authentication. 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.

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

∀request ∃traceId HasTrace(request, traceId)

If mistakenly written as ∃traceId ∀request ..., it would imply that all requests share the same trace ID.

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)

"The requirement that all administrators use multi-factor authentication" 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 MFA enabled, this 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

"The statement 'there is no administrator without 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.

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, specific finite domains, restricted fragments, or combined 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