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 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 D5 {U : Type u_1} [Fintype U] [DecidableEq U] (ob : Finset U → Finset (Finset U)) : Prop

Equations

• D5 ob = ∀ (X Y Z : Finset U), Y ⊆ X → 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 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 ob₂ (b : Fin 5 → Bool) : 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 ∧ B5 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 : Set U | T.toFinset ∈ ob S.toFinset}

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

theorem fin_emp {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₀ : B5 ob₀) : CJ5b fun (S : Set U) => {T : Set U | T.toFinset ∈ ob₀ S.toFinset}

theorem inter_toFinset₂ {U : Type} [Fintype U] [DecidableEq U] {X Y : Set U} {hβ : X ∩ Y ≠ ∅} : X.toFinset ∩ Y.toFinset ≠ ∅

Used in aux_toFinset.

theorem 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