Sets, Logic and Proof

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 operational 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.

Admissibility is part of the mechanism

A countermodel matters only if it belongs to the class the claim is meant to cover. Syntax does not choose that class by itself. Types exclude malformed cases, premises exclude cases that contradict declared facts, background theories constrain relations, and an operational model decides which state transitions are reachable. Together these choices form an admission contract for models.

The opening countermodel is admissible if reviewers may be assigned separately. It is inadmissible if the implemented system enforces one current reviewer across all incidents. That exclusion must come from an enforced invariant, not from discomfort with the result. A design aspiration, a policy sentence and a mechanism that prevents split assignment are three different things.

Three exclusions are often confused. A case can be impossible under the chosen types, prohibited by policy but technically reachable, or simply absent from previous observations. Only the first is automatically outside the formal domain. The second may be central to assurance because systems can violate policy. The third remains a live possibility unless some mechanism rules it out.

Changing the admissible model class changes the theorem. Adding a justified invariant can make a conclusion follow because the system now prevents the defeating structure. Adding an unjustified assumption can produce the same formal result while merely defining the failure away. A review should therefore record each exclusion, its evidence, its owner and the condition that would invalidate it.

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.

A witness must be realised by a mechanism

The formula ∀c∃r Assigned(r,c) establishes a relational coverage condition. It does not specify how a running system finds the reviewer, how quickly it does so, or whether the reviewer has authority when selected. An existence claim can be true even when no executable selection procedure has been supplied.

A configured system must materialise the witness. It may use a deterministic routing function, a constrained search, or a human allocation step. Whatever the method, its preconditions must match the proof: the incident must appear in the current domain, the candidate roster must be current, and the assignment operation must complete before later reasoning treats the relation as true.

The second premise also needs a mechanism. Assigned(r,c) → MayRead(r,c) may be enforced by a synchronous transaction, or it may be an eventual relationship across a policy service and an access gateway. Those implementations admit different intermediate states. A proof about the composed relation is only as current as the mechanisms that realise each logical bridge. Quantifiers expose the dependency; architecture determines whether that dependency is actually satisfied.

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.

Proof becomes useful when it can be withdrawn

A proof certificate is durable only while its premises, definitions and admission contract remain valid. In a changing system, that makes withdrawal as important as derivation. If the reviewer roster changes, an assignment invariant is relaxed, or the meaning of MayRead moves from policy entitlement to verified gateway access, affected conclusions should lose their approved status until they are checked again.

A minimal operational proof pack contains the formal claim, the named logic, the model admission contract, the derivation or checked certificate, and evidence for each empirical premise. It also identifies the counterexample shape used during review. This package separates two questions: whether the conclusion follows from the encoded assumptions, and whether current operating evidence still supports those assumptions.

The separation creates practical controls. A release gate can reject a configuration that violates a proven invariant. A change-impact check can identify conclusions that depend on an altered premise. During an incident, the dependency graph can direct investigation towards the first failed bridge rather than the final symptom.

Proof is not a substitute for monitoring; it determines what monitoring must keep true. A static derivation can certify the relationship between assumptions and conclusion. Receipts, readbacks and failure tests establish whether the live system remains inside that certified region.

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]

Counterexamples become instruments

A good counterexample is small, admissible and diagnostic

A counterexample is not merely 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

A countermodel can be decisive and still mislead

A countermodel decisively refutes entailment inside the implemented semantics. It does not show that the case is reachable, likely or causally responsible for an observed failure. An abstraction may admit a state that the real transition rules prevent. Such a witness is spurious operationally, even though it is genuine relative to the abstraction.

The opposite error is more dangerous. An overconstrained model can exclude the real failure before search begins. If the specification defines assignment and effective access as the same relation, no checker can discover the propagation gap in the worked scenario. The hidden equivalence has removed the critical intermediate state from the model class.

Every returned witness therefore needs four checks: type correctness, premise satisfaction, transition reachability and correspondence with the intended real-world terms. A spurious witness calls for a justified refinement. A reachable witness calls for rejection, containment or a stronger mechanism. A witness excluded only by an unsupported assumption calls for reopening the admission contract.

Countermodel search is a test of the claim plus its boundary, never of the sentence alone. When no witness appears, report the exact bound and theory searched. When one appears, report both the logical refutation and the separate evidence for operational reachability.

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.

The decision this changes

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.

For a configured system, link every empirical premise to the evidence that keeps it current. A registry premise needs a roster readback. A permission premise needs an effect receipt from the enforcing gateway. A transition premise needs a trace or failure test that exercises the relevant ordering. The proof record should become stale when any linked evidence expires, changes meaning or loses its authoritative source.

Also decide whether the guarantee concerns a snapshot or a trajectory. Snapshot proof is sufficient for questions about one settled state. It is insufficient when a release, handover, retry or partial failure can pass through an unsafe intermediate state. In that case, prove an invariant over allowed transitions and test the mechanism that preserves it. The formal claim, operational evidence and recovery action must use the same boundary.

This discipline produces a useful stopping rule. Approve only the strongest claim supported by both derivation and operating evidence. If the proof covers a smaller model class than the decision, narrow the decision. If the decision cannot be narrowed, expand the model and search again before granting authority.

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.