Carmo and Jones' system(s) of deontic logic for contrary-to-duty obligations

• Carmo and Jones 2002
• Carmo and Jones 2013
• Kjos-Hanssen 2017
• Carmo and Jones 2022

def CJ5a {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5a ob = ∀ (X : Set U), ∅ ∉ ob X

def CJ5b {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

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

def CJ5c_star {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5c_star ob = ∀ (X : Set U), ∀ β ⊆ ob X, β ≠ ∅ → ⋂₀ β ∩ X ≠ ∅ → ⋂₀ β ∈ ob X

def CJ5c_star_finite {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

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

def CJ5d {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

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

def CJ5e {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

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

def CJ5bd {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5bd ob = ∀ (X Y Z : Set U), Y ∈ ob X ∧ X ⊆ Z → Z \ X ∪ Y ∈ ob Z

def CJ5f {U : Type u_1} (ob : Set U → Set (Set U)) : Prop

Equations

• CJ5f ob = ∀ (β : Set (Set U)), β ≠ ∅ → ∀ (X : Set U), (∀ Z ∈ β, X ∈ ob Z) → X ∈ ob (⋃₀ β)

theorem bd5 {α✝ : Type u_1} {ob : Set α✝ → Set (Set α✝)} (b5 : CJ5b ob) (d5 : CJ5d ob) : CJ5bd ob

theorem first_equality {U : Type u_1} {β : Set (Set U)} {X : Set U} : ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} = ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z = x} ∪ X

theorem subset_of_Union {U : Type} {ob : Set U → Set (Set U)} (b5 : CJ5b ob) (d5 : CJ5d ob) {β : Set (Set U)} {X : Set U} {h3 : ∀ Z ∈ β, X ∈ ob Z} : {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} ⊆ ob (⋃₀ β)

theorem exists_at_beta {U : Type u_1} {β : Set (Set U)} {h2 : β ≠ ∅} : ∃ (B : Set U), B ∈ β

theorem defX {U : Type u_1} {β : Set (Set U)} {X : Set U} {h2 : β ≠ ∅} : X = ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x}

theorem not_empty {U : Type u_1} {ob : Set U → Set (Set U)} {β : Set (Set U)} {X : Set U} {h2 : β ≠ ∅} {h3 : ∀ Z ∈ β, X ∈ ob Z} (a5 : CJ5a ob) : {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} ≠ ∅

theorem inter_not_empty {U : Type u_1} {ob : Set U → Set (Set U)} {β : Set (Set U)} {X : Set U} {h2 : β ≠ ∅} {h3 : ∀ Z ∈ β, X ∈ ob Z} (a5 : CJ5a ob) (b5 : CJ5b ob) : ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} ∩ ⋃₀ β ≠ ∅

theorem II_2_2 {U : Type} {ob : Set U → Set (Set U)} (a5 : CJ5a ob) (b5 : CJ5b ob) (cstar5 : CJ5c_star ob) (d5 : CJ5d ob) : CJ5f ob