Resolution, refutation, and falsification

This tutorial is about one deep structural resemblance:

• logic can prove a statement by assuming its negation and driving that assumption into contradiction,
• science can attack a theory by trying to falsify it and seeing whether it survives.

Those are not the same thing.

But they do share the same adversarial shape.

The key distinction is this:

Resolution is falsification inside a closed formal world. Science is falsification inside an open empirical world.

The point of this page is to say that precisely, in formulas.

One distinction matters immediately:

• symbols like $\models$ and $\vdash$ are metalogical, they talk about truth-from-premises and derivability,
• ordinary predicate logic writes the same idea using predicates and quantifiers inside the formula language.

Both are useful. This page uses both, but it keeps them separate.

Quick reading guide:

• Σ ⊨ P means P is true in every model that satisfies Σ,
• Σ ⊢ P means there is a formal derivation of P from Σ using the proof rules,
• ⊨ is semantic entailment,
• ⊢ is syntactic provability.

Part I: the resolution rule itself

The simplest resolution step is:

\[\frac{A \lor B \qquad \neg A \lor C}{B \lor C}\]

More generally:

\[\frac{L \lor \Gamma \qquad \neg L \lor \Delta}{\Gamma \lor \Delta}\]

where $L$ is a literal and $\Gamma,\Delta$ are disjunctions of literals.

So in this rule:

• L is the attacked literal,
• ¬L is its negation,
• Γ stands for “the rest of the first clause,”
• Δ stands for “the rest of the second clause.”

This is a rule for removing an attacked middle term. If one clause says “either $A$ or $B$,” and another says “either not-$A$ or $C$,” then any model satisfying both must satisfy $B \lor C$.

Another way to say the same thing is this:

• the first clause leaves two escape routes, $A$ or $B$,
• the second clause shuts down the $A$ route unless $C$ is available,
• so any surviving model must leave $B$ or $C$ open.

That is why resolution feels like adversarial reasoning. It keeps squeezing away options until either some options remain or none do.

Part I.5: what the symbols mean

The main logical formula in this tutorial is:

\[\Sigma \models P \iff \neg \exists M \in \mathcal{M}\; (M \models \Sigma \land M \models \neg P).\]

In plain English, the same formula says:

P follows from Sigma exactly when there is no model M in the model class under discussion that satisfies all of Sigma and also makes P false.

Read each symbol slowly:

• Σ is the fixed set of premises,
• P is the claim to be proved,
• 𝓜 is the model class under consideration,
• M ⊨ Σ means model M satisfies all premises in Σ,
• M ⊨ ¬P means model M is a counterexample to P,
• ¬∃M means no such counterexample model exists.

So the formula says:

$P$ follows from $\Sigma$ exactly when there is no allowed model in which the premises hold and $P$ fails.

That is the cleanest formal version of “closed formal world.” The world is closed because the premises, language, proof rules, and model class are fixed before the search begins.

That formula is metalogical. If an ordinary predicate-logic version is wanted instead, it can be written by replacing $\models$ with explicit predicates:

\[\mathrm{ClosedFormalWorld}(\Sigma,P) \iff \neg \exists m\; \big( \mathrm{AllowedModel}(m) \land \mathrm{SatAll}(m,\Sigma) \land \mathrm{Sat}(m,\neg P) \big).\]

This says the same thing, but now the whole statement is written as one predicate-logic formula.

Part II: proof by refutation

Let $\Sigma$ be a clause set and let $P$ be the statement to prove.

The semantic form is:

\[\Sigma \models P \iff \neg \exists M \; (M \models \Sigma \land M \models \neg P).\]

This is the cleanest formula for the “closed formal world” idea.

It says:

• the premises are fixed, namely $\Sigma$,
• the candidate counterexamples are fixed, namely models $M$,
• the attack condition is fixed, namely satisfying both $\Sigma$ and $\neg P$.

If no such model exists, then $P$ follows from $\Sigma$.

This can be understood as failed counterexample search:

\[\text{prove } P \quad\Longleftrightarrow\quad \text{show that every attempted model of } \Sigma \land \neg P \text{ fails}.\]

The proof-theoretic refutation form is:

\[\Sigma \models P \iff \Sigma \cup \{\neg P\}\ \text{is unsatisfiable}.\]

And for resolution specifically:

\[\Sigma \models P \iff \Sigma \cup \{\neg P\} \vdash_{\mathrm{Res}} \Box\]

