Observation-Intervention-Counterfactual Query-Kernel Hierarchy

Abstract

Nested observational, interventional, and counterfactual query families induce a kernel chain, and both links admit concrete strictness witnesses.

Theorem 1.1 (Nested query families induce the kernel hierarchy).

$\forall M \in Type, O b s I n d e x \in Type, I n t I n d e x \in Type, C f I n d e x \in Type, O b s A n s w er \in O b s I n d e x \to Type, I n t A n s w er \in I n t I n d e x \to Type, C f A n s w er \in C f I n d e x \to Type, o b s Q u ery \in (o i : O b s I n d e x) \to M \to O b s A n s w er (o i), in tQ u ery \in (ii : I n t I n d e x) \to M \to I n t A n s w er (ii), c f Q u ery \in (c i : C f I n d e x) \to M \to C f A n s w er (c i), o b s T o I n t \in O b s I n d e x \to I n t I n d e x, in tT o C f \in I n t I n d e x \to C f I n d e x, o b s F ro m I n t \in (o i : O b s I n d e x) \to I n t A n s w er (o b s T o I n t (o i)) \to O b s A n s w er (o i), in tF ro m C f \in (ii : I n t I n d e x) \to C f A n s w er (in tT o C f (ii)) \to I n t A n s w er (ii), h O b s \in (\forall o i \in O b s I n d e x, m \in M, o b s F ro m I n t (o i, in tQ u ery (o b s T o I n t (o i), m)) = o b s Q u ery (o i, m)), h I n t \in (\forall ii \in I n t I n d e x, m \in M, in tF ro m C f (ii, c f Q u ery (in tT o C f (ii), m)) = in tQ u ery (ii, m)), (\forall m \in M, n \in M, q u eryKer n e l (c f Q u ery, m, n) \Rightarrow q u eryKer n e l (in tQ u ery, m, n)) \land ((\forall m \in M, n \in M, q u eryKer n e l (in tQ u ery, m, n) \Rightarrow q u eryKer n e l (o b s Q u ery, m, n)) \land ((\exists S \in De t er mini s t i c B oo lSCM, T \in De t er mini s t i c B oo lSCM, I n t (S) = I n t (T) \land CF (S) \neq = CF (T)) \land (\exists S \in De t er mini s t i c B oo lSCM, T \in De t er mini s t i c B oo lSCM, O b s (S) = O b s (T) \land I n t (S) \neq = I n t (T))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Causal/QueryKernelHierarchy.query_kernel_hierarchy (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each observational answer is read from a designated interventional answer, and each interventional answer is read from a designated counterfactual answer. Equality at the richer layer therefore forces equality at the next layer.

The two final clauses reuse the established Boolean structural-model countermodels. One separates equal single-world intervention answers from cross-world responses; the other separates equal observations from intervention answers.

References

Truth anchor: D5/S3/ConceptDynamics/Causal/QueryKernelHierarchy.query_kernel_hierarchy
Dependency: D5/S3/ConceptDynamics/Causal/ObservationInterventionCounterfactualChain
Dependency: D5/S3/ConceptDynamics/Sufficiency/QueryFamilyIdentification

Keyboard shortcuts

trureturing Blueprint

Observation-Intervention-Counterfactual Query-Kernel Hierarchy

Abstract

References