Assumption Ledger¶
Tracking artifact — instantiates Contradiction-Closure Proof
A running two-column register that keeps temporary assumptions apart from accepted premises and tags each derived line with what it depends on, so nothing sneaks into the conclusion.
Assumption Ledger is bookkeeping, not reasoning. It is a live register — two columns and a dependency tag — maintained alongside a proof so that at every moment you can answer one question: is this fact something we accepted, or something we only supposed for the sake of argument? An indirect proof runs on a temporary falsehood (the negation of the claim), and its single most dangerous failure is that this temporary supposition quietly gets treated as established, or that the accepted premises are themselves inconsistent and the "contradiction" comes from them rather than the supposition. The ledger prevents both by physically separating the two categories and by tagging each derived line with the exact set of lines it leaned on, so that when the proof closes you can read off whether the impossibility truly traces back to the supposition. It never draws an inference; it only records where every inference's authority came from.
Example¶
A team is building a safety case for an avionics autopilot, arguing that "the aircraft can never enter mode M with the flaps retracted." They run it as an indirect argument and keep an Assumption Ledger. The accepted column holds the certified facts: the sensor interlock spec, the mode-transition table, the flap-position invariant. The supposed column holds exactly one temporary entry: "the system is in M with flaps retracted." As the engineers derive consequences, each new line gets a dependency tag — "line 7 depends on {interlock spec, supposition}." When they reach a line that violates the mode-transition table, the ledger shows that line depends on the supposition, not solely on the accepted facts.
That tag is what makes the closure trustworthy. Without the ledger, a reviewer months later cannot tell whether the violation exposed a real impossibility or was baked into two accepted specs that already contradicted each other. With it, the audit trail says precisely which premises and which supposition each step used — and, crucially, that the certified facts alone were consistent.
How it works¶
- Two columns, kept apart. Accepted premises on one side, temporary suppositions on the other; the barrier between them is the point of the artifact.
- Dependency tags. Every derived line records the set of prior lines (accepted and supposed) it was inferred from, so provenance is explicit.
- Consistency spot-check on the accepted side. Before trusting any contradiction, confirm the accepted column alone does not already clash — otherwise the impossibility is meaningless.
- Discharge marking. When the supposition is rejected, the ledger marks it discharged and records which conclusion that licensed, leaving a clean trail.
Tuning parameters¶
- Dependency granularity — tag whole premise-sets or individual axioms. Fine tags localize blame precisely but cost effort on every line.
- Consistency-check depth — a quick sanity read of the accepted column versus a formal satisfiability check before proceeding. Deeper checks catch a poisoned premise base but slow the work.
- Retention scope — keep only live lines or archive discharged ones too. Archiving supports later audit but bloats the record.
- Formality — a margin annotation, a spreadsheet, or a structured proof-log format. More structure aids downstream tools; less suits a quick argument.
When it helps, and when it misleads¶
Its strength is that it makes assumption discipline auditable, echoing the scoped-assumption bookkeeping of Fitch-style proof[n1]: the ledger is where "keep the temporary assumption temporary" stops being advice and becomes a checkable record, and it is the cheapest defense against a contradiction smuggled in from an inconsistent premise base.
Its failure mode is that a ledger records provenance without judging validity: it will faithfully tag a line whose inference was invalid, and it cannot tell you the accepted premises are wrong — only that a step used them. A meticulous ledger can therefore lend confidence to an unsound proof, and over-detailed tagging can bury the one dependency that matters. The guarding discipline is to pair the ledger with an actual check that the accepted column is consistent, and to remember that the ledger certifies where a step came from, never that it was correct.
How it implements the components¶
Assumption Ledger realizes the provenance-and-separation side of the archetype:
negated_assumption_frame— the supposed column holds the negation as an explicitly temporary, quarantined entry, never merged into accepted fact.accepted_premise_base— the accepted column is the curated, consistency-checked set of premises the derivation may draw on.proof_audit_record— the dependency tags and discharge marks are the durable trail a later reviewer reads to reconstruct the proof.
The ledger records dependencies but does not itself derive the consequences or define what counts as the contradiction (derivation_path, contradiction_criterion) — that is Natural Deduction Proof Tree; the ledger annotates the derivation from the outside.
Related¶
- Instantiates: Contradiction-Closure Proof — supplies the assumption-separation and provenance trail the archetype's invariants demand.
- Sibling mechanisms: Reductio Proof Template · Natural Deduction Proof Tree · Contradiction Search Checklist · Minimal Unsat Core Analysis · Case-Split Elimination Table · Peer Proof Review · Proof Assistant Script · Unsatisfiability Certificate
Editorial Notes¶
Form Classification¶
Form family: Record, Log & Register
Rationale: A running two-column register that keeps temporary assumptions apart from accepted premises and tags each derived line with what it depends on, so nothing sneaks into the conclusion, making its operative form a durable account of actual events, decisions, or transitions whose value depends on history or provenance.
Independent corroboration: The frozen evidence defines Assumption Ledger as 'A running two-column register that keeps temporary assumptions apart from accepted premises and tags each derived line with what it depends on, so nothing sneaks into the conclusion', so its operative form is Record, Log & Register.
Review outcome: Independent reviewer agreement; high confidence.
Origin Attribution¶
Primary origin: Mathematics
Origin pattern: Single lineage
Present-day reach: Multi-domain
Rationale: Formal logic and natural-deduction proof practice, especially Fitch-style assumption scope, supply the dependency ledger's structure.
Related originating lineages:
- Philosophy — Philosophical logic developed the distinction between granted premises and temporary suppositions.
Review resolution: Both reviewers identify mathematical proof practice as primary and philosophy as the relevant alternate. The ledger travels broadly because explicit premises support many kinds of reasoning, but that reach does not create multiple independent origins or make the artifact Encyclopedia-authored.
Review outcome: Reconciled after independent review; high confidence.
Notes¶
[n1] Fitch notation, devised by Frederic Fitch, records natural-deduction proofs with vertical bars marking the scope of each assumption, so that a formula's dependence on temporary hypotheses is visible on the page. The ledger generalizes that scoping idea into an explicit dependency record. ↩