where $\Box$ is the empty clause.

So the direct logical shape is:

\[\text{Proof by refutation} := \neg \exists M \; (M \models \Sigma \land M \models \neg P).\]

That is why “closed formal world” is the right phrase. The world of possible counterexamples is a mathematically fixed model class.

Part II.5: a tiny worked refutation

Take

\[\Sigma = \{A \lor B,\ \neg A\}\]

and suppose the goal is to prove $B$.

Add the negation of the goal:

\[\Sigma \cup \{\neg B\} = \{A \lor B,\ \neg A,\ \neg B\}.\]

Now resolve:

\[\frac{A \lor B \qquad \neg A}{B}\]

and then:

\[\frac{B \qquad \neg B}{\Box}\]

So:

\[\Sigma \cup \{\neg B\}\vdash_{\mathrm{Res}} \Box\]

hence

\[\Sigma \models B.\]

The shape is important:

1. assume the negation,
2. search for a consistent survivor,
3. derive contradiction,
4. conclude the original claim.

That is the exact proof-side analogue of “attack the claim and see whether anything survives.”

In ordinary predicate-logic style, that same proof-side shape is:

\[\mathrm{ProvedByRefutation}(\Sigma,P) \iff \neg \exists m\; \big( \mathrm{AllowedModel}(m) \land \mathrm{SatAll}(m,\Sigma) \land \mathrm{Sat}(m,\neg P) \big).\]

Part III: what “closed” means in logic

The closed-world part can be written explicitly by indexing entailment to a chosen model class $\mathcal{C}$:

\[\Sigma \models_{\mathcal{C}} P \iff \neg \exists M \in \mathcal{C}\; (M \models \Sigma \land M \models \neg P).\]

Now everything is fixed:

• the premises $\Sigma$,
• the language,
• the rules,
• the model class $\mathcal{C}$.

So if the proof system is sound, then

\[\Sigma \vdash P \to \Sigma \models_{\mathcal{C}} P.\]

And if the proof system is complete for that setting, then

\[\Sigma \models_{\mathcal{C}} P \to \Sigma \vdash P.\]

This is what makes logical proof final relative to the assumptions:

\[\Sigma \cup \{\neg P\} \vdash_{\mathrm{Res}} \Box \to \Sigma \models P.\]

No future experiment can reopen the matter unless the assumptions, language, or rules change.

This is why proof is stronger than corroboration. In logic, the search space is not merely sampled. It is defined by the model class $\mathcal{C}$. The quantifier really ranges over that whole class:

\[\forall M \in \mathcal{C}.\]

That is the source of finality. If the system is sound and complete for the chosen setting, then the adversarial search has nowhere else to go.

Part IV: Popper in formulas

Now write the scientific side in the same style.

Let $T$ be a theory, and let $E$ be the set of tests actually performed so far.

Define corroboration by:

\[\mathrm{Corroborated}(T,E) \iff \neg \exists e \in E \; \mathrm{Falsifies}(e,T).\]

If falsification is spelled out through predictions, one can write:

\[\mathrm{Falsifies}(e,T) \iff \exists \varphi \; \big( \mathrm{Predicts}(T,e,\varphi) \land \mathrm{Observed}(e,\neg \varphi) \big).\]

So corroboration becomes:

\[\mathrm{Corroborated}(T,E) \iff \forall e \in E,\; \neg \mathrm{Falsifies}(e,T).\]

This already shows the structural resemblance.

The theory survives because no performed test in the current evidence set refutes it.

In ordinary predicate logic, one can make the “open empirical world” point explicit by writing:

\[\mathrm{Corroborated}(T,E) \iff \neg \exists e\; \big( \mathrm{PerformedTest}(e,E) \land \mathrm{Falsifies}(e,T) \big).\]

and

\[\mathrm{OpenEmpiricalWorld}(E) \iff \exists e\; \big( \mathrm{PossibleTest}(e) \land \neg \mathrm{PerformedTest}(e,E) \big).\]

Together these say: no performed test has falsified the theory, and there still exist possible tests outside the current evidence set.

The word “performed” matters. The quantifier is not over all possible experiments. It is over the evidence set currently in hand:

\[\forall e \in E.\]

That is a weaker statement than ranging over every physically possible future test condition.

Part V: the common shape

Now place the two formulas side by side.

Logical proof by refutation:

