Canonical models of Carmo and Jones' systems

Abstract: We show that the two approaches sketched in

• Kjos-Hanssen 2017

are both consistent with

• Carmo Jones 2022.

Preferably, we let F(X) = X ∩ A for a fixed set A.

However, to incorporate contrary-to-duty obligations we introduce a predicate B, where A worlds, A ⊆ B, are the best and B \ A worlds the second best.

Thus, if X ∩ A = ∅ but X ∩ B ≠ ∅, we let F(X) = X ∩ B.

We prove the following results about which axioms hold in which model.

Axiom \ Model	canon	canon_II	canon₂	canon₂_II
A	✓	✓	✓	✓
B	✓	✓	✓	✓
C	✓	✓	✓	✓
D	thus ✓	×	✓	thus ×
E	×	✓	thus ×	✓
F	✓	✓	✓	×!
G	✓	✓	×!	✓

theorem emp_filter₃ {n : ℕ} {A X Y : Finset (Fin n)} (h₀ : Y ⊆ X) (h₁₀ : X ∩ A = ∅) : Y ∩ A = ∅

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

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

theorem inter₃ {n : ℕ} {U X Y Z : Finset (Fin n)} (h₀ : U = X ∩ Y) (h₁ : U = X ∩ Z) : U = X ∩ (Y ∩ Z)

theorem emp_filter₀ {n : ℕ} {B X Y Z : Finset (Fin n)} (h₀ : Y ⊆ X) (h₃ : Y ∩ B = ∅) (h₁ : X ∩ B = X ∩ Z) : Y ∩ Z = ∅

theorem emp_filter₂ {n : ℕ} {A X Y Z : Finset (Fin n)} (h₀ : Y ⊆ X) (h₃ : Y ∩ A = ∅) (h₁ : X ∩ A = X ∩ Z) : Y ∩ Z = ∅

theorem emp_filter₁ {n : ℕ} {A B : Finset (Fin n)} (h : A ⊆ B) {X Y Z : Finset (Fin n)} (h₀ : Y ⊆ X) (h₃ : Y ∩ B = ∅) (h₁ : X ∩ A = X ∩ Z) : Y ∩ Z = ∅

theorem subset_same {n : ℕ} {B X Y Z : Finset (Fin n)} (h₀ : Y ∩ X = Z ∩ X) : X ∩ B ⊆ Y ↔ X ∩ B ⊆ Z

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

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

theorem inter₃₀ {n : ℕ} {A B X Y Z : Finset (Fin n)} (h₁₀ : Y ∩ A = ∅) (h₀ : X ∩ A = X ∩ Y) (h₁ : Y ∩ B = Y ∩ Z) : X ∩ (Y ∩ Z) = ∅

theorem inter₃₁ {n : ℕ} {A B X Y Z : Finset (Fin n)} (h : A ⊆ B) (h₆ : X ∩ A = ∅) (h₀ : X ∩ B = X ∩ Y) (h₁ : Y ∩ A = Y ∩ Z) : X ∩ (Y ∩ Z) = ∅

theorem no_filter₀ : Finset.filter (fun (i : Fin 3) => i = 0 ∨ i = 1) Finset.univ ∩ Finset.filter (fun (i : Fin 3) => i = 0 ∨ i = 2) Finset.univ ≠ ∅

theorem no_filter₁ : Finset.filter (fun (i : Fin 3) => i = 0 ∨ i = 2) Finset.univ ≠ ∅

theorem no_filter₂ : Finset.filter (fun (i : Fin 3) => i = 2) Finset.univ ≠ ∅

theorem no_filter₃ : Finset.filter (fun (i : Fin 3) => i = 0 ∨ i = 1) Finset.univ ∩ Finset.filter (fun (i : Fin 3) => i = 1 ∨ i = 2) Finset.univ ≠ ∅

theorem no_filter₄ : ¬Finset.filter (fun (i : Fin 3) => i = 0 ∨ i = 1) Finset.univ ∩ Finset.filter (fun (i : Fin 3) => i = 0 ∨ i = 2) Finset.univ ⊆ Finset.filter (fun (i : Fin 3) => i = 1 ∨ i = 2) Finset.univ

def canon {n : ℕ} (A : Finset (Fin n)) : Finset (Fin n) → Finset (Finset (Fin n))

Equations

• canon A S = if S ∩ A = ∅ then ∅ else Finset.filter (fun (T : Finset (Fin n)) => S ∩ A ⊆ T) Finset.univ

