In response to the phenomenon of "Evaporation of Responsibility" in automated and bureaucratic decision-making, this paper provides a structural impossibility proof rather than an ethical critique. We proceed within the axiomatic system of ZF set theory to ensure a constructive proof with minimal assumptions, explicitly excluding dependence on the Axiom of Choice.
The claims of this paper intersect with the following research domains: (i) Accountability gaps in algorithmic decision-making (e.g., [Matthias2004], [Kroll2017]). (ii) Data and Decision Provenance frameworks ensuring auditability (e.g., [W3CPROV], [Cheney2009], [Singh2019]). (iii) Robustness of algorithmic recourse and post-hoc explanations (e.g., [Karimi2022], [Upadhyay2021], [Rudin2019]).
While most existing studies discuss "what should be explained or recorded" as a matter of policy or design, this paper is distinct in providing a necessary condition (impossibility) from a set-theoretic perspective: without an Exploration Interval (Exploration Log), Responsibility Fixability (the existence of a left inverse) cannot exist mathematically.
We proceed within the framework of ZF set theory. We adopt the standard Kuratowski definition for ordered pairs, \((a,b):=\{\{a\},\{a,b\}\}\), and treat relations as sets of ordered pairs. A function (or mapping) \(f\) is defined as a relation such that for any \(x\) in the domain \(\mathrm{Dom}(f)\), there exists a unique \(y\) satisfying \((x,y)\in f\); this unique \(y\) is denoted as \(f(x)\). The notation \(f:A\to B\) implies \(\mathrm{Dom}(f)=A\) and \(\mathrm{Im}(f)\subseteq B\). The image is defined as \(\mathrm{Im}(f):=\{y\in B\mid \exists x\in A\,((x,y)\in f)\}\) (via the Axiom of Separation), and the restriction mapping is \(f\upharpoonright S:=\{(x,y)\in f\mid x\in S\}\). A function is injective if \(\forall x_1,x_2\in\mathrm{Dom}(f)\,(f(x_1)=f(x_2)\Rightarrow x_1=x_2)\), and surjective if \(\mathrm{Im}(f)=B\).
We assume the following entities are sets within ZF:
(1 \(\Rightarrow\) 2)
Assume \(\Phi\) is Responsibility Fixable with left inverse \(R\). Let \(\Phi(c_1) = \Phi(c_2)\). Since this value is in \(\mathrm{Im}(\Phi)\), applying \(R\) yields:
$$ c_1 = R(\Phi(c_1)) = R(\Phi(c_2)) = c_2 $$
Thus, \(\Phi\) is injective.
(2 \(\Rightarrow\) 1)
Assume \(\Phi\) is injective. Consider the class of ordered pairs defined by \(c\mapsto(\Phi(c),c)\) for all \(c\in\mathcal{C}\). By the Axiom of Replacement, the set
$$ R := \{(\Phi(c),c)\mid c\in\mathcal{C}\} $$
exists. We show \(R\) is a function. If \((x,c_1)\in R\) and \((x,c_2)\in R\), then \(x=\Phi(c_1)=\Phi(c_2)\). By injectivity, \(c_1=c_2\). Thus, \(R\) maps each \(x\) to a unique \(c\).
The domain of \(R\) is \(\mathrm{Im}(\Phi)\), and for any \(c\in\mathcal{C}\), since \((\Phi(c),c)\in R\), it follows that \(R(\Phi(c))=c\).
We now formulate the condition where the context space \(\mathcal{C}\) is "sufficiently complex" relative to the trace space \(\mathcal{X}_0\). We term this "Context Richness."
Let \(f:X\to\mathcal{P}(X)\) be an arbitrary mapping. By the Axiom of Separation, the set $$ D:=\{x\in X\mid x\notin f(x)\}\subseteq X $$ exists. For any \(x\in X\), if \(D=f(x)\), then \(x\in D \iff x\notin f(x) \iff x\notin D\), a contradiction. Thus, \(\forall x\in X, D\neq f(x)\). Consequently, \(f\) cannot be surjective.
Assumption: \(\mathcal{C}\) is Rich relative to \(\mathcal{X}_0\) (Definition 2).
Claim: No decision mapping \(\Phi_0: \mathcal{C} \to \mathcal{X}_0\) is Responsibility Fixable.
We proceed by contradiction. Assume there exists a mapping \(\Phi_0: \mathcal{C}\to\mathcal{X}_0\) that is Responsibility Fixable.
1. By Lemma 1 (1 \(\Rightarrow\) 2), \(\Phi_0\) is injective.
2. Following the construction in Lemma 1 (2 \(\Rightarrow\) 1), there exists a left inverse \(R:\mathrm{Im}(\Phi_0)\to\mathcal{C}\) such that \(R(\Phi_0(c))=c\) for all \(c\).
3. By the Assumption (Definition 2), there exists a surjection \(h:\mathcal{C}\twoheadrightarrow\mathcal{P}(\mathcal{X}_0)\).
Now, consider the mapping \(g:\mathcal{X}_0\to\mathcal{P}(\mathcal{X}_0)\) defined as:
$$ g(x):=\begin{cases}
(h\circ R)(x) & \text{if } x\in \mathrm{Im}(\Phi_0),\\
\emptyset & \text{if } x\notin \mathrm{Im}(\Phi_0).
\end{cases} $$
(Note: The graph of \(g\) is constructible in ZF via Separation and Union axioms.)
For any subset \(S\in\mathcal{P}(\mathcal{X}_0)\), since \(h\) is surjective, there exists \(c\in\mathcal{C}\) such that \(h(c)=S\). Let \(x:=\Phi_0(c)\). Then \(x\in\mathrm{Im}(\Phi_0)\), and:
$$ g(x) = h(R(\Phi_0(c))) = h(c) = S. $$
Thus, \(g\) is surjective onto \(\mathcal{P}(\mathcal{X}_0)\). However, by Lemma 3 (Cantor's Theorem), no such surjection exists. This is a contradiction. Therefore, \(\Phi_0\) cannot be Responsibility Fixable.
We axiomatize the Exploration Log as a finite sequence of events. Let \(\mathcal{E}\) be the set of events (observations, branches, etc.), and let \(n\in\omega\) be a finite ordinal. A log of length \(n\) is a function \(\gamma:n\to\mathcal{E}\). We define the log space as: $$ \mathcal{L}:=\bigcup_{n\in\omega} \mathcal{E}^n $$ The generation rule is a relation \(P\subseteq \mathcal{C}\times\mathcal{L}\) assigning a unique \(\gamma\) to each \(c\), defining the function \(\ell: \mathcal{C} \to \mathcal{L}\). (Existence: \(\mathcal{L}\) exists in ZF via Power Set, Separation, Replacement, and Union axioms).
Consider the extended mapping \(\Phi_1(c) = (\Phi_0(c), \ell(c))\). Let \(F_x = \{ c \in \mathcal{C} \mid \Phi_0(c) = x \}\) be the fiber of \(\Phi_0\) over \(x\).
(\(\Rightarrow\)) Assume \(\Phi_1\) is injective. For any \(x\in\mathcal{X}_0\) and \(c_1,c_2\in F_x\) with \(\ell(c_1)=\ell(c_2)\), we have \(\Phi_1(c_1)=(\Phi_0(c_1),\ell(c_1))=(x,\ell(c_2))=\Phi_1(c_2)\). Thus \(c_1=c_2\).
(\(\Leftarrow\)) Conversely, if \(\Phi_1(c_1)=\Phi_1(c_2)\), then \(\Phi_0(c_1)=\Phi_0(c_2)=:x\) and \(\ell(c_1)=\ell(c_2)\). Thus \(c_1,c_2 \in F_x\). Since \(\ell|_{F_x}\) is injective, \(c_1=c_2\).
Theorem 1 implies that under rich contexts, any mapping \(\Phi_0\) based solely on the trace space \(\mathcal{X}_0\) is necessarily non-injective. Consequently, there exist distinct contexts \(c_1, c_2\) yielding the same result \(x\). For such \(x\), no function \(R\) exists to uniquely identify the cause. Thus, any attempt to assign responsibility becomes a Post-hoc Impossibility.
We have established the "necessity of Exploration Intervals" as a theorem within ZF set theory. Responsibility Fixability requires injectivity (Lemma 1), and injectivity fails for rich contexts without exploration data (Theorem 1). The condition for restoring responsibility is precisely the fiber separation property of the log (Lemma 2).
This paper presents a limitative claim: without specific structural conditions (exploration intervals), the attribution of responsibility is mathematically undefined. This form parallels Gödel's incompleteness theorems or Arrow's impossibility theorem, where internal mathematical limits inform external philosophical frameworks ([Godel1931], [Arrow1951]).
Philosophically, responsibility is linked to the agent's ability to offer reasons ([Strawson1962], [Anscombe1957]). The Exploration Interval Log serves as the minimal structural condition to preserve these reasons (branches, rejections) for verification.
In bureaucracy and automation, the link between decision and reason often "evaporates" ([Weber1946], [Arendt1963]). We formalize this not as a moral failure, but as a mapping-theoretic impossibility when information is lossily compressed.
This connects directly to Decision Provenance ([Singh2019]). The Exploration Log is the implementation of the fiber-separating function required to make systems mathematically accountable.