2 Technical details of the characterization of CJ97
The theory BDE consists of the axioms 5(b)(d)(e).
The theory ADE consists of the axioms 5(a)(d)(e).
Conditional explosion for ob is the statement that ∀ (A B C : Finset U), A ∈ ob C → B ∩ Aᶜ ∩ C ≠ ∅ → B ∈ ob (Aᶜ ∩ C).
If ob satisfies axioms 5(a)(b)(d)(e) then ob satisfies conditional explosion.
If \(a_1\ne a_2\), \(a_1\notin A\), \(a_2\notin A\), \(\{ a_1,a_2\} \in \operatorname{ob}(\{ a_1,a_2\} )\), and \(A\in \operatorname{ob}(X)\) whenever \(A\subseteq X\), then \(\{ a_1\} \in \operatorname{ob}\{ a_1, a_2\} \) and \(\{ a_2\} \in \operatorname{ob}\{ a_1, a_2\} \).
If \(a_1\ne a_2\), \(a_1\notin A\), \(a_2\notin A\), \(\{ a_1,a_2\} \in \operatorname{ob}(\{ a_1,a_2\} )\), then it cannot be that \(A\in \operatorname{ob}(X)\) whenever \(A\subseteq X\).
If \(a_1 \notin A\) and \(a_2 \notin A\) and \(a_1 \ne a_2\) then it cannot be that \(A\in \operatorname{ob}(X)\) whenever \(A\subseteq X\).
A world \(a\) is bad if ∃ (X : Finset (Fin n)), a ∈ X ∧ \(X \setminus \{ a\} \in \operatorname{ob}X\).
The world \(a\) is quasibad if ∃ (X : Finset (Fin n)) (Y : Finset (Fin n)), a ∈ X \(\setminus \) Y ∧ Y ∈ ob X.
Thus, a world \(a\) is bad if in some context there is an obligation to simply avoid \(a\). For example, if there is an obligation “do not go to war” then the world representing “going to war with Syria” is quasibad, but it is not bad unless there is also the specific obligation “do not go to war with Syria”. (In “reasonable” systems this distinction would perhaps not need to be made, but here we are in the process of proving that a certain system 5(abcde) is not reasonable.)
If \(a\) is bad and \(Y \setminus \{ a\} \ne \emptyset \) then \(Y \setminus \{ a\} \in \operatorname{ob}Y\).
Lemma 23 says that badness of the world does not depend on context.
If \(X ∈ \operatorname{ob}X\) and \(Y ≠ ∅\) then \(Y ∈ ob Y \).
Lemma 24 says that if any context is obligatory relative to itself, then they all are.
If \(\emptyset \ne X \setminus \{ a\} ∈ ob X\) then \(X ∈ \operatorname{ob}X\).
Lemma 25 says that if there is a bad world then the corresponding context is self-obligatory.
Assume axioms 5(abde). If \(a\) is \(\operatorname{ob}\)-bad then \(\{ a\} ∈ \operatorname{ob}\{ a\} \).
Lemma 26 is a technicality: even if \(a\) is bad, it is still self-obligatory.
If \(\mathrm{univ} \setminus \{ a\} ∈ \operatorname{ob}\mathrm{univ}\) then \(\mathrm{univ} ∈ \operatorname{ob}\mathrm{univ}\).
Lemma 27 is another technicality: if \(a\) is bad in the global context then the global context is self-obligatory.
Suppose that for all contexts \(A\), if \(A\) is obligatory in all larger contexts \(X\supseteq A\), then \(A\) is a cosubsingleton, i.e., missing at most one element (from the global context). Then for all \(B\) and \(C\), if \(B\subseteq C\) is obligatory relative to \(C\) then \(C\setminus B\) is a cosubsingleton.
Lemma 28 is a “global-to-local” principle allowing us to conclude a fact about an arbitrary context \(C\) from a fact about the global context.
The antecedent of Lemma 28 is provided by Lemma 29 and hence the consequent is provided by Lemma 30.
For all contexts \(A\), if \(A\) is obligatory in all larger contexts \(X\supseteq A\), then \(A\) is a cosubsingleton, i.e., missing at most one element (from the global context).
For all \(B\) and \(C\), if \(B\subseteq C\) is obligatory relative to \(C\) then \(C\setminus B\) is a cosubsingleton.
The model stayAlive is defined by stayAlive e X = \(\{ Y | X \cap Y \ne \emptyset \wedge X \setminus \{ e\} \subseteq X \cap Y\} \).
The model alive is defined by alive n X = \(\{ Y \mid X \ne \emptyset \wedge Y \supseteq X\} \).
The model noObligations is defined by noObligations X = ∅.
We think of alive as a computer game like “Snake” where the objective is to stay alive, with the surprising twist that it is not possible to die. In contrast, in the model noObligations there are no obligations at all, and in the model stayAlive the objective is standard: stay alive.
Thus, someone playing Snake under the noObligations model can relax completely, whereas someone playing under the alive model may worry that perhaps there is a way to die that they just have not seen yet. In fact, alive is a reduct of stayAlive where we remove the one bad world.
We prove several technical lemmas, culminating in Theorem 42:
If ob ≠ noObligations and ∀ a, ¬ quasibad ob a, then ob = alive k.
If bad ob a and bad ob b then \(a = b\).
If bad ob a and \(X ∩ Y ∈ ob X\) then \(X ∩ Y = X\) or \(X ∩ Y = X \setminus \{ a\} \).
If bad ob a and X ≠ a and X ≠ ∅ then X ∈ ob X.
If bad ob a and \(X \setminus \{ a\} \ne \emptyset \) then \(X ∈ \operatorname{ob}X\).
If bad ob a then ∀ Y, ob Y ⊆ stayAlive a Y.
Note that Lemma 40 does not require any form of C5.
If bad ob a then ∀ Y, stayAlive a Y ⊆ ob Y.
If bad ob a then ob = stayAlive a.
Every model of axioms 5(abcde) is either stayAlive \(a\) for some bad world \(a\), alive, or noObligations.
2.1 Acknowledgments
All mathematical claims above are verified in the proof assistant Lean, see [ 8 ] .
The main argument for our paradox was discovered by carefully analyzing some output from a script in the computer mathematics system Maple by Maplesoft [ 6 , Appendix ] .
This work was partially supported by a grant from the Simons Foundation (#704836 to Bjørn Kjos-Hanssen).