sec-internal-logic
0.12 Internal logic: infinitesimals, subobjects, and interventions
There is a shared logical feature behind two constructions used later in the book. Synthetic differential geometry represents first-order variation by the infinitesimal object
while sheaf- and topos-based causal models represent predicates, admissible contexts, and domains of applicability by subobjects. In both settings the ambient category may have an intuitionistic internal logic: the law of excluded middle
is not available as an unrestricted internal inference rule.
The reason is structural rather than philosophical. In \(\mathsf{Set}\), the subobject classifier is the two-valued set \(\Omega =\{ \bot ,\top \} \), and every subset has a complement. In a general topos, a monomorphism \(A\hookrightarrow X\) is still classified by a map \(\chi _A:X\to \Omega \), but \(\Omega \) is generally a Heyting algebra rather than a Boolean algebra [ Mac Lane and Moerdijk , 1992 ] . Truth can depend on a stage or context, and a subobject need not have a complementary subobject. Thus failure to establish membership in \(A\) does not by itself establish membership in its complement.
For synthetic differential geometry this distinction is indispensable. Kock’s axiom says that every map \(g:D\to R\) has a unique form
If equality on \(D\) were decidable internally, excluded middle would permit the discontinuous case split “\(d=0\) or \(d\ne 0\).” Together with the Kock–Lawvere axiom, that split collapses the intended infinitesimal behavior and leads to contradiction [ Kock , 2006 , Section I.1 ] . The elements of \(D\) are therefore not ordinary hidden real numbers waiting to be classified as zero or nonzero; they are generalized elements whose first-order action is visible through maps out of \(D\).
The causal parallel requires care. A causal intervention is not created merely by naming a subobject. In a categorical causal model it normally also requires a mechanism-replacement map, policy, or other intervention semantics. Subobjects instead describe such things as an observational event, an admissible context, the region on which a protocol is defined, or the stages at which an independence or identification claim is validated. When these subobjects live in a non-Boolean sheaf topos, the model need not decide globally between “the causal claim holds” and “the causal claim fails.” A claim may hold after restriction to a cover, remain unresolved at the present stage, or acquire a counterexample on a refinement. This is the logic used by intuitionistic \(j\)-do-calculus [ Mahadevan , 2025c ] .
This common logic has four practical consequences for LINCS.
Unknown is not false. The absence of a factorization witness, causal certificate, or global section is not automatically a witness of nonexistence.
Diagnosis is stage-sensitive. An obstruction may be visible on one context, become locally trivial on a cover, or survive every admitted refinement. These are different judgments.
Repair requires positive evidence. A proposal is not admitted merely because its negation has not been proved. Admission must provide the declared witness, test, or certificate.
Boolean reasoning is local and declared. An application may use ordinary classical logic externally, and may reason classically about a decidable predicate or inside a Boolean model. What it may not do is assume without justification that every internal structural or causal predicate is decidable.
LINCS distinguishes not observed, observed to fail, and proved impossible. Constructive internal logic preserves these three states until an observer or admission rule supplies enough evidence to identify them.
In The Sign of the Four, Sherlock Holmes tells Watson, “when you have eliminated the impossible whatever remains, however improbable, must be the truth” [ Doyle , 1890 , Chapter 6 ] . The maxim cleanly separates possibility from probability, but it hides two logical certificates.
Suppose an external investigator has a finite, exhaustive family of hypotheses
and constructive refutations of every hypothesis except \(H_k\). Then \(H_k\) follows even intuitionistically: eliminating cases from an explicitly given disjunction does not itself require excluded middle. The stronger Holmesian move is to assume that the hypothesis family is exhaustive, that each impossibility judgment is sound, and that no unrepresented explanation remains.
Internally, those assumptions may fail. If eliminating \(\neg H\) yields only \(\neg \neg H\), intuitionistic logic does not in general permit the final step \(\neg \neg H\Rightarrow H\). Likewise, failure to construct \(H_i\) is not a construction of \(\neg H_i\). For LINCS, Holmes’s maxim is therefore a valid admission rule only when exhaustiveness and elimination are themselves certified; otherwise the remainder is a candidate for repair, not yet the truth.
This is not a demand that implementations abandon classical arithmetic or Boolean control flow. The distinction is between the external metatheory in which a model is built and the internal language used to reason about its context-dependent objects. One may study a smooth or causal topos using ordinary classical mathematics while correctly refraining from inserting excluded middle into that topos’s internal logic.