The system of Carmo and Jones 1997

def stayAlive {α : Type u_1} [Fintype α] [DecidableEq α] (e : α) : Finset α → Finset (Finset α)

Equations

• stayAlive e X = {Y : Finset α | X ∩ Y ≠ ∅ ∧ X \ {e} ⊆ X ∩ Y}

def stayAlive' {n : ℕ} (e : Fin n) : Finset (Fin n) → Finset (Finset (Fin n))

Equations

• stayAlive' e X = {Y : Finset (Fin n) | X ∩ Y ≠ ∅ ∧ X \ {e} ⊆ Y}

theorem stayAlive_eq_stayAlive' {n : ℕ} (e : Fin n) : stayAlive e = stayAlive' e

def alive₀ (α : Type u_1) [Fintype α] [DecidableEq α] : Finset α → Finset (Finset α)

Equations

• alive₀ α X = {Y : Finset α | X ≠ ∅ ∧ X ⊆ Y}

def alive (n : ℕ) : Finset (Fin n) → Finset (Finset (Fin n))

A version of stayAlive where e is missing, or if you will, e = n ∉ Fin n.

Equations

• alive n X = {Y : Finset (Fin n) | X ≠ ∅ ∧ Y ⊇ X}

theorem alive_properties (n : ℕ) : A5 (alive n) ∧ B5 (alive n) ∧ C5Strong (alive n) ∧ D5 (alive n) ∧ E5 (alive n)

theorem stayAlive_properties {n : ℕ} (e : Fin n) : A5 (stayAlive e) ∧ B5 (stayAlive e) ∧ C5Strong (stayAlive e) ∧ D5 (stayAlive e) ∧ E5 (stayAlive e)

This shows that the system studied in "A new approach to contrary-to-duty obligations" (1997) in 1996 has infinitely many models. June 4, 2025.

def small₂ {n : ℕ} (A : Finset (Fin n)) : Prop

Equations

• small₂ A = (2 ≤ Aᶜ.card)

theorem card_ge_two {k : ℕ} (A : Finset (Fin k)) : 2 ≤ A.card ↔ ∃ a ∈ A, ∃ b ∈ A, a ≠ b

A convenient companion lemma for card_le_one.

def ccss {n : ℕ} (B A : Finset (Fin n)) : Prop

A is a conditional cosubsingleton within B.

Equations

• ccss B A = (A ⊆ B → (B \ A).card ≤ 1)

def cocos {n : ℕ} (B : Finset (Fin n)) : Finset (Finset (Fin n))

A is a cocos in B if it's not a subset of B, or else is a cosubsingleton of B.

Equations

• cocos B = {A : Finset (Fin n) | A ⊆ B → (B \ A).card ≤ 1}

theorem alive_ne_cocos : alive 1 ≠ cocos

Although alive and cocos are the same type of thing, they are quite different. However, alive ⊆ cocos so alive is covering; and indeed stayAlive and noObligations are too by our main theorem.

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

A is relatively obligatory given B. A ∈ ifsub ob B means that A ∈ ob B, if it should happen that A ⊆ B.

Equations

• ifsub ob B = {A : Finset (Fin n) | A ⊆ B → A ∈ ob B}

theorem ifsub_apply {n : ℕ} {ob : Finset (Fin n) → Finset (Finset (Fin n))} {A B : Finset (Fin n)} (h : A ∈ ifsub ob B) (h₀ : A ⊆ B) : A ∈ ob B

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

ob has the drop_at_most_one property if whenever a subset is obligatory, it is a relative cosubsingleton

Equations

• covering ob = ∀ (C B : Finset (Fin n)), B ∈ ob C → B ∈ cocos C

theorem covering_def {n : ℕ} (ob : Finset (Fin n) → Finset (Finset (Fin n))) : covering ob ↔ ∀ (C : Finset (Fin n)), ob C ⊆ cocos C

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

A context A is inter_ifsub obligatory if A is obligatory in any larger context.

Equations

• inter_ifsub ob A = ∀ (X : Finset (Fin n)), A ∈ ifsub ob X

def cosubsingleton {n : ℕ} (A : Finset (Fin n)) : Prop

