Asserting a claim takes a breath; checking one can take an essay. The asymmetry is well studied — Sperber calls the checking side epistemic vigilance — and unexamined claims pile up wherever talk is cheap, which is everywhere. The proper machinery for evaluating arguments is heavy, and nobody deploys it mid-conversation. I wanted a test you could run on a single claim in a single sitting. That test became a paper, the paper acquired a machine-checked core, and somewhere along the way the framework failed its own test and had to be repaired in print.
The move
Every claim leans on more than it states. Toulmin called the unstated licence that carries you from evidence to conclusion the warrant; I call it the load-bearing assumption: the thing such that if it goes, the claim goes with it. The Trident fixes on that one assumption and asks what its defender does with it when challenged. Four postures cover the ground: hold it and accept wherever extending it leads; drop it; suspend it, declining to affirm or deny; or blur it, keeping the word while loosening the meaning until no counterexample can find purchase. (A fifth posture, defending the assumption with further grounds, opens the Agrippan regress; the tool brackets it deliberately.)
Pressed, the postures produce three failures. Hold a warrant and extend it into something you are committed to rejecting, and you land in reductio-incoherence (F1). Drop or suspend a warrant the claim genuinely needed, and the claim loses its support (F2). Blur it, and the claim becomes compatible with every outcome, safe and empty (F3); the internet knows this manoeuvre as the motte-and-bailey. None of the forks is my invention (the reductio is Socratic, retraction costs are Hamblin's, immunising vagueness runs from Popper through Shackel); the contribution is the integration: one extracted assumption, three old failure modes, runnable in a sitting.
One worked example
Take the health-food staple: it is natural, so it is good for you. The load-bearing assumption is that naturalness transmits goodness. Hold: arsenic, botulism, and cholera are impeccably natural, so the extended warrant drags those endorsements along — Fork 1. Drop: nothing now connects natural to good; the claim hangs unsupported — Fork 2. Suspend (“I'm not saying nature is always good, I'm just asking questions”) does identical damage, since a withheld premise is as unavailable as a denied one. Blur: “truly natural things are good”, where “truly natural” quietly excludes each counterexample, until the claim forbids nothing — Fork 3.
But failure is not compulsory. The claimant can bite the bullet, coherent if alarming at dinner parties. She can block the inference, denying for stated reasons that naturalness extends to pathogens. Or she can notice the claim never needed the warrant and discard it. Each is survival. A test that cannot be passed is not a test; it is a mood.
What the machine bought
The founding sketch claimed the three forks exhaust the available responses; the survivals above refute it, and I found out by running the tool on itself. The framework's central claim rests on an undefended assumption of its own — that the posture inventory is complete and every posture ends in a fork — and pressed on its own prongs it failed two of them, booking the coherent bullet-biter as a reductio failure and reclassifying every counterexample away. A diagnostic for underdefined claims that ships with an underdefined claim has no standing to issue verdicts, so the paper records the repair rather than hiding the wound.
The repair is where formalisation earns its keep. Separate what a claimant does (the posture) from what the audit says (the verdict), make the contestable facts explicit, and three binary facts against four postures give thirty-two cases — enumerated outright in a Lean 4 core, no external libraries, every theorem closed by the decide tactic. Under two explicit scope conditions it proves the corrected claim: the failure outcomes are exactly the three forks, each reachable, nothing outside them, with survival a genuine further outcome. And three is explained rather than stipulated: dropping and suspending do identical damage to a claim's support, so four postures collapse to three failure cells.
The proof settles a property of the verdict map, not of the world. It does not establish that the posture inventory is complete; that stays an assumed, load-bearing scope condition — the Trident's own Fork 3 turned inward. The adversarial pass surfaced one candidate for a missing move, refine: precisify the assumption and narrow its scope, the opposite of blurring. It recurses rather than terminates, so the trichotomy survives while the response space becomes a tree. There may be others. I cannot prove there are not, and saying so is the whole point.
Where this goes
The part I now find most interesting is not the trident but the genre. The paper audits itself: it runs the tool on its own warrant, fails, prints the repair, and ships a machine-checked ledger of what got proved and what stayed assumed — a self-auditing formal paper. Most papers have a load-bearing assumption somewhere in section 2 that nobody, least of all the author, has pressed; the tooling for pressing it is now cheap. Whether the format scales past tiny cores is open, but the direction feels right: fewer papers asserting their own soundness, more checking what they can and labelling what they cannot.
Away from the seminar room the recipe is unchanged: find the assumption the claim cannot do without, press it, and watch which of the three doors the defence goes through.
The paper is “The Trident: A Trilemmatic Diagnostic for Claim Analysis” (Dissensus working paper DAI-2607); the Lean core and Python enumeration will be released alongside it.