\[\neg \exists M \; (M \models \Sigma \land M \models \neg P).\]

Scientific corroboration:

\[\neg \exists e \in E \; \mathrm{Falsifies}(e,T).\]

The same shape is visible:

\[\neg \exists (\text{surviving counterexample}).\]

That is the precise structural analogy.

In logic, the counterexample is a countermodel.

In science, the counterexample is a falsifying observation or experiment.

If a single abstract schema is wanted, it can be written as:

\[\mathrm{NoCounterexample}(X,U,F) \iff \neg \exists u \in U \; F(u,X).\]

Then logic instantiates it as:

\[\mathrm{NoCounterexample}\big(P,\mathcal{M},F_{\mathrm{logic}}\big) \iff \neg \exists M \in \mathcal{M}\; (M \models \Sigma \land M \models \neg P),\]

while science instantiates it as:

\[\mathrm{NoCounterexample}\big(T,E,F_{\mathrm{science}}\big) \iff \neg \exists e \in E\; \mathrm{Falsifies}(e,T).\]

So the common shape is real. The difference comes from what the universe $U$ is.

If the aim is to state the comparison only in ordinary predicate logic, the pair is:

\[\neg \exists m\; \big( \mathrm{AllowedModel}(m) \land \mathrm{SatAll}(m,\Sigma) \land \mathrm{Sat}(m,\neg P) \big)\]

versus

\[\neg \exists e\; \big( \mathrm{PerformedTest}(e,E) \land \mathrm{Falsifies}(e,T) \big).\]

Part VI: where the analogy breaks

The difference can also be written formally.

In logic:

\[\Sigma \models P \iff \neg \exists M \; (M \models \Sigma \land M \models \neg P).\]

So under fixed assumptions, “no counterexample exists” is equivalent to truth relative to $\Sigma$.

In science:

\[\mathrm{Corroborated}(T,E) \iff \neg \exists e \in E \; \mathrm{Falsifies}(e,T)\]

but generally

\[\mathrm{Corroborated}(T,E) \not\Rightarrow \mathrm{True}(T).\]

Why not?

Because $E$ is not the set of all possible future tests.

That can be written as:

\[E \subsetneq E^{*}\]

where $E^{*}$ is the open-ended space of possible tests, measurements, and future experimental conditions.

So the stronger scientific truth condition would be:

\[\neg \exists e \in E^{*} \; \mathrm{Falsifies}(e,T),\]

but science never possesses the whole $E^{*}$ as a completed finite object.

So the contrast in quantifier scope is:

\[\text{Logic: } \forall M \in \mathcal{M}\]

versus

\[\text{Science: } \forall e \in E \quad \text{with} \quad E \subsetneq E^{*}.\]

Logic closes the world by fixing the admissible model class. Science stays open because future observations, new instruments, and new environments can enlarge the effective test set.

That is why science gets corroboration:

\[\neg \exists e \in E \; \mathrm{Falsifies}(e,T),\]

not proof of final truth.

Part VII: one-line comparison

The shortest exact comparison is:

\[\text{Logic: } \neg \exists M \; (M \models \Sigma \land M \models \neg P) \Rightarrow \Sigma \models P.\] \[\text{Science: } \neg \exists e \in E \; \mathrm{Falsifies}(e,T) \Rightarrow \mathrm{Corroborated}(T,E),\]

but not

\[\Rightarrow \mathrm{True}(T).\]

So:

• proof is countermodel elimination in a fixed formal universe,
• corroboration is failed falsification in a currently sampled empirical universe.

Another compact way to write the contrast is:

\[\text{Proof} = \text{no countermodel in the full allowed class}\] \[\text{Corroboration} = \text{no falsifier in the tested subclass}\]

In ordinary predicate logic, the same contrast is:

\[\mathrm{Proof}(\Sigma,P) \iff \neg \exists m\; \big( \mathrm{AllowedModel}(m) \land \mathrm{SatAll}(m,\Sigma) \land \mathrm{Sat}(m,\neg P) \big)\] \[\mathrm{Corroborated}(T,E) \iff \neg \exists e\; \big( \mathrm{PerformedTest}(e,E) \land \mathrm{Falsifies}(e,T) \big)\]

with

\[\exists e\; \big( \mathrm{PossibleTest}(e) \land \neg \mathrm{PerformedTest}(e,E) \big)\]

showing why corroboration is not final truth.