Equations

• cosubsingleton A = (Aᶜ.card ≤ 1)

theorem cosubsingleton_eq_ccss_univ {n : ℕ} (A : Finset (Fin n)) : cosubsingleton A ↔ ccss Finset.univ A

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

Not only is a "bad" but there is an obligation that singles it out.

Equations

• bad ob a = ∃ (X : Finset (Fin n)), a ∈ X ∧ X \ {a} ∈ ob X

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

Equations

• quasibad ob a = ∃ (X : Finset (Fin n)) (Y : Finset (Fin n)), a ∈ X \ Y ∧ Y ∈ ob X

def noObligations' (α : Type u_1) [Fintype α] [DecidableEq α] : Finset α → Finset (Finset α)

Equations

• noObligations' α x✝ = ∅

def noObligations (n : ℕ) : Finset (Fin n) → Finset (Finset (Fin n))

The model according to which there are no obligations at all.

Equations

• noObligations n x✝ = ∅

theorem diff_diff {n : ℕ} {X Y : Finset (Fin n)} : X ∩ Y = Y \ (Y \ X)

structure BDE {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} : Prop

Putting the commonly combined axioms 5(b)(d)(e) into a structure.

• b5 : B5 ob
• d5 : D5 ob
• e5 : E5 ob

theorem insert_single_ob_pair {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} {A : Finset (Fin k)} (d5 : D5 ob) {a₁ a₂ : Fin k} (ha₁₂ : a₁ ≠ a₂) (h : inter_ifsub ob A) : A ∪ {a₂} ∈ ob (A ∪ {a₁, a₂})

If we add two worlds to a inter_ifsub set, then each one is preferable to the other.

