Canonical models of CJ 2022 axioms

We demonstrate that Carmo and Jones 2022 axioms 5(a)(b)(c)(g) do not imply their 5(d) or 5(f). We also show that 5(a)(b)(c)(d)(f)(g) together do not imply 5(e). This is done using two-world model counterexamples.

None of the other axioms imply 5a: consider the no-worlds model (which contradicts CJ axiom 1) with ∅ ∈ ob ∅.

We show that the system has arbitrarily large models.

def A5 {U : Type u_1} [Fintype U] (ob : Finset U → Finset (Finset U)) : Prop

Equations

• A5 ob = ∀ (X : Finset U), ∅ ∉ ob X

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

Equations

• B5 ob = ∀ (X Y Z : Finset U), Y ∩ X = Z ∩ X → Y ∈ ob X → Z ∈ ob X

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

Equations

• B5original ob = ∀ (X Y Z : Finset U), Y ∩ X = Z ∩ X → (Y ∈ ob X ↔ Z ∈ ob X)

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

Equations

• C5 ob = ∀ (X Y Z : Finset U), Y ∈ ob X → Z ∈ ob X → X ∩ Y ∩ Z ≠ ∅ → Y ∩ Z ∈ ob X

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

An axiom going back to the 1990s.

Equations

• C5Strong ob = ∀ (X Y Z : Finset U), Y ∈ ob X → Z ∈ ob X → Y ∩ Z ∈ ob X

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

5c*_2013 = 5c_2022 def CJ5c_star (ob : Set U → Set (Set U)) := ∀ (X : Set U) (β : Set (Set U)), (h1 : β ⊆ ob X) → (h2 : β ≠ ∅) → ⋂₀β ∩ X ≠ ∅ → ⋂₀β ∈ ob X

Equations

• D5 ob = ∀ (X Y Z : Finset U), Y ⊆ X → Y ∈ ob X → X ⊆ Z → Z \ X ∪ Y ∈ ob Z

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

Equations

• BD5 ob = ∀ (X Y Z : Finset U), Y ∈ ob X → X ⊆ Z → Z \ X ∪ Y ∈ ob Z

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

Equations

• E5 ob = ∀ (X Y Z : Finset U), Y ⊆ X → Z ∈ ob X → Y ∩ Z ≠ ∅ → Z ∈ ob Y

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

Equations

• E5weak ob = ∀ (Y Z : Finset U), Z ∈ ob Finset.univ → Y ∩ Z ≠ ∅ → Z ∈ ob Y

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

Equations

• F5 ob = ∀ (X Y Z : Finset U), X ∈ ob Y → X ∈ ob Z → X ∈ ob (Y ∪ Z)

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

Equations

• G5 ob = ∀ (X Y Z : Finset U), Y ∈ ob X → Z ∈ ob Y → X ∩ Y ∩ Z ≠ ∅ → Y ∩ Z ∈ ob X

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

Weak conditional deontic explosion, implicit in [KH17].

Equations

• CXweak ob = ∀ (A B : Finset U), A ∈ ob Finset.univ → B \ A ≠ ∅ → B ∈ ob Aᶜ

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

Full conditional deontic explosion, implicit in [KH17]. Many variations of this statement could be considered.

Equations

• CX ob = ∀ (A B C : Finset U), A ∈ ob C → B ∩ Aᶜ ∩ C ≠ ∅ → B ∈ ob (Aᶜ ∩ C)

theorem CXimpliesWeak {U : Type u_1} [Fintype U] [DecidableEq U] (ob : Finset U → Finset (Finset U)) (h : CX ob) : CXweak ob

def ob₂ (b : Fin 5 → Bool) (B : Finset (Fin 2)) : Finset (Finset (Fin 2))

All the ob's satisfying 5(a) and 5(b) in a two-world domain.

Equations

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

theorem ob₂5a (b : Fin 5 → Bool) : A5 (ob₂ b)

theorem ob₂5b (b : Fin 5 → Bool) : B5 (ob₂ b)

theorem ob₂5c (b : Fin 5 → Bool) : C5 (ob₂ b)

theorem ob₂5d (b : Fin 5 → Bool) : ((b 0 || b 1) = true → b 2 = true) → D5 (ob₂ b)

theorem ob₂5e (b : Fin 5 → Bool) : b 0 = b 1 → b 1 = b 2 → (b 3 = true → b 0 = true) → (b 4 = true → b 1 = true) → E5 (ob₂ b)

theorem ob₂5f (b : Fin 5 → Bool) : ((b 0 || b 1) = true → b 2 = true) → F5 (ob₂ b)

theorem ob₂5g (b : Fin 5 → Bool) : G5 (ob₂ b)

theorem do_not_imply_5d_or_5f : ∃ (ob : Finset (Fin 2) → Finset (Finset (Fin 2))), A5 ob ∧ B5original ob ∧ C5 ob ∧ ¬D5 ob ∧ E5 ob ∧ ¬F5 ob ∧ G5 ob

def converter {U : Type} [Fintype U] (ob : Finset U → Finset (Finset U)) : Set U → Set (Set U)

Equations

• converter ob S T = (T.toFinset ∈ ob S.toFinset)

theorem empty_finset {U : Type} [Fintype U] {X : Set U} (h : X.toFinset = ∅) : X = ∅

theorem toFinset_empty' {U : Type} [Fintype U] : ∅ = ∅.toFinset

theorem get_5a {U : Type} [Fintype U] {ob₀ : Finset U → Finset (Finset U)} (hob₀ : A5 ob₀) : CJ5a fun (S : Set U) => {T : Set U | T.toFinset ∈ ob₀ S.toFinset}

theorem get_5b {U : Type} [Fintype U] [DecidableEq U] {ob₀ : Finset U → Finset (Finset U)} (hob₀ : B5original ob₀) : CJ5b fun (S : Set U) => {T : Set U | T.toFinset ∈ ob₀ S.toFinset}

theorem inter_inter_toFinset {U : Type} [Fintype U] [DecidableEq U] {X Y Z : Set U} (h₀ : X ∩ Y ∩ Z ≠ ∅) : X.toFinset ∩ Y.toFinset ∩ Z.toFinset ≠ ∅

theorem get_5c {U : Type} [Fintype U] [DecidableEq U] {ob₀ : Finset U → Finset (Finset U)} (hob₀ : C5 ob₀) : CJ5c_star_finite fun (S : Set U) => {T : Set U | T.toFinset ∈ ob₀ S.toFinset}

theorem get_not_5d {U : Type} [Fintype U] [DecidableEq U] {ob₀ : Finset U → Finset (Finset U)} (hob₀ : ¬D5 ob₀) : ¬CJ5d fun (S : Set U) => {T : Set U | T.toFinset ∈ ob₀ S.toFinset}

theorem Set_result_from_computation : ∃ (U : Type) (ob : Set U → Set (Set U)), CJ5a ob ∧ CJ5b ob ∧ CJ5c_star_finite ob ∧ ¬CJ5d ob

theorem do_not_imply_5e : ∃ (ob : Finset (Fin 2) → Finset (Finset (Fin 2))), A5 ob ∧ B5 ob ∧ C5 ob ∧ D5 ob ∧ ¬E5 ob ∧ F5 ob ∧ G5 ob