Part VIII: why resolution feels Popperian

Resolution has the same intellectual rhythm as falsification:

1. challenge a claim,
2. push the challenge as far as possible,
3. see whether any surviving counterexample remains.

In formulas, that is:

\[\Sigma \cup \{\neg P\} \vdash_{\mathrm{Res}} \Box\]

versus

\[\neg \exists e \in E \; \mathrm{Falsifies}(e,T).\]

Same adversarial shape.

Different domain.

Different consequence.

One last boundary matters here. Resolution is not merely brute-force enumeration of all truth assignments. It is a syntactic calculus that can compress the search by deriving consequences directly. So the analogy is strongest at the level of adversarial form, not at the level of implementation strategy.

Part IX: the deeper master schema

The two cases can be abstracted one level further.

Let:

• $X$ be the object under attack, a claim, theory, program, or machine,
• $U$ be the searched universe of possible witnesses,
• $B(u,X)$ mean that witness $u$ is bad for $X$.

Then the master schema is:

\[\mathrm{NoBadWitness}(X,U,B) \iff \neg \exists u\; \big(U(u,X) \land B(u,X)\big).\]

This single formula contains all the earlier cases:

Logical proof:

\[\mathrm{Proof}(\Sigma,P) \iff \neg \exists m\; \big( \mathrm{AllowedModel}(m,\Sigma,P) \land \mathrm{Countermodel}(m,\Sigma,P) \big).\]

Scientific corroboration:

\[\mathrm{Corroborated}(T,E) \iff \neg \exists e\; \big( \mathrm{PerformedTest}(e,E) \land \mathrm{Falsifies}(e,T) \big).\]

Safety of a machine:

\[\mathrm{Safe}(M) \iff \neg \exists s\; \big( \mathrm{Reachable}(s,M) \land \mathrm{Disaster}(s) \big).\]

That is the rabbit hole one level down. Truth, corroboration, and safety are all absence-of-bad-witness claims. What changes is the searched universe and the badness predicate.

Part X: soundness, coverage, and why proof is rare

The next layer is not just whether a bad witness was found. It is whether the search was trustworthy.

Two properties matter:

Bad-witness soundness:

\[\mathrm{SoundBadness}(B) \iff \forall u \forall X\; \big( B(u,X) \rightarrow \mathrm{RealDefect}(u,X) \big).\]

Universe coverage:

\[\mathrm{CoversAllRelevantCases}(U) \iff \forall u \forall X\; \big( \mathrm{RealDefect}(u,X) \rightarrow U(u,X) \big).\]

Now the deeper assurance theorem is:

\[\mathrm{SoundBadness}(B) \land \mathrm{CoversAllRelevantCases}(U) \land \neg \exists u\; \big(U(u,X)\land B(u,X)\big) \rightarrow \neg \exists u\; \mathrm{RealDefect}(u,X).\]

This is the stronger backbone underneath proof, verification, testing, and chaos engineering.

• Logic often gets both, because the model class is fixed and the countermodel notion is exact.
• Science rarely gets full coverage, because the set of possible future tests stays open.
• Ordinary software testing rarely gets full coverage either.
• Formal verification can recover coverage, but only relative to a stated model and assumptions.

This is why “no bug found” is not enough. One must ask:

\[\text{No bug found in what searched universe, under what badness predicate?}\]

Part XI: state-space pruning and unreachable disaster states

The same schema becomes especially useful in software and protocol design.

Let $M_{old}$ and $M_{new}$ be two shapes for the same system. If the new shape prunes the reachable state space, one wants:

\[\forall s\; \big( \mathrm{Reachable}(s,M_{new}) \rightarrow \mathrm{Reachable}(s,M_{old}) \big).\]

This says the new shape reaches no states outside the old reachable set. It is a pruning relation.

If, in addition,

\[\neg \exists s\; \big( \mathrm{Reachable}(s,M_{new}) \land \mathrm{Disaster}(s) \big),\]

then the new shape makes disaster states unreachable.

This is the same adversarial form as refutation:

\[\text{safe} \iff \neg \exists (\text{reachable disaster state}).\]

So assurance can often be restated as a reachability problem:

\[\mathrm{Assured}(M) \iff \neg \exists s\; \big( \mathrm{Reachable}(s,M) \land \mathrm{Bad}(s) \big).\]

That is one of the deepest bridges between proof search and system security.