theorem single_ob_pair₁ {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (c5 : C5 ob) (d5 : D5 ob) (e5 : E5 ob) {A : Finset (Fin k)} {a₁ a₂ : Fin k} (ha₂ : a₁ ≠ a₂) (ha₁ : a₂ ∉ A) (hcorr : {a₁, a₂} ∈ ob {a₁, a₂}) (h : inter_ifsub ob A) : {a₁} ∈ ob {a₁, a₂}

theorem single_ob_pair {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (c5 : C5 ob) (d5 : D5 ob) (e5 : E5 ob) {A : Finset (Fin k)} {a₁ a₂ : Fin k} (ha₂ : a₁ ≠ a₂) (ha₀ : a₁ ∉ A) (ha₁ : a₂ ∉ A) (hcorr : {a₁, a₂} ∈ ob {a₁, a₂}) (h : inter_ifsub ob A) : {a₁} ∈ ob {a₁, a₂} ∧ {a₂} ∈ ob {a₁, a₂}

A weaker version using the weaker C5 axiom.

theorem C5_of_C5Strong {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (c5 : C5Strong ob) : C5 ob

structure ACDE {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} : Prop

• a : A5 ob
• c : C5Strong ob
• d : D5 ob
• e : E5 ob

theorem semiglobal_holds {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (f : ACDE) {A : Finset (Fin k)} {a₁ a₂ : Fin k} (ha₂ : a₁ ≠ a₂) (ha₀ : a₁ ∉ A) (ha₁ : a₂ ∉ A) (h : inter_ifsub ob A) : {a₁, a₂} ∉ ob {a₁, a₂}

If A is missing a self-obligatory pair then A is not inter_ifsub. A key use of the (too) strong version C5Strong.

structure ADE {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} : Prop

• a5 : A5 ob
• d5 : D5 ob
• e5 : E5 ob

structure ABCDE {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} : Prop

• a5 : A5 ob
• b5 : B5 ob
• c5 : C5Strong ob
• d5 : D5 ob
• e5 : E5 ob

theorem global_holds_specific {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) {A : Finset (Fin k)} {a₁ a₂ : Fin k} (h₁ : a₁ ∉ A) (h₂ : a₂ ∉ A) (h₁₂ : a₁ ≠ a₂) : ¬inter_ifsub ob A

If A is small₂ (missing a pair of worlds) then A is not inter_ifsub.

theorem obSelfSdiff_of_bad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : BDE) {a : Fin k} (hbad : bad ob a) {Y : Finset (Fin k)} (han : Y \ {a} ≠ ∅) : Y \ {a} ∈ ob Y

theorem obSelf_of_obSelf {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : BDE) {X Y : Finset (Fin k)} (hX : X ∈ ob X) (hY : Y ≠ ∅) : Y ∈ ob Y

theorem obSelf_univ {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (d5 : D5 ob) (e5 : E5 ob) (a : Fin k) (ha : Finset.univ \ {a} ∈ ob Finset.univ) : Finset.univ ∈ ob Finset.univ

theorem sdiff_union_sdiff {k : ℕ} (A B C : Finset (Fin k)) : A \ C ⊆ A \ B ∪ B \ C

theorem diff_ne {k : ℕ} {a : Fin k} {X : Finset (Fin k)} (ha : X ≠ {a}) (he : X ≠ ∅) : X \ {a} ≠ ∅

theorem sdiff_union_sdiff_eq {k : ℕ} {a : Fin k} {X : Finset (Fin k)} (ha : a ∈ X) : Finset.univ \ {a} = Finset.univ \ X ∪ X \ {a}

theorem local_of_global_theoretical {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (d5 : D5 ob) (e5 : E5 ob) (h : ∀ (A : Finset (Fin k)), (∀ (B : Finset (Fin k)), A ∈ ifsub ob B) → ∀ (B : Finset (Fin k)), ccss B A) {A B : Finset (Fin k)} (hBC₁ : A ∈ ifsub ob B) : ccss B A

If every everywhere-inter_ifsub set is a cosubsingleton of univ then every somewhere-inter_ifsub set is a cosubsingleton there. Because we can just union up with the relative complement.

This version is "theoretical" in that it is not so easy to apply but has a beautiful logical structure.

theorem local_of_global' {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (d5 : D5 ob) (e5 : E5 ob) {B C : Finset (Fin k)} (hBC₀ : (C \ B).card ≥ 2) (hBC₁ : B ⊆ C) (hBC₂ : B ∈ ob C) : ∃ (A : Finset (Fin k)), Aᶜ.card ≥ 2 ∧ inter_ifsub ob A

A trivial consequence of local_of_global_theoretical.

theorem local_of_global {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (d5 : D5 ob) (e5 : E5 ob) (large_of_ob : ∀ (A : Finset (Fin k)), inter_ifsub ob A → cosubsingleton A) : covering ob

Given that no small₂ set is inter_ifsub (which is not automatic here since we don't assume B5 and C5), an obligatory set cannot be more than 1 world away from its larger context.

If every universally inter_ifsub set is cosubsingle then every somewhere inter_ifsub set is there-cosubsingle.

theorem global_holds {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) (A : Finset (Fin k)) (hs : small₂ A) : ¬inter_ifsub ob A

If A is small₂ then A is not inter_ifsub. This is just some set-wrangling on top of global_holds_specific.

theorem local_holds {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) : covering ob

A direct consequence of global_holds and local_of_global.

def local_holds_apply {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) {B C : Finset (Fin k)} : C ∈ ob B → C ∈ cocos B

Allow B and C to be implicit in local_holds.

Equations

• ⋯ = ⋯

theorem obSelf_of_ob_of_subset {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (b5 : B5 ob) {X Y : Finset (Fin k)} (hd : Y ⊆ X) (h : X ∈ ob Y) : Y ∈ ob Y

An obvious consequence of B5.

theorem not_ob_of_almost {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (H₁ : ∀ (a : Fin k), ¬quasibad ob a) {X Y : Finset (Fin k)} (h₀ : (Y \ X).card = 1) : X ∉ ob Y

theorem obSelf_of_ob_of_almost_subset {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (b5 : B5 ob) (H₁ : ∀ (a : Fin k), ¬quasibad ob a) {X Y : Finset (Fin k)} (h : X ∈ ob Y) (hd : (Y \ X).card ≤ 1) : Y ∈ ob Y

theorem bad_of_quasibad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (b5 : B5 ob) (e5 : E5 ob) (a : Fin k) (h : quasibad ob a) : bad ob a

The anonymous referee's proof.

theorem sub_alive {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (b5 : B5 ob) (H₁ : ∀ (a : Fin k), ¬quasibad ob a) (Y : Finset (Fin k)) : ob Y ⊆ alive k Y

theorem alive_sub {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) (H₀ : ob ≠ noObligations k) (H₁ : ∀ (a : Fin k), ¬quasibad ob a) (Y : Finset (Fin k)) : alive k Y ⊆ ob Y

theorem alive_of_no_quasibad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) (H₀ : ob ≠ noObligations k) (H₁ : ∀ (a : Fin k), ¬quasibad ob a) : ob = alive k

theorem unique_bad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) {a b : Fin k} (ha : bad ob a) (hb : bad ob b) : a = b

theorem bad_cosubsingleton_of_ob {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) {a : Fin k} (hbad : bad ob a) {X Y : Finset (Fin k)} (h' : X ∩ Y ∈ ob X) : X ∩ Y = X ∨ X ∩ Y = X \ {a}

theorem obSelf_of_obSelfSdiff {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : BDE) {X : Finset (Fin k)} {a : Fin k} (h : X \ {a} ∈ ob X) (han : X \ {a} ≠ ∅) : X ∈ ob X

theorem obSelf_of_bad.nonsingle {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : BDE) {a : Fin k} (hbad : bad ob a) {X : Finset (Fin k)} (ha : X ≠ {a}) (he : X ≠ ∅) : X ∈ ob X

If X contains an element b≠a where a is a given bad world, then X is self-obligatory.

theorem obSelf_of_bad.single {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (b5 : B5 ob) (d5 : D5 ob) (e5 : E5 ob) {a : Fin k} (hbad : bad ob a) : {a} ∈ ob {a}

Bad singletons are self-obligatory. Proved from first principles.

theorem obSelf_of_bad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (b5 : B5 ob) (d5 : D5 ob) (e5 : E5 ob) (hbad : ∃ (a : Fin k), bad ob a) {X : Finset (Fin k)} (he : X ≠ ∅) : X ∈ ob X

theorem sub_stayAlive_of_bad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) {a : Fin k} (hbad : bad ob a) (Y : Finset (Fin k)) : ob Y ⊆ stayAlive a Y

theorem stayAlive_sub_of_bad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (a5 : A5 ob) (b5 : B5 ob) (d5 : D5 ob) (e5 : E5 ob) {a : Fin k} (hbad : bad ob a) (Y : Finset (Fin k)) : stayAlive a Y ⊆ ob Y

theorem stayAlive_of_bad {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) {a : Fin k} (hbad : bad ob a) : ob = stayAlive a

theorem models_ofCJ_1997 {k : ℕ} {ob : Finset (Fin k) → Finset (Finset (Fin k))} (t : ABCDE) : (∃ (a : Fin k), ob = stayAlive a) ∨ ob = alive k ∨ ob = noObligations k

There are only three models of CJ 1997 for a given n ≥ 1: stayAlive, alive, noObligations.

theorem models_ofCJ_1997₀ (ob : Finset (Fin 0) → Finset (Finset (Fin 0))) (a5 : A5 ob) : ob = alive 0 ∧ ob = noObligations 0

theorem setsFin1 (X : Finset (Fin 1)) (h₀ : X ≠ {0}) : X = ∅

theorem models_ofCJ_1997₁ (ob : Finset (Fin 1) → Finset (Finset (Fin 1))) (a5 : A5 ob) (b5 : B5 ob) : (∃ (a : Fin 1), ob = stayAlive a) ∨ ob = alive 1 ∨ ob = noObligations 1

An exhaustive list of models of A5 ∧ B5 over Fin 1. The first two alternatives are actually the same

theorem models_ofCJ_1997_equiv {n : ℕ} (ob : Finset (Fin n) → Finset (Finset (Fin n))) : A5 ob ∧ B5 ob ∧ C5Strong ob ∧ D5 ob ∧ E5 ob ↔ (∃ (a : Fin n), ob = stayAlive a) ∨ ob = alive n ∨ ob = noObligations n