1.6 From semantic axioms to a repair calculus

Do-calculus transforms interventional distributions. Its rules are licensed by separation statements in a manipulated causal graph. A LINCS calculus has a different target. It transforms judgments about declared structures and their permitted repairs. A convenient judgment form is

where:

• \(\Gamma \) records semantic hypotheses, observers, and cover data;

• \(e\) is a registered edit from \(D\) to \(D'\);

• \(\mathcal I\) lists the non-target obligations held invariant; and

• \(\mathcal E\) records the evidence still required for admission.

The judgment says that \(e\) is a structurally licensed candidate. It does not yet say that \(e\) has been admitted or that it is a causal intervention on the represented domain.

When the registered edit is a natural transformation \(e:D\Rightarrow D'\), the graphical language of Figure 1 makes an important distinction visible. The repair is a 2-cell between model functors. Applying an observer \(\Omega :\mathcal C\to \mathcal Z\) does not create a new repair; it whiskers the existing one to obtain \(\Omega e:\Omega D\Rightarrow \Omega D'\). The observed change is therefore downstream of the typed model change.

If an edit changes the indexing sketch, its source and target models are not parallel functors and this picture no longer type-checks. Such theory-level repairs require a schema functor and a comparison cell, typically expressed through Kan extension; they are treated separately in the later chapters.