Action Expansion Indistinguishability Law

Abstract

A separating new action can make behavioral indistinguishability shrink strictly.

Theorem 1.1 (Action expansion reveals previously hidden distinctions).

$$\begin{array}{c}\forall A,X,B:\mathrm{Type},\\ M,M_{expanded}:\mathrm{Set}\left(A\right),F:A\to X\to X,O:X\to B,\\ M\subseteq M_{expanded}\Rightarrow \\ {\sim }_{M_{expanded}}\subseteq {\sim }_M\wedge \\ \forall u\in M_{expanded}\setminus M,\forall x,y:X,x{\sim }_{M}y\wedge O(F(u)(x))\ne O(F(u)(y))\Rightarrow \neg x{\sim }_{M_{expanded}}y\wedge \\ \exists M_0,M_1:\mathrm{Set}\left(Unit\right),F_0:Unit\to Bool\to Bool,O_0:Bool\to Bool,x_0,y_0:Bool,M_0\subset M_1\wedge x_0{\sim }_{M_0}{y}_0\wedge \neg x_0{\sim }_{M_1}{y}_0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/OperationalOntology/ActionExpansionIndistinguishabilityLaw.action_expansion_indistinguishability_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary action, state, and output carriers, agreement under every expanded action implies agreement under every original action.

If a newly available action gives unequal public outputs on a pair from the original indistinguishability relation, that pair is absent from the expanded relation.

The public countermodel uses empty and singleton Unit action sets with the identity Boolean transition. The same states belong to the original relation and fail to belong to the expanded relation, so the converse inclusion is not valid in general.

References

• Truth anchor: D5/S3/ConceptDynamics/OperationalOntology/ActionExpansionIndistinguishabilityLaw.action_expansion_indistinguishability_law
• Dependency: D5/S3/ConceptDynamics/OperationalOntology/ActionExpansionIndistinguishability