The reviewer who could see everything

A compliance team asks a reasoning system whether every incident dossier will remain reviewable during a staffing change. The system reads two policy statements:

The conclusion sounds like a tidy restatement. The same nouns recur. The same permission relation appears. No arithmetic changes. Yet the conclusion does not follow.

Imagine two incidents, c₁ and c₂, and two reviewers, r₁ and r₂. Reviewer r₁ is assigned only to c₁; reviewer r₂ is assigned only to c₂. Both premises are true. Every incident has a cleared reviewer, and each reviewer can read the assigned incident. The conclusion is false because neither reviewer can read both incidents.

The system silently changed for every incident, there exists a reviewer into there exists a reviewer for every incident. It replaced ∀c∃r with ∃r∀c. A two-object counterexample is enough to expose the error.

This small failure reveals the central mechanism of logic. A claim is not constrained by how persuasive its sentence sounds; it is constrained by the space of interpretations its formal structure still permits. Sets establish which objects count. Relations establish how those objects may be connected. Quantifiers establish how widely the claim ranges and whether witnesses may vary. Premises remove some interpretations. A modal frame decides which alternatives matter. Proof succeeds only when no admissible interpretation remains in which the premises hold and the conclusion fails.

The distinction matters well beyond mathematics. A system requirement, research conclusion, safety assurance or model capability claim can be factually plausible and logically unsupported. Conversely, an argument can be perfectly valid while starting from false premises. Logic does not replace evidence. It tells us exactly what evidence, assumptions and structure would be sufficient for the conclusion.

The boundary comes before the claim

Membership is a boundary, not a label

Begin with a roster. Let R = {r₁, r₂} be the set of reviewers and C = {c₁, c₂} the set of incidents. Writing r₁ ∈ R says that r₁ belongs to the reviewer domain. It does not yet say what r₁ knows, may do or is connected to.

Set membership performs a quiet but decisive act: it draws a boundary around the objects over which later claims range. In standard set-theoretic foundations, membership is the primitive relation from which sets, functions and many familiar mathematical structures can be built; extensionality then says that sets with exactly the same members are the same set.[1] The practical lesson is simpler. Before asking whether a universal claim is true, ask which objects are inside its domain.

This is a common source of misplaced certainty. “All models passed the test” can mean all models in a selected registry, all deployed versions, all checkpoints derived from a family, or all configurations that share a product name. Each domain produces a different claim. A universal quantifier cannot repair an incomplete roster.

Relations add structure

Now add the assignment relation A ⊆ R × C. The ordered pair (r₁,c₁) ∈ A means reviewer r₁ is assigned to incident c₁. A relation is therefore not another bag of objects. It is a pattern among objects.

Two organisations can have identical reviewer and incident sets but radically different assignment structures. One may centralise every incident under one reviewer. Another may distribute incidents one-to-one. Membership alone cannot distinguish them. The relation does the causal work.

In typed form, a unary predicate such as Cleared(r) classifies one object. A binary relation such as Assigned(r,c) connects two. Lean’s formal account mirrors this distinction: a predicate on objects of type α has the form α → Prop, while a binary relation has the form α → α → Prop.[2] The notation is compact because it keeps the input types visible.

A claim needs a typed record

Natural language usually compresses the information that formal reasoning needs. “Every approved agent can execute the task” leaves open what counts as an agent, which task, whether approval is current, whether permission is task-specific, and whether “can” means technically possible, policy-authorised or guaranteed under all allowed states.

A useful claim record therefore has six fields. This is a practitioner synthesis rather than a new logical calculus:

The record converts a sentence into a search space. Once the admissible objects, structures and alternatives are explicit, proof and counterexample cease to be rhetorical labels. They become two opposed ways of exploring that space.

