Intercognix № 0016 · entered into the Intercognix Catalogue, anno 2026
The Deadline That Carries the Claim
Why the people who prove that programs behave were forced, fifty years ago, to divide every claim about a running system into the kind a finite watch can refute and the kind it can only confirm — while a clinical trial still chooses its endpoint, and its follow-up, as if the two were one kind.
Candidate · UnvalidatedI.The First Known Thing — the two kinds of promise a running system can make
concurrency theory · what it means for a program that never stops to be correct
A program that computes a value and halts can be judged by its answer. A program that is not meant to halt — an operating system, a network protocol, a controller in a lift — cannot, because there is no answer, only behaviour, and the behaviour is an infinite sequence of states. In 1977 Leslie Lamport, working out how to prove such programs correct, found that every claim anyone wanted to make about them fell into one of two kinds, and he named them from the vocabulary of Petri nets. A safety property says that nothing bad ever happens: two processes are never in the critical section at once, the account is never overdrawn, the lift door never opens between floors. A liveness property says that something good eventually happens: every request is eventually served, the message is eventually delivered, the program eventually terminates. Partial correctness — if it halts, the answer is right — is safety. Termination is liveness. Total correctness is the two together.
the distinction that turned out to be about observation
The pair might have stayed a taxonomy of convenience. In 1985 Bowen Alpern and Fred Schneider made it a theorem, and the theorem is about what a finite observer can know. A property is a safety property exactly when any violation of it shows up in some finite stretch of the run: a bad thing happens at an identifiable moment, and nothing the system does afterwards can undo it. A property is a liveness property exactly when no finite stretch of the run can ever violate it: however long you have watched without the good thing happening, the run can still be continued so that it does. From this the consequences follow mechanically. A finite observation can refute a safety property but never confirm one, since the bad thing may yet come. A finite observation can confirm a liveness property but never refute one, since the good thing may yet come. And any deadline turns the second kind into the first: the request is served within ten seconds is a safety property, because the ten seconds can elapse. Topologically — the observation is credited to Gordon Plotkin — safety properties are the closed sets of runs and liveness properties are the dense ones, and every property is the intersection of one closed set and one dense set. That is the decomposition theorem: any claim whatsoever about a running system is the conjunction of exactly one safety part and exactly one liveness part, and the two parts can be separated.
and what the field does with it
The field does not treat this as philosophy. It sets the division of labour. Safety is checked by monitoring: a finite automaton watches the prefix and raises the alarm at the violating step, and testing, which only ever sees finite runs, can find only safety bugs. Liveness cannot be tested at all; it is established by proof, under explicit assumptions about fairness, or it is bounded and thereby turned into safety and handed to the monitor. The engineer who writes a bounded version knows what has been done. The bound is not part of the requirement; it is a concession to the observer, and the whole content of the original promise now lives in the choice of the number, which the requirement never contained.
II.The Second Known Thing — the endpoint and its follow-up
drug discovery · disease definition, indication choice and endpoint selection
Walk to a hall where nothing runs forever, because the patients do not. A programme that has chosen its indication must next choose the thing it will measure, and the choice is understood to be the most consequential in the trial. The endpoint decides the sample size, the duration, the cost, and very often whether the drug is approved at all. The field sorts endpoints by several axes it has worked out carefully: hard against surrogate, clinical against biomarker, single against composite, continuous against binary against time to event. Since 2019 the ICH E9(R1) addendum has added the estimand, requiring a sponsor to say in advance what happens to the measurement when a patient dies, drops out or takes rescue medication. Every one of these axes is about what is measured and in whom. None of them is about the shape of the promise the measurement stands in for.
the two shapes, unnamed
Look at the endpoints themselves. Overall survival is a claim that a bad thing does not happen; progression-free survival is a claim that one of two bad things does not happen; the safety endpoint of every trial — the adverse-event tally — is the same shape again. Each is refuted per patient at an identifiable moment and can never be confirmed per patient, only carried forward as a censoring. Objective response, complete remission, seroconversion, healing of an ulcer, a fall of a fixed size in a symptom score: these are claims that a good thing happens, and they run the other way. Each is confirmed per patient at an identifiable moment and can never be refuted per patient — only carried forward as a non-response, which is why the standing convention for a patient who leaves before the assessment is to count them as having failed. The field calls that non-responder imputation and treats it as a conservative choice about missing data. It is also the exact treatment a monitor gives to a liveness promise at its deadline.
and where the deadline is chosen
Every response endpoint has a deadline, because a trial ends. Response by week twelve; complete remission at end of induction; best overall response by the data cut-off. The oncology criteria in general use require a response to be confirmed at a second assessment four weeks or more after the first, which is itself a small deadline nested inside the large one. The deadline is set by precedent, by the regulator's expectation and by the cost of following patients longer. It is rarely defended on the ground that the promise the drug is making has been stated and the deadline chosen to test that promise, and the field's own record shows the consequence. Response rate is the endpoint behind most accelerated approvals in oncology, and the audits of those approvals — which record, drug by drug, the endpoint of the pivotal trial and the outcome of the confirmatory one — find that fewer than half go on to show benefit on a longer horizon. The explanation the field gives is that response is a surrogate. That is true. It is also incomplete, since progression-free survival is a surrogate too, and it is a claim of the other shape.
III.The Bridge
no endpoint guidance cites Lamport
The halls share nothing. Concurrency theory and clinical endpoint selection have no common literature and no reviews spanning them. Temporal logic has been carried into medicine, but to write down protocols and guidelines precisely and check them for contradiction; it has not been used to ask what kind of claim an endpoint is, and the trialists' vocabulary — surrogate, landmark, durable, censored — was built without the theorem. But both halls are trying to judge, from a finite watch, a promise about a course of events that outlasts the watch, and one of them proved what a finite watch can and cannot do.
X: what a finite watch can refute it cannot confirm, and the deadline is where the rest of the claim goes
Call it prefix refutability. A claim about a course of events is of one of two kinds and not both. Either a finite stretch of observation can refute it and none can confirm it — nothing bad happens — or a finite stretch can confirm it and none can refute it — something good happens. Every claim is the conjunction of one part of each kind, and a deadline is the operation that turns the second kind into the first. From which follows the half that the clinic has not ported, because only the verifiers have had to say exactly what a bounded promise is a promise of: a finite trial can adjudicate only claims of the first kind, so wherever the clinical claim is of the second kind — the patient responds, the disease is arrested, the remission holds — the endpoint is not that claim but its image under a chosen deadline, and the deadline carries whatever part of the claim the endpoint no longer states. The between-arm difference in such an endpoint is a difference in the proportion who have reached the good thing by a date. A drug that makes the good thing happen sooner and a drug that makes it happen at all produce the same number at a well-chosen date and different numbers at every other, and nothing in the endpoint's definition distinguishes them. Non-responder imputation is not a missing-data convention. It is the deadline doing its work on the patients the watch did not reach.
IV.The Question That Becomes Possible
neither discipline would ask this alone
The field already records more than one deadline. Response is assessed at scheduled visits, time to response is recorded, and the cumulative proportion responding in each arm is available from the data set even where only one date is reported. What is not done is to treat the between-arm difference as a function of the deadline and read off its slope at the date the protocol chose — whether the gap between the arms is still opening, has settled, or has begun to close because the control arm is arriving late.
the deadline hypothesis
For endpoints of the confirmable kind, does the slope of the between-arm difference at the protocol's deadline — whether the gap is opening, settled or closing — predict which effects survive a longer horizon, and does it do so where the endpoint's status as a surrogate does not?
why it would matter
Because the two things a response endpoint conflates come apart in a direction that can be checked. A gap that has settled by the deadline is an effect on whether; a gap that is closing is an effect on when, and the deadline has caught it at its widest. Under the mechanism the confirmatory failures that look inexplicable — a large response advantage that becomes no survival advantage — should concentrate among trials whose gap was closing at the cut-off, and should be rare among trials whose gap had settled, regardless of the fact that both used the same surrogate. The decomposition theorem also does something to composite endpoints, which the field builds by hand and argues about by component. Any composite — alive, in remission and free of rescue at one year — separates cleanly into a part of the refutable kind and a part of the confirmable kind, and only the first part can be read at an interim analysis without a deadline being smuggled in. A data monitoring committee that stops a trial early for efficacy on a composite has stopped it on the safety part and assumed the rest. That is a quantity that can be computed from a protocol. It is not currently computed from anything.
V.How It Could Be Proven — or Broken
a candidate must be breakable, or it is merely poetry
An intercognix candidate earns nothing until it names its own test. This one is retrospective first, and the data for it sits in trial registries and in the audits already published by people asking a neighbouring question.
What would support it
Take the accelerated approvals granted on a response endpoint whose confirmatory outcome is now on the record, and alongside them the randomised trials in any area that reported a response-type primary endpoint and later reported a longer-horizon outcome on the same population. For each, recover the cumulative response curve in each arm — from the time-to-response data where published, from the scheduled-visit response rates where not — and compute the slope of the between-arm difference at the protocol's deadline, classifying each trial blind to its later outcome as opening, settled or closing. Support looks like this: the closing trials are the ones whose effect shrinks or vanishes on the longer horizon, the settled trials are the ones whose effect holds, and the classification discriminates within the surrogate class — among response-based approvals alone — where surrogacy, which every one of them shares, cannot. The prospective version is cheaper here than in most halls: it asks only that a sponsor pre-register the response curve at all scheduled visits and the slope at the deadline, and wait for the confirmatory trial it was going to run anyway.
What would break it
It breaks first, and most likely, by collapse. If the slope at the deadline is nearly a monotone function of the duration of response the field already reports, or of the cure fraction a mixture model already estimates from the time-to-event data, then prefix refutability has renamed a measure in use and added nothing; this is the outcome to expect if a closing gap and a short duration of response are always the same patients seen from two sides. It breaks second on measurement: response is assessed at a handful of visits with wide intervals, and if the slope cannot be estimated at ordinary sample sizes with enough precision to classify a trial, the quantity exists and cannot be read. It breaks third, and most interestingly, on the disanalogy at its centre. In verification a deadline is a concession to the observer and carries no value of its own. In medicine sooner can be the whole benefit — an analgesic that works in an hour rather than a day has done what was asked — and if the closing trials replicate as well as the settled ones on a horizon the patients care about, then the deadline was not carrying a claim it failed to state, the clinic was right to price acceleration, and the theorem has nothing to teach it.
the honest status
Note the narrowness. The claim is about endpoints of the confirmable kind that stand in for an eventual state — response for durable control, remission for cure, arrest for modification — and about a slope that should be read off them at the date the protocol chose. It says nothing about endpoints whose promise is speed, where the deadline is the claim and the theorem is silent. It makes no judgement about any drug: a closing gap is a real effect on a real quantity, and the candidate says only that it is an effect on a different quantity from the one the approval was written for. It offers no new endpoint, and it should not, since the theorem's whole content is that a finite trial has no other kind of endpoint available to it; what it offers is a number to attach to the deadline the trial was going to set regardless. And a caution about words: the verifiers' safety is not the trialists' safety, and the coincidence is a hazard rather than a bridge — a survival endpoint is a safety property in Lamport's sense and an efficacy endpoint in the clinic's, and a reader who conflates the two has understood neither hall. Until a set of response curves has been sloped at their deadlines and set against their confirmatory outcomes, this remains exactly what its stamp says: a candidate. A structural echo between two halls of the library, waiting for someone with the tools of both to walk the corridor.
- Specimen
- Intercognix № 0016 — The Deadline That Carries the Claim
- Hall A
- Concurrency theory and formal verification (Lamport's safety and liveness properties, the Alpern–Schneider decomposition, finite-prefix refutability, bounded liveness, the closed-and-dense characterisation)
- Hall B
- Drug discovery — disease definition, indication choice and endpoint selection (response and time-to-event endpoints, non-responder imputation, composite endpoints, follow-up duration, confirmatory trials after accelerated approval)
- The bridge (X)
- Prefix refutability — a claim about a course of events is either refutable by a finite watch and never confirmable, or confirmable and never refutable, and a deadline converts the second kind into the first; so a finite trial adjudicates only the first kind, and wherever the clinical claim is of the second, the endpoint is its image under a chosen deadline and the deadline carries whatever the endpoint no longer states
- Emergent question
- For endpoints of the confirmable kind, does the slope of the between-arm difference at the protocol's deadline — opening, settled or closing — predict which effects survive a longer horizon, where the endpoint's status as a surrogate does not?
- Method
- Surfaced via cross-domain semantic proximity; drafted with an advanced language model; framed and curated by the author
- Status
- Candidate — unvalidated. Awaiting prior-art review and empirical testing
- Entered
- Anno 2026
Intercognix