Part XII: chaos engineering as sampled refutation

Chaos engineering fits naturally into the same family.

Let $f$ range over faults, delays, dropped messages, stale oracles, partial partitions, clock skew, and similar disturbances.

An ideal robustness property would be:

\[\mathrm{Robust}(M,F) \iff \neg \exists f\exists s\; \big( \mathrm{InScopeFault}(f,F) \land \mathrm{Reachable}(s,M \oplus f) \land \mathrm{Disaster}(s) \big).\]

This is a closed-world robustness claim over a fixed in-scope fault universe $F$.

But ordinary chaos testing usually establishes only:

\[\neg \exists f\exists s\; \big( \mathrm{InjectedFault}(f,E_F) \land \mathrm{Reachable}(s,M \oplus f) \land \mathrm{Disaster}(s) \big).\]

That is useful, but weaker. The injected faults $E_F$ are a tested subset, not necessarily the whole in-scope fault universe.

So chaos engineering is often Popperian:

• inject failure,
• hunt disaster,
• if no disaster appears, increase confidence,
• but do not confuse sampled survival with universal robustness unless fault coverage is justified.

Part XIII: AI-generated scenarios and automated reasoning

Now bring in language models, search models, or other generative systems.

Assumption D matters here. A generator can enlarge the searched subset. It cannot by itself prove that the full universe has been covered.

Let $G$ be a scenario generator and $H$ be a verifier or checker. Then:

\[\mathrm{GeneratedBy}(u,G,X)\]

means generator $G$ proposed witness $u$ against object $X$, and

\[\mathrm{AcceptedByChecker}(u,H,X)\]

means the checker accepts $u$ as a valid candidate scenario or counterexample attempt.

The searched set induced by the generator-checker pair is:

\[\mathrm{GeneratedUniverse}(u,G,H,X) \iff \mathrm{GeneratedBy}(u,G,X) \land \mathrm{AcceptedByChecker}(u,H,X).\]

Now the AI-assisted refutation loop is:

\[\neg \exists u\; \big( \mathrm{GeneratedUniverse}(u,G,H,X) \land B(u,X) \big).\]

This can be very powerful. It increases the rate at which candidate counterexamples are produced and tested.

But it is not yet proof.

To get proof, one needs something like:

\[\forall u\; \big( \mathrm{Relevant}(u,X) \rightarrow \mathrm{GeneratedUniverse}(u,G,H,X) \big),\]

or some other argument that the generator-checker pipeline covers all relevant cases.

Without that, the correct conclusion is:

\[\mathrm{NoBadWitnessFoundInGeneratedSet}(G,H,X),\]

not:

\[\mathrm{NoBadWitnessExists}(X).\]

So the right way to think about AI here is:

• it can synthesize candidate tests,
• it can mutate fault scenarios,
• it can generate attacker moves,
• it can propose conjectures and proof obligations,
• it can focus search where bad witnesses are more likely,

but the checker, solver, model checker, or theorem prover still determines what counts as a valid witness or valid proof step.

In that sense, a model can be a search-expansion operator:

\[\mathrm{SearchExpansion}(G,X) \iff \forall U_0\; \exists U_1\; \big( U_0 \subseteq U_1 \land \mathrm{UsefulForFindingBadWitnesses}(U_1,X) \big).\]

That is a strong practical role, even though it is not the same as formal completeness.

Part XIV: the deepest split, witness search versus witness elimination

At the bottom of the rabbit hole, two modes appear.

Witness search:

\[\exists u\; \big(U(u,X)\land B(u,X)\big)\]

Witness elimination:

\[\neg \exists u\; \big(U(u,X)\land B(u,X)\big)\]

Most testing, science, red-teaming, and chaos engineering live on the search side. They try to produce a witness.

Proof and full verification live on the elimination side. They justify the universal absence of such a witness, relative to a fixed universe and assumptions.

So the deepest compact summary is:

\[\mathrm{Assurance}(X) \text{ rises as } \mathrm{Coverage}(U) \text{ and } \mathrm{Soundness}(B) \text{ rise, while } \exists u(U(u,X)\land B(u,X)) \text{ is driven toward false.}\]

That sentence is the shared spine behind:

• resolution,
• Popperian falsification,
• theorem proving,
• model checking,
• software verification,
• state-space pruning,
• red-teaming,
• chaos engineering,
• AI-assisted counterexample generation.