flowchart TD
  A["The reviewer who could see<br/>everything"] --> B["The boundary comes before the<br/>claim"]
  B --> C["Quantifiers allocate the burden"]
  C --> D["Proof closes a space of<br/>alternatives"]
  D -. "re-test" .-> A
  classDef first fill:#0a1424,stroke:#B96D00,stroke-width:2px,color:#e6f3ff
  classDef step fill:#0a1424,stroke:#3f7da0,stroke-width:1px,color:#e6f3ff
  class A first
  class B,C,D step

Quantifiers allocate the burden

Universal and existential claims fail differently

The universal quantifier ∀ says that a condition holds for every object in the domain. The existential quantifier ∃ says that at least one object satisfies it. Their evidential burdens are asymmetric.

One verified witness establishes an existential claim. One verified exception defeats a universal claim. The reverse directions are harder. To refute an existential claim, the domain must be exhausted or a structural proof must show that no witness can exist. To prove a universal claim by enumeration, every relevant object must be covered. The quantifier therefore determines what a decisive test result looks like.

Negation exposes the same asymmetry. In classical logic, ¬∀x P(x) is equivalent to ∃x ¬P(x): “not everyone passed” means “someone did not pass”. But ∀x ¬P(x) says “nobody passed”, which is much stronger. Scope is not punctuation. It changes the claim.

Formal systems express quantifiers through introduction and elimination rules. To prove a universal claim, one reasons about an arbitrary object and shows the property without relying on anything special about that object. To use a universal claim, one instantiates it at a particular object. To prove an existential claim, one supplies a witness. To use an existential claim, one reasons from an arbitrary witness without assuming which witness it is.[2] These rules prevent a proof from smuggling a chosen example into a general conclusion.

Quantifier order also specifies an information dependency. In ∀x∃y R(x,y), the choice of y may depend on the observed x. A routing service may inspect an incident and then choose a suitable reviewer. In ∃y∀x R(x,y), the witness must be selected before the cases vary, so the same y must work without case-specific substitution. The prefix is therefore a compact description of who may know what before choosing. In engineering terms, the first formula permits an adaptive policy; the second requires a fixed resource or invariant. A system that chooses after seeing each request has not demonstrated that one preselected choice will survive every request.

Relations make exhaustive checking grow quickly

Suppose a domain has n objects. A unary predicate can be interpreted in 2ⁿ ways because each object is either inside or outside the predicate’s extension. A binary relation can be interpreted in 2ⁿ² ways because each ordered pair may be related or not. With five objects, one unary predicate has 32 possible interpretations; one binary relation has 33,554,432.

This growth explains why rigorous reasoning cannot rely on “trying a few cases” once relational structure appears. Proof compresses many cases into a rule-governed derivation. Model search uses symmetry, constraints and heuristics to find a violating case without enumerating everything blindly.

Truth, validity and soundness answer different questions

Truth concerns a sentence under an interpretation. Validity concerns an argument form across interpretations. An argument is valid when there is no admissible case in which all its premises are true and its conclusion is false. This model-centred account makes a counterexample the defining witness of invalidity.[3][4]

Soundness, in the everyday argument sense, adds factual premises. A sound argument is valid and has true premises. That distinction prevents two errors. A valid argument can start from fiction. An invalid argument can land on a true conclusion by accident.

Consider the valid argument: all unicorns are licensed pilots; Nila is a unicorn; therefore Nila is a licensed pilot. The form is impeccable. The premises are not established. Now consider: the server is online; therefore the audit is complete. Both statements may happen to be true, but the inference is invalid because the premise does not force the conclusion.

A correct conclusion does not retrospectively validate the route that produced it. This matters when evaluating generated rationales. A model may state a true answer and offer premises that do not entail it. Conversely, a machine-checked derivation may be valid relative to assumptions that fail operationally. Outcome accuracy, premise truth and inferential validity belong in separate ledgers.

Proof closes a space of alternatives

A proof is a dependency object

A proof is often displayed as a line of steps, but its deeper structure is a dependency graph. Definitions support premises. Premises support intermediate lemmas. Lemmas support the conclusion. Some branches may be independent. Others converge on a single hidden assumption.

