Graded models of Carmo and Jones' systems

We show that the two approaches sketched in [Kjos-Hanssen 2017] are both consistent with [Carmo Jones 2022].

To incorporate contrary-to-duty obligations we introduce predicates A, B for the best and at least second-best worlds with A ⊆ B.

If X ∩ A = ∅ but X ∩ B ≠ ∅, the desirable worlds given X are X ∩ B.

We prove the following results about which axioms hold in which model. Since the models without the subscript ₂ are special cases of those with it, some results follow: these are indicated with (parentheses).

5	canon	canon_II	canon₂	canon₂_II
a	(✓	(✓)	✓	✓
			canon₂_A5	canon₂_II_A5
--	------------	---------------	------------	----------------
b	(✓)	(✓)	✓	✓
			canon₂_B5	canon₂_II_B5
--	------------	---------------	------------	----------------
c	(✓)	(✓)	✓	✓
			canon₂_C5	canon₂_II_C5
--	------------	---------------	------------	----------------
d	(✓)	×	✓	(×)
		not_canon_II_D5	canon₂_D5
--	------------	---------------	------------	----------------
e	×	✓	(×)	✓
	not_canon_E5	canon_II_E5		canon₂_II_E5
--	------------	---------------	------------	----------------
f	(✓)	✓	✓	×!
		canon_II_F5	canon₂_F5	not_canon₂_II_F5
--	------------	---------------	------------	----------------
g	✓	(✓)	×!	✓
	canon_G		not_canon₂_G	canon₂_II_G5
--	------------	---------------	------------	----------------
The counterexamples used are quite simple and include A = {0} ⊆ U = {0,1},
A = {0} ⊆ B = {0,1} = U,
and A = {0} ⊆ B = {0,2} ⊆ U = {0,1,2},
with X = {0, 1}, Y = {0, 1, 2}, Z = {1, 2}.

We study three systems in detail:

• CJ 1997: the models have a unique-bad-world feature. Nevertheless the system has several models.
• CJ 2013: the system implies conditional deontic explosion but not unique-bad-world.
• CJ 2022: the system does not imply unique-bad-world but the brief-marriage paradox.

Perhaps fittingly for papers about contrary-to-duty obligations, ideally we should avoid the brief-marriage paradox, but if we cannot we should at least avoid deontic explosion, and if we cannot, at least avoid unique-bad-world.

def canon {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : Finset α → Finset (Finset α)

Equations

• canon A S = if S ∩ A = ∅ then ∅ else {T : Finset α | S ∩ A ⊆ T}

def canon_II {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : Finset α → Finset (Finset α)

The canon models, which say that what is obligatory is to be in one of the still-possible optimal worlds, satisfy all axioms except E5. This corresponds to approach (I) in [Kjos-Hanssen 2017]

We make a [CJ 2022] style canon_II by letting ob X = {Y | Y ∩ X = A ∩ X}. [Kjos-Hanssen 2017]'s (II) corresponds to:

Equations

• canon_II A X = if X ∩ A = ∅ then ∅ else {Y : Finset α | X ∩ Y = X ∩ A}

def canon_II'' {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : Finset α → Finset (Finset α)

Equations

• canon_II'' A X = if X ∩ A = ∅ then Finset.univ \ {∅} else {Y : Finset α | X ∩ Y = X ∩ A}

theorem canon_II_symm {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : canon_II A = fun (X : Finset α) => if X ∩ A = ∅ then ∅ else {Y : Finset α | X ∩ A = X ∩ Y}

theorem canon_II_E5 {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : E5 (canon_II A)

canon_II does satisfy axiom 5(e).

theorem not_canon_E5 : ∃ (n : ℕ) (A : Finset (Fin n)), ¬E5 (canon A)

canon does not satisfy axiom 5(e).

theorem many_not_canon_II_D5 {n : ℕ} {A : Finset (Fin n)} (h₀ : A ≠ ∅) (h₁ : A ≠ Finset.univ) : ¬D5 (canon_II A)

theorem many_not_canon_II''_D5 {n : ℕ} {A : Finset (Fin n)} (h₀ : A ≠ ∅) (h₁ : A ≠ Finset.univ) : ¬D5 (canon_II'' A)

theorem not_canon_II_D5 : ∃ (n : ℕ) (A : Finset (Fin n)), ¬D5 (canon_II A)

canon_II does not satisfy axiom 5(d).

def canon₂ {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : Finset α → Finset (Finset α)

Equations

• canon₂ A B X = if X ∩ B = ∅ then ∅ else if X ∩ A = ∅ then {T : Finset α | X ∩ B ⊆ T} else {T : Finset α | X ∩ A ⊆ T}

def canon₂' {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) (P : Finset (Finset α)) : Finset α → Finset (Finset α)

There is some uncertainty about what is obligatory when no good options are available. This definition avoids that by packaging it into a set P.

Equations

• canon₂' A B P X = if X ∩ B = ∅ then P else if X ∩ A = ∅ then {T : Finset α | X ∩ B ⊆ T} else {T : Finset α | X ∩ A ⊆ T}

theorem canon₂_C5Strong {n : ℕ} (A B : Finset (Fin n)) : C5Strong (canon₂ A B)

theorem fixD5 {n : ℕ} {ob : Finset (Fin n) → Finset (Finset (Fin n))} (d5 : D5 ob) (A B C : Finset (Fin n)) : A ∩ B ∩ C ∈ ob (A ∩ B) → A \ (A ∩ B) ∪ A ∩ B ∩ C ∈ ob A

theorem canon_eq_canon₂ {n : ℕ} {A : Finset (Fin n)} : canon A = canon₂ A A

theorem canon₂_eq_canon₂' {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : canon₂ A B = canon₂' A B ∅

def canon₂_II {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : Finset α → Finset (Finset α)

Equations

• canon₂_II A B X = if X ∩ B = ∅ then ∅ else if X ∩ A = ∅ then {Y : Finset α | X ∩ B = X ∩ Y} else {Y : Finset α | X ∩ A = X ∩ Y}

theorem inter_two {n : ℕ} {B X Y Z : Finset (Fin n)} (h₀ : X ∩ B = X ∩ Y) (h₁ : X ∩ B = X ∩ Z) : X ∩ B = X ∩ (Y ∩ Z)

theorem canon₂_II_C5Strong {n : ℕ} (A B : Finset (Fin n)) : C5Strong (canon₂_II A B)

theorem canon₂_II_subset_canon₂ {α : Type u_1} [Fintype α] [DecidableEq α] (A B X : Finset α) : canon₂_II A B X ⊆ canon₂ A B X

theorem canon_II_is_canon₂_II {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : canon_II A = canon₂_II A A

def canon₂General {α : Type u_1} [Fintype α] [DecidableEq α] (ob : Finset α → Finset (Finset α)) : Prop

canon₂_II says that only "perfect" scenarios are obligatory, whereas canon₂ is permissive. canon₂General captures the idea of being somewhere in between. For example perhaps "Be law-abiding or cheat on your taxes" is not obligatory but "Be law-abiding or speed on the freeway" is obligatory. Note that canon₂_II fails F5 and passes E5 and canon₂ fails E5 and passes F5. Perhaps some canon₂General can pass both? Perhas A5 B5 C5 hold for any canon₂General A5 yes, see below. B5 no, clearly C5 no, clearly what's interesting however is those ob that do satisfy canon₂General and also B5, C5

maybe what we can show is that no model satisfying canon₂General can satisfy all CJ2022's requirements.

Equations

• canon₂General ob = ∃ (A : Finset α) (B : Finset α), ∀ (X : Finset α), canon₂_II A B X ⊆ ob X ∧ ob X ⊆ canon₂ A B X

theorem subset_canon₂_A5 {α : Type u_1} [Fintype α] [DecidableEq α] (ob : Finset α → Finset (Finset α)) (P : Finset (Finset α)) (hP : ∅ ∉ P) (h : ∃ (A : Finset α) (B : Finset α), ∀ (X : Finset α), ob X ⊆ canon₂' A B P X) : A5 ob

theorem canon₂_II_A5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : A5 (canon₂_II A B)

The canon₂_II models satisfy axiom 5(a).

theorem canon₂_II_B5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : B5 (canon₂_II A B)

The canon₂_II models satisfy axiom 5(b).

theorem canon₂_II_C5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : C5 (canon₂_II A B)

The canon₂_II models satisfy axiom 5(c).

theorem many_not_canon₂_E5_P {n : ℕ} {A B : Finset (Fin n)} (P : Finset (Finset (Fin n))) (hP : Finset.univ ∉ P) (h₄ : B ≠ ∅) (h₀ : A ∪ B ≠ Finset.univ) : ¬E5 (canon₂' A B P)

Mild conditions on B work here, that generalize A=B. (June 2, 2025)

theorem many_not_canon₂_E5 {n : ℕ} {A B : Finset (Fin n)} (h₄ : B ≠ ∅) (h₀ : A ∪ B ≠ Finset.univ) : ¬E5 (canon₂ A B)

Mild conditions on B work here, that generalize A=B. (June 2, 2025)

theorem many_not_canon_E5 {n : ℕ} {A : Finset (Fin n)} (h₀ : A ≠ ∅) (h₁ : A ≠ Finset.univ) : ¬E5 (canon A)

theorem canon₂_II_E5 {α : Type u_1} [Fintype α] [DecidableEq α] {A B : Finset α} (h : A ⊆ B) : E5 (canon₂_II A B)

The canon₂_II models satisfy axiom 5(e) if A ⊆ B.

theorem canon₂_II_G5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : G5 (canon₂_II A B)

The canon₂_II models satisfy axiom 5(g).

theorem canon₂_A5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : A5 (canon₂ A B)

The canon₂ models satisfy axiom 5(a).

theorem canon₂_B5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : B5 (canon₂ A B)

The canon₂ models satisfy axiom 5(b).

theorem canon₂_C5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : C5 (canon₂ A B)

The canon₂ models satisfy axiom 5(c).

theorem canon₂_D5 {α : Type u_1} [Fintype α] [DecidableEq α] {A B : Finset α} (h : A ⊆ B) : D5 (canon₂ A B)

The canon₂ models satisfy axiom 5(d).

theorem theorem10_1996_related : ∃ (ob : Finset (Fin 3) → Finset (Finset (Fin 3))), (∀ (X : Finset (Fin 3)), 0 ∈ X → {0} ∈ ob X) ∧ A5 ob ∧ C5Strong ob ∧ B5 ob ∧ D5 ob ∧ ¬E5 ob

theorem many_not_canon₂_G {n : ℕ} {A B : Finset (Fin (n + 3))} (h₄' : A ≠ ∅) (h₀' : A ∪ B ≠ Finset.univ) (h₁' : B \ A ≠ ∅) : ¬G5 (canon₂ A B)

Based on the fact that A = {2}, B={1,2}, X₀={0,1}, Y₀=univ, Z₀={0,2} works.

theorem infinitely_many_not_canon₂_G {n : ℕ} : ∃ (A : Finset (Fin (n + 3))) (B : Finset (Fin (n + 3))), A ⊆ B ∧ ¬G5 (canon₂ A B)

theorem not_canon₂_G : ∃ (n : ℕ) (A : Finset (Fin n)) (B : Finset (Fin n)), A ⊆ B ∧ ¬G5 (canon₂ A B)

canon₂ models do not satisfy Axiom 5(g). Since canon₂_II does satisfy 5(g) (see canon₂_II_G5) 5(g) belongs firmly in the II category.

theorem canon₂_F5 {α : Type u_1} [Fintype α] [DecidableEq α] (A B : Finset α) : F5 (canon₂ A B)

The canon₂ models satisfy axiom 5(f).

def CJ_all_2022 {α : Type u_1} [Fintype α] [DecidableEq α] (ob : Finset α → Finset (Finset α)) : Prop

All the axioms (including the paradoxical B, D, E):

Equations

• CJ_all_2022 ob = (A5 ob ∧ B5 ob ∧ C5 ob ∧ D5 ob ∧ E5 ob ∧ F5 ob ∧ G5 ob)

def CJ_noE_2022 {α : Type u_1} [Fintype α] [DecidableEq α] (ob : Finset α → Finset (Finset α)) : Prop

Equations

• CJ_noE_2022 ob = (A5 ob ∧ B5 ob ∧ C5 ob ∧ D5 ob ∧ F5 ob ∧ G5 ob)

def CJ_noD_2022 {α : Type u_1} [Fintype α] [DecidableEq α] (ob : Finset α → Finset (Finset α)) : Prop

This could also be called CJ_2022.

Equations

• CJ_noD_2022 ob = (A5 ob ∧ B5 ob ∧ C5 ob ∧ E5 ob ∧ F5 ob ∧ G5 ob)

def CJ_noDF_2022 {α : Type u_1} [Fintype α] [DecidableEq α] (ob : Finset α → Finset (Finset α)) : Prop

Equations

• CJ_noDF_2022 ob = (A5 ob ∧ B5 ob ∧ C5 ob ∧ E5 ob ∧ G5 ob)

def CJ_noEG_2022 {α : Type u_1} [Fintype α] [DecidableEq α] (ob : Finset α → Finset (Finset α)) : Prop

Equations

• CJ_noEG_2022 ob = (A5 ob ∧ B5 ob ∧ C5 ob ∧ D5 ob ∧ F5 ob)

theorem CJ_no_DF_canon₂_II {α : Type u_1} [Fintype α] [DecidableEq α] {A B : Finset α} (h : A ⊆ B) : CJ_noDF_2022 (canon₂_II A B)

theorem CJ_no_EG_canon₂ {α : Type u_1} [Fintype α] [DecidableEq α] {A B : Finset α} (h : A ⊆ B) : CJ_noEG_2022 (canon₂ A B)

theorem generalize_F5_canon_II {α : Type u_1} [Fintype α] [DecidableEq α] {A B : Finset α} (hBA : B ⊆ A) : F5 (canon₂_II A B)

A modest generalization of canon_II_F5.

theorem canon_II_F5 {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : F5 (canon_II A)

theorem CJ_noD_canon_II {α : Type u_1} [Fintype α] [DecidableEq α] {A : Finset α} : CJ_noD_2022 (canon_II A)

theorem canon_G {α : Type u_1} [Fintype α] [DecidableEq α] (A : Finset α) : G5 (canon A)

theorem CJ_noE_canon {α : Type u_1} [Fintype α] [DecidableEq α] {A : Finset α} : CJ_noE_2022 (canon A)

theorem coincidence {α : Type u_1} [Fintype α] [DecidableEq α] : canon Finset.univ = canon_II Finset.univ

theorem CJ_all_canon_univ {α : Type u_1} [Fintype α] [DecidableEq α] : CJ_all_2022 (canon Finset.univ)

For any n, there is an n-world model of A5 through G5, namely: let ob(X) be all the supersets of X, except that ob(∅)=∅.

def observation_5_2' (X : Finset (Fin 4)) : Finset (Finset (Fin 4))

Like observation_5_2 but with Finset instead of Set.

Equations

• observation_5_2' X = if X ∩ {0, 1} = ∅ then {Y : Finset (Fin 4) | Y ∩ X = {3}} else {Y : Finset (Fin 4) | Y ∩ X ⊇ {0, 1} ∩ X}

theorem observation_5_2_subset_canon₂ (X : Finset (Fin 4)) : canon₂ {0, 1} {0, 1, 3} X ⊇ observation_5_2' X

theorem canon₂_II_subset_observation_5_2 (X : Finset (Fin 4)) : canon₂_II {0, 1} {0, 1, 3} X ⊆ observation_5_2' X

theorem canon₂General_observation_5_2 : canon₂General observation_5_2'

The utility of the definition canon₂General may seem questionable but it is hereby demonstrated:

theorem observation_5_2_not_subset_canon₂_II : ∃ (X : Finset (Fin 4)), ¬canon₂_II {0, 1} {0, 1, 3} X ⊇ observation_5_2' X

theorem canon₂_not_subset_observation_5_2 : ∃ (X : Finset (Fin 4)), ¬canon₂ {0, 1} {0, 1, 3} X ⊆ observation_5_2' X

theorem observation_5_2_ne_canon₂ : canon₂ {0, 1} {0, 1, 3} ≠ observation_5_2'

We see that their model is not canon₂ because Y ∩ X ⊇ {3} is not the same as Y ∩ X = {3}. 2 may or may not be in.

theorem many_not_E5_canon₂ {n : ℕ} {A B : Finset (Fin n)} (h₀ : A ∩ B ≠ ∅) (h₁ : B ≠ Finset.univ) : ¬E5 (canon₂ A B)

For the most part, 5(e) does hold in canon₂ models.

theorem similar_to_canon₂_II_often_fails_F5 {n : ℕ} {a₀ a₁ : Fin n} {A B : Finset (Fin n)} (h₀ : a₀ ∈ B) (h₁ : a₁ ∈ B) (h₂ : a₀ ∈ A) (h₃ : a₁ ∉ A) (ob : Finset (Fin n) → Finset (Finset (Fin n))) (hc₀ : canon₂_II A B {a₀} ⊆ ob {a₀}) (hc₀' : canon₂_II A B {a₁} ⊆ ob {a₁}) (hc₁₂ : ob ({a₀} ∪ {a₁}) ⊆ canon₂_II A B ({a₀} ∪ {a₁})) : ¬F5 ob

F5 fails for certain ob that are close to canon₂_II.

theorem not_canon₂_II_F5 {n : ℕ} {A B : Finset (Fin n)} (h : A ∩ B ≠ ∅) (h' : B \ A ≠ ∅) : ¬F5 (canon₂_II A B)

Generically, F5 fails for canon₂_II. Specifically canon₂_II {0} univ does not, although canon₂_II {0} {0} does, over Fin 2.

theorem canon₂_II_often_fails_F5 {n : ℕ} (A B : Finset (Fin n)) (hA : A ≠ ∅) (hA' : A ≠ B) (h₁ : A ⊆ B) : ¬F5 (canon₂_II A B)

A weaker form of not_canon₂_II_F5.

theorem cj1_2 {U : Type u_1} [Fintype U] {A B : Finset U} {ob : Finset U → Finset (Finset U)} (hg : weakly_mutually_generic A B) (b5 : B5 ob) (d5 : D5 ob) (e5w : E5weak ob) (hu₀ : A ∈ ob Finset.univ) : B ∈ ob Aᶜ

THEOREM 1.2 The main result of [Kjos-Hanssen 2017]. Adapted from rj-mike-final.lean Math 654 final project Fall 2020.

theorem may30_2025 {U : Type u_1} [Fintype U] {ob : Finset U → Finset (Finset U)} (a5 : A5 ob) (b5 : B5 ob) (d5 : D5 ob) (e5w : E5weak ob) : CXweak ob

The weak form of E5 proves weak conditional explosion. Should also be true if we remove both occurrences of "weak".

theorem ab_ob {U : Type u_1} [Fintype U] {ob : Finset U → Finset (Finset U)} (a5 : A5 ob) (b5 : B5 ob) (A C : Finset U) (hu₀ : A ∈ ob C) : A ∩ C ≠ ∅

Assuming axioms A5, B5, if A ∈ ob C then A ∩ C ≠ ∅.

theorem conditional_explosion {U : Type u_1} [Fintype U] {ob : Finset U → Finset (Finset U)} (a5 : A5 ob) (b5 : B5 ob) (d5 : D5 ob) (e5 : E5 ob) : CX ob

The axioms A5, B5, D5, E5 imply conditional deontic explosion. (Separately we prove CJ 2022's conjecture that A5, B5, C5, E5, F5, G5 do not.)

theorem e5Needed : ∃ (ob : Finset (Fin 3) → Finset (Finset (Fin 3))), B5 ob ∧ D5 ob ∧ ¬CX ob

theorem e5Needed₂ : ∃ (ob : Finset (Fin 2) → Finset (Finset (Fin 2))), B5 ob ∧ D5 ob ∧ ¬CX ob

theorem b5Needed₀ (ob : Finset (Fin 0) → Finset (Finset (Fin 0))) : CX ob

Over Fin 0, we don't need B5 to get CX.

theorem b5Needed₁ (ob : Finset (Fin 1) → Finset (Finset (Fin 1))) (a5 : A5 ob) : CX ob

Over Fin 1, we don't need B5 to get CX.

def obNonB5 : Finset (Fin 2) → Finset (Finset (Fin 2))

A minimal ob given the constraints (h₀ : {0} ∈ ob {1}) (h₁ : {1} ∉ ob {1}) found in nonCXcondition It satisfies A5, D5, E5, (and C5 and F5 and G5) but not CX (and hence not B5). It clarifies the key role played by B5 in deriving CX.

Equations

• obNonB5 X = if X = {1} then {{0}} else ∅

theorem obNonB5Facts : ¬CX obNonB5 ∧ A5 obNonB5 ∧ C5 obNonB5 ∧ D5 obNonB5 ∧ E5 obNonB5 ∧ F5 obNonB5 ∧ G5 obNonB5

theorem nonCXcondition (ob : Finset (Fin 2) → Finset (Finset (Fin 2))) (h₀ : {0} ∈ ob {1}) (h₁ : {1} ∉ ob {1}) : ¬CX ob

theorem b5Needed : ∃ (ob : Finset (Fin 1) → Finset (Finset (Fin 1))), D5 ob ∧ E5 ob ∧ ¬CX ob ∧ ¬A5 ob

[KH2017] showed that B5 ∧ D5 ∧ E5 |= CX. This shows that B5 is needed. A5 fails too here, as it must when n=1 by b5Needed₁.

def adequate {n : ℕ} (ob : Finset (Fin n) → Finset (Finset (Fin n))) : Prop

ob is the type of model that was sought but not found in [CJ 2022, Observation 5.2]. The concept is a bit obsolete given the limited deontic explosion in that system.

Equations

• adequate ob = (A5 ob ∧ B5 ob ∧ C5 ob ∧ E5 ob ∧ F5 ob ∧ G5 ob ∧ ¬CX ob)

theorem canon₂_II_not_CX {n : ℕ} {A B : Finset (Fin n)} (hA : A ≠ ∅) (hB : B ≠ ∅) (h₂ : Bᶜ ∩ Aᶜ ≠ ∅) : ¬CX (canon₂_II A B)

canon₂_II A B avoids deontic explosion in a general setting: A type of genericity that includes the case A = B.

theorem canon_II_not_CX {n : ℕ} {A : Finset (Fin n)} (hA : A ≠ ∅) (hA' : A ≠ Finset.univ) : ¬CX (canon₂_II A A)

theorem infinitely_many_adequate {n : ℕ} {A : Finset (Fin n)} (hA : A ≠ ∅) (hA' : A ≠ Finset.univ) : adequate (canon₂_II A A)

canon_II generally is adequate (but it does not involve contrary-to-duty obligations). For most A and B, canon₂_II A B is not adequate, by not_canon₂_II_F5, and canon₂ A B is not adequate since by many_not_canon₂_E5, E5 does not hold for it.

theorem injective_canon₂_II {n : ℕ} {A B : Finset (Fin n)} (hBA : canon₂_II A B = canon_II A) : B = A

To show that generalize_F5_canon_II is not trivial.

def modified_obs52 : Finset (Fin 4) → Finset (Finset (Fin 4))

This is the closest canon₂_II analogue of observation_5_2.

Equations

• modified_obs52 = canon₂_II {0, 1} {0, 1, 3}

theorem not_CX_modified_obs52 : ¬CX modified_obs52

theorem canon₂_II_not_CX_of_mutually_generic {n : ℕ} {A B : Finset (Fin n)} (hm : mutually_generic A B) : ¬CX (canon₂_II A B)

A weaker form of canon₂_II_not_CX.