Part XV: alternating quantifiers, adversaries, and synthesis

The next depth is reached when the witness is not just searched for, but chosen by an adversary against a system response.

For a controller $C$ facing an environment $E$, safety can be written as:

\[\forall e\; \big( \mathrm{AllowedEnvMove}(e) \rightarrow \neg \exists s\; \big( \mathrm{ReachableUnder}(s,C,e) \land \mathrm{Disaster}(s) \big) \big).\]

This means every allowed environment move still leaves no reachable disaster state.

But synthesis problems often have alternating quantifiers:

\[\exists C\; \forall e\; \neg \exists s\; \big( \mathrm{ReachableUnder}(s,C,e) \land \mathrm{Disaster}(s) \big).\]

Read it as:

there exists a controller such that for every allowed environment behavior, no disaster state is reachable.

That is deeper than plain falsification. It is not just:

\[\neg \exists (\text{bad witness})\]

It is:

\[\exists (\text{defense})\; \forall (\text{attack})\; \neg \exists (\text{disaster witness}).\]

This is where verification shades into synthesis and game theory.

Part XVI: fixed points, reachability, and model checking

Reachability itself can be defined recursively.

Let $\mathrm{Init}(s)$ mean $s$ is an initial state and $\mathrm{Step}(s,t)$ mean the machine can move from $s$ to $t$.

Then reachable state is the least fixed point:

\[\mathrm{Reachable}(t) \iff \mu R.\; \Big( \mathrm{Init}(t) \lor \exists s\; (R(s)\land \mathrm{Step}(s,t)) \Big).\]

This says the reachable set is the smallest set containing the initial states and closed under the step relation.

Now safety is:

\[\neg \exists s\; \big( \mathrm{Reachable}(s) \land \mathrm{Bad}(s) \big).\]

In temporal logic notation, the same claim is often written:

\[\mathbf{AG}\; \neg \mathrm{Bad}\]

and the violation is:

\[\mathbf{EF}\; \mathrm{Bad}.\]

So one more rabbit-hole layer is:

• refutation in clause logic,
• nonexistence of countermodels in semantics,
• nonreachability of bad states in transition systems,
• temporal invariance in modal logic,
• least fixed points underneath the reachability relation.

These are not identical notations, but they preserve the same adversarial structure.

Part XVII: AI generators as witness proposal distributions

A generator usually does not enumerate the whole witness space uniformly. It induces a distribution over candidates.

Let $G(u \mid X)$ be the probability or score that generator $G$ proposes witness $u$ against object $X$.

Then the expected bad-witness yield is:

\[\mathrm{Yield}(G,X) := \sum_u G(u \mid X)\cdot \mathbf{1}_{B(u,X)}.\]

If the witness space is continuous, replace the sum with an integral.

This does not prove safety. It measures how aggressively the generator concentrates on plausible defects.

A stronger target is coverage over a witness family $W$:

\[\forall u\; \big( W(u,X) \rightarrow \Pr[G \text{ proposes } u \mid X] > 0 \big).\]

That says every relevant witness in family $W$ is at least reachable by the generator.

Then a checker can be required to be sound:

\[\forall u\; \big( \mathrm{AcceptedByChecker}(u,H,X) \rightarrow \mathrm{ValidScenario}(u,X) \big).\]

Putting the two together gives a disciplined AI-assisted search story:

\[\text{generator for breadth} \land \text{checker for validity} \land \text{solver or runtime for verdict}.\]

This is why models are useful in chaos engineering and automated reasoning. They can bias the search toward semantically rich or attacker-like witnesses that a blind enumerator would reach much later.

But the same warning remains:

\[\mathrm{HighYield}(G,X) \not\Rightarrow \mathrm{Completeness}(G,X).\]

Good generation improves search power. It does not erase the closed-world versus open-world distinction.

Part XVIII: how actions perturb the shape of a world model

To go deeper, one should distinguish the world itself from the agent’s world model.

Let the agent’s current possibility set be $\Omega_t$. Let action $a$ be taken and observation $o$ be received. Then a standard logical update is:

\[\Omega_{t+1} = \big\{ w' \mid \exists w\; (\Omega_t(w)\land \mathrm{Step}(w,a,w')) \big\} \cap \big\{ w' \mid \mathrm{ObsCompatible}(w',o) \big\}.\]

This says:

• action pushes the possibility set forward through the transition relation,
• observation cuts the pushed set back down.