Formal proof systems specify which transformations are allowed. Soundness means that permitted derivations do not carry true premises to a false conclusion. Completeness, for classical first-order logic, means that every semantically valid consequence can in principle be derived in a suitable proof system.[5] These are claims about the relation between syntax and semantics, not guarantees that every theorem is easy to find.

Proof assistants such as Lean place propositions and proofs in a formal language, then ask a small trusted kernel to check that a proof term has the claimed type. The system can verify that the derivation follows its rules. It cannot decide whether the chosen definitions capture the organisation’s intended policy or whether an empirical premise is true.[8]

A proof certificate should expose its assumption surface. In an operational setting, each premise can carry an owner, source, effective interval and revocation condition. The dependency lattice then becomes more than a mathematical picture. It becomes a change-impact map: when one premise expires, every dependent conclusion is marked for re-evaluation.

Validity is global; necessity is frame-relative

The notation Γ ⊨ φ says that every admissible interpretation making all premises in Γ true also makes φ true. Validity quantifies over interpretations of the relevant non-logical vocabulary. A countermodel is an interpretation in which Γ is true and φ false.

Necessity introduces another layer. In relational modal semantics, a model contains possible worlds and an accessibility relation. At a world w, □P is true when P is true at every world accessible from w. Possibility ◇P requires at least one accessible world where P holds.[6]

This makes necessity precise but also relative. Logical necessity, physical necessity, policy necessity and temporal invariance use different spaces of alternatives. “The reviewer must retain access” may mean the current policy requires access, every allowed future policy state preserves access, or access follows from logic alone. Those are not interchangeable.

“Necessary” is incomplete until the comparison class is named. A policy team may reasonably exclude physically impossible states. A safety team may include adversarial but reachable states. A mathematician may quantify over all models of an axiom system. Each choice changes what a counterexample must look like.

Proof and model search meet at negation

The semantic relation has a computationally useful form:

To challenge a conclusion, keep the premises and add the negation of the conclusion. If a satisfying model exists, it is a countermodel. If no model exists, the premises rule out every way for the conclusion to fail within the chosen logic and theory. SMT systems operationalise this satisfiability perspective for formulas interpreted with background theories such as integers, arrays and bit-vectors.[9]

stateDiagram-v2
  [*] --> Claim
  state "Membership is a boundary, not<br/>a label" as Claim
  state "Relations add structure" as Test
  state "A claim needs a typed record" as Revision
  Claim --> Test: expose mechanism
  Test --> Decision: evidence survives
  Test --> Revision: rival survives
  Revision --> Claim: narrow or rebuild
  Decision --> [*]

Counterexamples become instruments

A good counterexample is small, admissible and diagnostic

A counterexample is more than an awkward exception. It is a model of the premises plus the negation of the conclusion. Its job is to show exactly how the claim can fail while respecting everything the claim declared non-negotiable.

The smallest counterexample is often the most informative. The two-reviewer, two-incident model reveals that the missing property is not “more reviewers” or “more incidents”. It is a shared witness. Adding scale would hide that structure.

A practical counterexample protocol works in this order:

1. Declare the domain and typing rules.
2. Write the relation symbols and their arities.
3. Normalise quantifier order and negation scope.
4. Keep the premises, then add the negated conclusion.
5. Search the smallest admissible models first.
6. Classify the failure: boundary, relation, scope, premise, modality or execution path.
7. Repair by weakening the conclusion or adding a justified premise.

Model checking brought this idea into systems engineering. A finite-state model checker evaluates whether a model satisfies a temporal specification and, when the property fails, can return a counterexample execution showing a violating path.[11][12] The trace is evidence of violation, not automatically a diagnosis of root cause. The specification, abstraction and environment assumptions still require scrutiny.

Executable lab: a bounded premise and counterexample checker

The instrument below accepts a small first-order vocabulary with unary predicates, binary relations, equality, connectives and quantifiers. It enumerates finite interpretations over domains of size one to three, searching for a model in which every premise is true and the conclusion is false.

