1.1 Propositional Logic: From Requirement Sentences to Decidable Formulas

A common statement in permission requirements is: "Only administrators who have passed two-factor authentication can delete projects." Someone implemented this as:

if (isAdmin || hasMfa) {
    deleteProject();
}

The code runs, but the meaning has changed. In natural language, words like "only," "unless," and "if and only if" are easily misinterpreted as different conditions. Propositional logic gives us a way to check whether the formal condition matches the requirement.

Propositions and Formulas

A proposition is a statement with a definite truth value. In a given context, it is either true or false:

• The server is accepting traffic;
• The request carries a valid token;
• 2 + 3 = 5.

Questions, commands, and sentences with uncertain meaning cannot be directly treated as propositions. x > 3 is not a closed proposition because x has not been assigned a value; it is better suited for handling in predicate logic.

Use propositional variables p and q to represent atomic propositions, and then construct a formula using logical connectives:

Name	Symbol	Truth Condition	Common Code Shapes
Negation	¬p	p is false	!p
Conjunction	p ∧ q	Both true	p && q
Disjunction	p ∨ q	at least one true	p || q
Implication	p → q	False only when p is true and q is false	Constraint relationship, not equivalent to if statement
Biconditional	p ↔ q	Same truth value	Bidirectional implication

Formal grammar tells us which strings are formulas, for example:

φ ::= p | ¬φ | (φ ∧ φ) | (φ ∨ φ) | (φ → φ) | (φ ↔ φ)

Parentheses and precedence are syntactic; truth values are semantic. In engineering documentation, it's best to keep parentheses and avoid letting readers guess the binding order of ¬p ∨ q ∧ r.

Truth Assignments Define Semantics

An assignment v specifies for each atomic proposition either T or F, and the truth value of composite formulas is recursively computed by the rules of connectives.

For example:

p	q	p → q	¬p ∨ q
T	T	T	T
T	F	F	F
F	T	T	T
F	F	T	T

The two columns are identical for all assignments, so:

p → q ≡ ¬p ∨ q

When p is false, p → q is true, which is known as the case where the antecedent is false. It expresses a truth constraint, but does not automatically imply causal relationships, temporal sequence, or correlation in reality.

Necessary and Sufficient Conditions

"p is a sufficient condition for q" means: if p holds, then q is true.

p → q

"p is a necessary condition for q" means: without p, q is impossible.

q → p

Back to the initial permission requirements:

Here delete means that this request is allowed to delete, not that deletion has actually happened. Permission does not require the user to perform the operation:

Only administrators who have completed MFA can delete.
delete → (admin ∧ mfa)

It states that administrators and MFA are necessary conditions for a delete operation. Only add the reverse direction when the requirement also grants permission to everyone meeting both conditions.

delete ↔ (admin ∧ mfa)

Permission systems often include conditions such as resource ownership and policy denial, so don't arbitrarily strengthen necessary conditions into biconditionals.

This Python 3 standard-library example enumerates the two necessary conditions and finds counterexamples to the opening || implementation:

from itertools import product

violations = []
for admin, mfa in product([False, True], repeat=2):
    granted_by_bad_code = admin or mfa
    necessary = admin and mfa
    if granted_by_bad_code and not necessary:
        violations.append((admin, mfa))
print(violations)
# [(False, True), (True, False)]

The counterexamples are a non-administrator with MFA and an administrator without MFA. Replacing or with and enforces these two necessary conditions; the remaining policies still determine permission. Four Boolean combinations exhaust this model, without covering unmodeled facts such as identity trust or session expiry.

Inclusive and Exclusive Or

The logical symbol ∨ typically denotes OR: at least one is true, and both being true also holds. Exclusive OR (XOR) means exactly one is true:

p ⊕ q ≡ (p ∨ q) ∧ ¬(p ∧ q)

"User password or passkey login" in requirements usually means inclusive OR; "the primary node can only be on A or B, not both" is closer to exclusive OR. The word "or" in natural language must be clarified by business constraints.

Three Important Formula Properties

For the formula φ:

• Tautology: Every assignment makes φ true, for example p ∨ ¬p;
• Contradiction: There is no assignment that makes φ true, for example p ∧ ¬p;
• Satisfiable: There exists at least one assignment that makes φ true.

Satisfiable does not imply always true. p ∧ q is satisfiable, but holds only when both are true.

There are two relationships that are easy to confuse:

φ ≡ ψ  the same truth value under every assignment (logical equivalence)
Γ ⊨ φ means every assignment that satisfies the premise set Γ also satisfies φ (semantic entailment).

For example:

{p → q, p} ⊨ q

This doesn't mean that q is logically equivalent to the premise, but rather that any assignment satisfying both premises cannot make q false.

Steps to Translate Requirement Formulas

Requirements:

If deployed to production, approval and security scanning are required; emergency changes may bypass standard approvals but must still undergo scanning.

First, define atomic propositions:

p: Deploy to production
a: Complete standard approval
s: Security scan passed
e: Emergency change

Break it down into separate constraints:

p → s
(p ∧ ¬e) → a
e → p  // If business definition states that urgent changes are always production changes

Don't rush to collapse it into a single "smart" formula. Multiple clearly named constraints are easier to review and help SAT/SMT tools pinpoint exactly which one is causing a conflict.

Logical operations are not the same as program execution

On pure boolean values, p ∧ q and q ∧ p are equivalent; in programs with side effects or errors, swapping the operands may change behavior:

user != null && user.isActive()

Java's && short-circuit evaluation first checks user != null. Reversing the order would first dereference user, possibly throwing an exception. Database SQL still contains NULL causing three-valued logic, and cannot directly rewrite all WHERE conditions as classic binary propositional formulas.

Before optimizing code with logical equivalence, ensure the expression evaluation is always defined, has no side effects, and that the truth value system of the programming language is consistent.

The Java behavior is specified by JLS 21 §15.23. Distinguish primitive boolean from nullable Boolean, which can also throw during unboxing.

Completion Check

Translate the following requirements into formulas and provide definitions of atomic propositions:

1. Only owners or administrators can close tickets;
2. Releases must go through testing unless the release is canceled;
3. The primary and standby replicas have at least one available, but not both can serve as the primary at the same time;
4. If the request has neither a token nor is within the allowed network, reject the request.

For each formula, find one "similar wording but different logic" counterexample.

References

• Open Logic Project
• SMT-LIB Standard