So action perturbs the shape of the world model in at least four distinct ways.

State translation:

\[\Omega_{t+1} = \mathrm{Post}_a(\Omega_t)\]

Expansion of reachability:

\[\exists w'\; (\Omega_{t+1}(w') \land \neg \Omega_t(w'))\]

Contraction by information:

\[\Omega_{t+1} \subseteq \Omega_t\]

Boundary deformation:

\[\partial \Omega_{t+1} \neq \partial \Omega_t\]

if one thinks geometrically about which regions of possibility space remain admissible.

The safest actions are the ones that shrink the bad region of the reachable shape:

\[\forall s\; \big( \mathrm{Reachable}(s,M_{after}) \rightarrow \mathrm{Reachable}(s,M_{before}) \big)\]

and ideally also:

\[\neg \exists s\; \big( \mathrm{Reachable}(s,M_{after}) \land \mathrm{Bad}(s) \big).\]

So an action perturbs the world model not only by moving a current state, but by changing the future geometry of reachability, observation, and exclusion.

Part XIX: the deepest shared idea, elimination of impossible worlds

The deepest common idea behind resolution and Popper is not merely “testing.” It is elimination of impossible worlds.

Start with a universe of possibilities $U_0$. Each constraint $c$ defines a survivor operator:

\[I_c(X) := \{u \in X \mid \mathrm{Passes}(u,c)\}.\]

This operator is:

Monotone:

\[X \subseteq Y \rightarrow I_c(X) \subseteq I_c(Y)\]

Anti-extensive:

\[I_c(X) \subseteq X\]

Idempotent:

\[I_c(I_c(X)) = I_c(X)\]

After constraints $c_1,\dots,c_n$, the survivor set is:

\[U_n = I_{c_n}(\cdots I_{c_2}(I_{c_1}(U_0))\cdots) = \{u \in U_0 \mid \forall i \le n,\; \mathrm{Passes}(u,c_i)\}.\]

This is the monotone shrinking core shared by:

• refutation,
• falsification,
• verification,
• red-teaming,
• chaos experiments,
• guarded execution,
• formal proofs of unreachability.

Resolution under $\neg P$ drives the model survivor set to empty:

\[U_0 := \{M \mid M \models \Sigma \land M \models \neg P\}\] \[U_n = \varnothing \rightarrow \Sigma \models P.\]

Popperian science shrinks a theory survivor set:

\[H_n = \{T \in H_0 \mid \forall e \in E_n,\; \neg \mathrm{Falsifies}(e,T)\}.\]

The same mathematical gesture is happening. Possibility space is being carved down by constraints.

Part XX: deeper than Popper, knowledge as shrinking support

One can go even deeper and remove “theory” and “model” entirely.

Let $X_t$ be the support of what remains live at time $t$. Then:

\[X_{t+1} = X_t \cap C_t\]

where $C_t$ is the set of candidates surviving the next constraint.

Equivalently:

\[X_t = \bigcap_{i \le t} C_i.\]

This is the pure elimination form.

In that sense, knowledge growth is often:

\[\text{more knowledge} = \text{smaller live possibility set}.\]

This is why proof, diagnosis, debugging, and scientific testing all feel similar from inside. They reduce what can still be the case.

Part XXI: is this universal Darwinism?

Not exactly.

There is a real relation, but one should separate:

• elimination,
• selection,
• optimization,
• replication and variation.

Darwinian dynamics require at least variation, heredity, and differential survival or reproduction.

A minimal selection equation looks like:

\[p_{t+1}(x) = \frac{p_t(x)\, f_t(x)}{\sum_y p_t(y)\, f_t(y)}\]

where $p_t(x)$ is the population share of type $x$, and $f_t(x)$ is its fitness.

With mutation or variation:

\[p_{t+1}(x) = \frac{\sum_y p_t(y)\, f_t(y)\, K_t(y,x)}{Z_t}\]

where $K_t(y,x)$ is the variation kernel and $Z_t$ is the normalizing constant.

That is not what resolution does.

Resolution has elimination without reproduction:

\[X_{t+1} = X_t \cap C_t.\]

Popperian falsification also has elimination without heredity:

\[H_{t+1} = H_t \cap C_t.\]

Darwinian evolution is more like:

\[H_{t+1} = \mathrm{Select}_t(\mathrm{Vary}_t(H_t)).\]

So the right conclusion is:

• resolution and Popper share a negative-selection shape,
• Darwinism contains that shape as one component,
• but Darwinism also adds replication, mutation, and path-dependent population dynamics.

So this is not identical to universal Darwinism. It is more general than that.

Part XXII: is this evolutionary optimization?

Also not exactly, unless badness can be reduced to thresholded objective failure.

Optimization usually has an objective:

\[x^* \in \arg\max_{x \in X} J(x)\]

or

\[x^* \in \arg\min_{x \in X} J(x).\]

By contrast, witness elimination only needs a badness predicate:

\[\neg \exists x\; (X(x)\land B(x)).\]

The two coincide only if:

\[B(x) \leftrightarrow J(x) < \tau\]

for some threshold $\tau$.

So:

• proof is usually not optimization,
• falsification is usually not optimization,
• safety is usually not optimization,
• but optimization can be encoded as elimination if one turns “below threshold” into the badness predicate.

This matters because many systems do not maximize a single scalar objective. They satisfy constraints, maintain invariants, and avoid disaster.

Part XXIII: the more universal pattern, expand and prune

A deeper common pattern than Darwinism is:

\[X_{t+1} = I_t(E_t(X_t))\]

where:

• $E_t$ expands, varies, proposes, or explores,
• $I_t$ prunes, rejects, falsifies, or guards.

Examples:

Evolution:

\[E_t = \mathrm{mutation/recombination}, \qquad I_t = \mathrm{selection}\]

Science:

\[E_t = \mathrm{new\ theories\ and\ new\ tests}, \qquad I_t = \mathrm{falsification}\]

Theorem proving:

\[E_t = \mathrm{branch\ or\ derive}, \qquad I_t = \mathrm{discard\ inconsistent\ branches}\]

AI-assisted chaos engineering:

\[E_t = \mathrm{generate\ scenarios}, \qquad I_t = \mathrm{checker\ plus\ runtime\ verdict}\]

Secure protocol shaping:

\[E_t = \mathrm{all\ executable\ traces}, \qquad I_t = \mathrm{guards,\ invariants,\ reject\ paths}\]

This pattern is more universal than Darwinism because it covers systems with no heredity and no reproduction.

Part XXIV: the bottom of the rabbit hole

At the deepest level reached here, the shared logic is:

\[\text{understanding} = \text{controlled elimination of live alternatives}\]

with three questions always present:

1. What is the universe of possible witnesses?
2. What counts as a bad witness?
3. Does the search really cover the relevant universe?

In formulas, that becomes:

\[\mathrm{Assurance}(X) \iff \mathrm{SoundBadness}(B) \land \mathrm{Coverage}(U) \land \neg \exists u\; \big(U(u,X)\land B(u,X)\big).\]

And when synthesis enters, it becomes:

\[\exists d\; \forall a\; \neg \exists u\; \big( \mathrm{Attack}(a) \land \mathrm{Witness}(u,d,a) \land \mathrm{Bad}(u) \big).\]

That is the form behind:

• controller synthesis,
• security design,
• protocol hardening,
• fail-closed guards,
• and any architecture whose purpose is to make disaster witnesses impossible.

So the deepest statement I would defend is this:

\[\text{logic, science, security, and adaptation all traffic in witness spaces}\]

and progress often means:

\[\text{compress the live witness space without accidentally deleting the truth.}\]

That is why abstraction, proof, falsification, scenario generation, guards, and world-model updates all feel connected. They are all operations on what is still allowed to survive.

Takeaway

If the goal is to say it in logic, the central formulas are these:

\[\Sigma \models P \iff \neg \exists M \; (M \models \Sigma \land M \models \neg P)\] \[\Sigma \cup \{\neg P\} \vdash_{\mathrm{Res}} \Box \Rightarrow \Sigma \models P\] \[\mathrm{Corroborated}(T,E) \iff \neg \exists e \in E \; \mathrm{Falsifies}(e,T)\] \[\mathrm{Safe}(M) \iff \neg \exists s\; \big( \mathrm{Reachable}(s,M) \land \mathrm{Disaster}(s) \big)\]

and the crucial asymmetry is:

\[\mathrm{Corroborated}(T,E) \not\Rightarrow \mathrm{True}(T).\]

That is the clean formal statement of the idea:

Resolution is falsification inside a closed formal world. Science is falsification inside an open empirical world.