Observer-Relative Action Rule Decidability

Abstract

Actor-relative readability is preserved exactly by compatible transitions.

Theorem 1.1 (Readability of the three action-rule forms).

$$\begin{array}{c}\forall X,U,I:\mathrm{Type},\\ B:I\to \mathrm{Type},q:\forall k:I,X\to B\left(k\right),\\ F:X\to \left(U\to \left(I\to \left(I\to X\right)\right)\right),i:I,\\ Q:X\times U\times I\to B\left(i\right)\times U\times I:=\Lambda z:X\times U\times I,\mathrm{triple}\left(q\left(i\right)\left(\mathrm{state}\left(z\right)\right),\mathrm{action}\left(z\right),\mathrm{recipient}\left(z\right)\right),\\ M:X\times U\times I\to X:=\Lambda z:X\times U\times I,F\left(\mathrm{state}\left(z\right),\mathrm{action}\left(z\right),\mathrm{recipient}\left(z\right),i\right),\\ A:X\times U\times I\to X:=\Lambda z:X\times U\times I,F\left(\mathrm{state}\left(z\right),\mathrm{action}\left(z\right),i,\mathrm{recipient}\left(z\right)\right),\\ [(\mathrm{FactorsThrough}\left(\mathrm{compose}\left(q\left(i\right),M\right),Q\right)\iff \left(\forall W\in X\to Prop,\mathrm{FactorsThrough}\left(W,q\left(i\right)\right)\Rightarrow \mathrm{FactorsThrough}\left(\Lambda z:X\times U\times I,\neg W\left(M\left(z\right)\right),Q\right)\right))\wedge \\ (\forall W\in X\to Prop,C\in X\times U\times I\to Prop,\left(\mathrm{FactorsThrough}\left(W,q\left(i\right)\right)\wedge \left(\mathrm{FactorsThrough}\left(C,Q\right)\wedge \mathrm{FactorsThrough}\left(\mathrm{compose}\left(q\left(i\right),M\right),Q\right)\right)\right)\Rightarrow \mathrm{FactorsThrough}\left(\Lambda z:X\times U\times I,W\left(M\left(z\right)\right)\wedge C\left(z\right),Q\right))\wedge \\ (\forall V\in \forall j:I,X\to Prop,\mathrm{FactorsThrough}\left(\Lambda z:X\times U\times I,\neg V\left(\mathrm{recipient}\left(z\right),A\left(z\right)\right),Q\right)\iff \mathrm{FactorsThrough}\left(\Lambda z:X\times U\times I,V\left(\mathrm{recipient}\left(z\right),A\left(z\right)\right),Q\right))].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/NormativeStructure/ObserverActionRuleDecidability.observer_action_rule_decidability (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actor readout, transition, mirrored transition, actual transition, and actor-visible action input are constructed explicitly on the source carrier.

Transition compatibility is equivalent to readability of every negative mirrored wish. This includes the source converse: an incompatible transition is separated by a readable wish.

Under the same compatibility, a readable wish conjoined with a readable capability remains readable. For the actual transition evaluated by another recipient’s wish, readability of the negated rule is exactly readability of the pulled-back wish itself.

References

• Truth anchor: D5/S3/ConceptDynamics/NormativeStructure/ObserverActionRuleDecidability.observer_action_rule_decidability