def canon_II {n : ℕ} (A : Finset (Fin n)) : Finset (Fin n) → Finset (Finset (Fin n))

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 my 2017 paper.

CJ 2022 presumably prefer (II) and 5e. We make a CJ style canon_II by letting ob X = {Y | Y ∩ X = A ∩ X}. My 2017 (II) corresponds to:

Equations

• canon_II A X = if X ∩ A = ∅ then ∅ else Finset.filter (fun (Y : Finset (Fin n)) => X ∩ Y = X ∩ A) Finset.univ

theorem canon_II_symmetry {n : ℕ} (A : Finset (Fin n)) : canon_II A = fun (X : Finset (Fin n)) => if X ∩ A = ∅ then ∅ else Finset.filter (fun (Y : Finset (Fin n)) => X ∩ A = X ∩ Y) Finset.univ

theorem canon_II_E5 {n : ℕ} (A : Finset (Fin n)) : E5 (canon_II A)

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

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

def canon₂ {n : ℕ} (A B : Finset (Fin n)) : Finset (Fin n) → Finset (Finset (Fin n))

Equations

• One or more equations did not get rendered due to their size.

def canon₂_II {n : ℕ} (A B : Finset (Fin n)) : Finset (Fin n) → Finset (Finset (Fin n))

Equations

• One or more equations did not get rendered due to their size.

theorem canon₂_II_A5 {n : ℕ} (A B : Finset (Fin n)) : A5 (canon₂_II A B)

theorem canon₂_II_B5 {n : ℕ} (A B : Finset (Fin n)) : B5 (canon₂_II A B)

theorem canon₂_II_C5 {n : ℕ} (A B : Finset (Fin n)) : C5 (canon₂_II A B)

theorem canon₂_II_E5 {n : ℕ} {A B : Finset (Fin n)} (h : A ⊆ B) : E5 (canon₂_II A B)

theorem canon₂_II_G5 {n : ℕ} {A B : Finset (Fin n)} (h : A ⊆ B) : G5 (canon₂_II A B)

theorem not_canon₂_II_F5 : ∃ (n : ℕ) (A : Finset (Fin n)) (B : Finset (Fin n)), A ⊆ B ∧ ¬F5 (canon₂_II A B)

theorem canon₂_A5 {n : ℕ} (A B : Finset (Fin n)) : A5 (canon₂ A B)

theorem canon₂_B5 {n : ℕ} (A B : Finset (Fin n)) : B5 (canon₂ A B)

theorem canon₂_C5 {n : ℕ} (A B : Finset (Fin n)) : C5 (canon₂ A B)

theorem canon₂_D5 {n : ℕ} {A B : Finset (Fin n)} (h : A ⊆ B) : D5 (canon₂ A B)

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

theorem canon₂_F5 {n : ℕ} (A B : Finset (Fin n)) : F5 (canon₂ A B)

def CJ_all_2022 {n : ℕ} (ob : Finset (Fin n) → Finset (Finset (Fin n))) : 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 {n : ℕ} (ob : Finset (Fin n) → Finset (Finset (Fin n))) : Prop

Equations

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

def CJ_noD_2022 {n : ℕ} (ob : Finset (Fin n) → Finset (Finset (Fin n))) : 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 {n : ℕ} (ob : Finset (Fin n) → Finset (Finset (Fin n))) : Prop

Equations

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

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

Equations

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

theorem CJ_no_DF_canon₂_II {n : ℕ} {A B : Finset (Fin n)} (h : A ⊆ B) : CJ_noDF_2022 (canon₂_II A B)

theorem CJ_no_EG_canon₂ {n : ℕ} {A B : Finset (Fin n)} (h : A ⊆ B) : CJ_noEG_2022 (canon₂ A B)

theorem F5_canon_II {n : ℕ} {A : Finset (Fin n)} : F5 (canon_II A)

theorem CJ_noD_canon_II {n : ℕ} {A : Finset (Fin n)} : CJ_noD_2022 (canon_II A)

theorem CJ_noE_canon {n : ℕ} {A : Finset (Fin n)} : CJ_noE_2022 (canon A)

theorem coincidence {n : ℕ} : canon Finset.univ = canon_II Finset.univ

theorem CJ_all_canon_univ {n : ℕ} : CJ_all_2022 (canon Finset.univ)

We prove that 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(∅)=∅.