The default case is the quantifier swap from the opening. Select “Valid transfer” to test a consequence that is valid in ordinary first-order logic. Select “Vacuity” to see how a universal premise can be true even when its subject class is empty.

for n in 1 .. max_domain_size:
    vocabulary = predicates_and_relations(premises, conclusion)
    for interpretation in all_interpretations(vocabulary, domain_size=n):
        if every(premise is true in interpretation)
           and conclusion is false in interpretation:
            return Countermodel(interpretation)
return NoCountermodelFoundWithinBound

How to interpret the checker

Quantified reasoning is a sharp boundary for automation. General first-order validity is not decidable, and practical solvers use incomplete heuristics for many quantified problems. The Z3 guide explicitly warns that quantified reasoning can diverge, especially when satisfiable formulas require infinite models.[10] “Unknown” and “not found” are legitimate outcomes, not failures to be hidden.

A negative search result inherits the limits of the search procedure. A positive counterexample is often stronger: one well-typed admissible witness can settle invalidity immediately. This asymmetry is why counterexample-first reasoning is efficient for broad claims.

The strongest boundary: formalisation can be wrong

Formal logic constrains what follows from a representation. It does not guarantee that the representation is the right one. A flawless proof of the wrong specification is still the wrong decision instrument.

Four boundaries deserve explicit treatment:

First, premise truth is not supplied by validity. Empirical claims require measurement, testimony, observation or authoritative records. A proof may show that a decision follows if those records are accurate.

Second, the model class is a substantive choice. Excluding a countermodel is legitimate only when a justified axiom, type rule or environmental constraint rules it out. Declaring an inconvenient case “unrealistic” after it appears is not a proof repair.

Third, logics encode different consequence relations. Classical logic validates excluded middle and explosion.[13] Intuitionistic logic ties assertion more closely to construction.[14] Paraconsistent logics can block arbitrary conclusions from contradiction.[15] Logical pluralism treats logics as rival accounts of validity for different purposes, so the selected consequence relation must be named rather than smuggled in.[7]

Fourth, machine checking verifies the formal object presented to it. A trusted kernel can reduce transcription and derivation errors. It cannot infer the omitted stakeholder, the stale policy, the wrong unit of analysis or the ambiguity hidden inside “must”.

The practical remedy is not to abandon formalism. It is to attach a specification review to the proof review. Ask domain experts to challenge membership and relation choices. Ask logicians or formal-methods practitioners to challenge quantifier scope and derivation. Ask operators to challenge reachability and temporal assumptions. Different reviewers attack different layers of the claim.

Make logic change the design

When a consequential claim arrives, do not begin by asking whether it sounds plausible or whether a confident system produced it. Begin by reconstructing the space it quantifies over.

• Membership: Which objects are inside the domain, and which operational objects sit outside it?
• Relation: Which connections, directions and types does the claim require?
• Quantification: May the witness vary by case, or must one witness persist across all cases?
• Validity: Can the premises all be true while the conclusion is false?
• Necessity: Across which alternatives, laws, policies or future states must the claim hold?
• Counterexample: What is the smallest admissible model or execution that would defeat it?

Then make one of three decisions. If a counterexample exists, reject or weaken the claim. If the conclusion requires a missing premise, make that premise explicit and obtain evidence for it. If the claim survives targeted counterexample search, move to a proof or a verification method whose guarantee matches the intended model class.

The access-control case now reads differently. “Every incident has someone who can read it” is a coverage claim. “Someone can read every incident” is a centralisation claim. “Someone will always be able to read every incident” is a temporal or modal resilience claim. Each demands a different architecture and a different proof obligation.

Logic earns its value when it changes the design, not when it decorates the conclusion. Sets reveal what the claim includes. Relations reveal the structure it assumes. Quantifiers reveal who carries the burden. Validity reveals whether the conclusion is forced. Necessity reveals which alternatives matter. Counterexamples reveal where the claim breaks. Proof is the certificate that no admissible break remains.