Theory CJDDLplus

(*<*)
theory CJDDLplus
  imports Main
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3]
(*>*)

section ‹Introduction›
text‹\noindent{We present an encoding of an ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency (PGC)"--- 
in Isabelle/HOL. The PGC has stirred much attention in philosophy and ethics \<^cite>‹"Beyleveld"› and has been proposed as a
potential means to bound the impact of artificial general intelligence (AGI) \<^cite>‹"Kornai"›.
With our contribution we make a first, important step towards formally assessing the PGC and its potential applications in AI.
Our formalisation utilises the shallow semantical embedding approach \<^cite>‹"J23"›
and adapts a recent embedding of dyadic deontic logic in HOL \<^cite>‹"C71"› \<^cite>‹"BenzmuellerDDL"›.
}›

section ‹Semantic Embedding of Carmo and Jones' Dyadic Deontic Logic (DDL) augmented with Kaplanian contexts›

text‹\noindent{We introduce a modification of the semantic embedding developed by Benzm\"uller et al. \<^cite>‹"C71"› \<^cite>‹"BenzmuellerDDL"›
for the Dyadic Deontic Logic originally presented by Carmo and Jones \<^cite>‹"CJDDL"›. We extend this embedding
to a two-dimensional semantics as originally presented by David Kaplan \<^cite>‹"Kaplan1979"› \<^cite>‹"Kaplan1989"›.}›

subsection ‹Definition of Types›

typedecl w   ― ‹  Type for possible worlds (Kaplan's "circumstances of evaluation" or "counterfactual situations")  ›
typedecl e   ― ‹  Type for individuals (entities eligible to become agents) ›
typedecl c   ― ‹  Type for Kaplanian "contexts of use" ›
type_synonym wo = "w⇒bool" ― ‹  contents/propositions are identified with their truth-sets ›
type_synonym cwo = "c⇒wo"  ― ‹  sentence meaning (Kaplan's "character") is a function from contexts to contents ›
type_synonym m = "cwo"      ― ‹  we use the letter 'm' for characters (reminiscent of "meaning") ›

subsection ‹Semantic Characterisation of DDL› (*cf. original Carmo and Jones Paper @{cite "CJDDL"} p.290ff*)

subsubsection ‹Basic Set Operations›
abbreviation subset::"wo⇒wo⇒bool" (infix ‹⊑› 46) where "α ⊑ β ≡ ∀w. α w  ⟶ β w"
abbreviation intersection::"wo⇒wo⇒wo" (infixr ‹⊓› 48) where "α ⊓ β ≡ λx. α x ∧ β x"
abbreviation union::"wo⇒wo⇒wo" (infixr ‹⊔› 48) where "α ⊔ β ≡ λx. α x ∨ β x"
abbreviation complement::"wo⇒wo" (‹∼_›[45]46) where "∼α ≡ λx. ¬α x"
abbreviation instantiated::"wo⇒bool" (‹ℐ_›[45]46) where "ℐ φ ≡ ∃x. φ x"
abbreviation setEq::"wo⇒wo⇒bool" (infix ‹=⇩_s› 46) where "α =⇩_s β ≡ ∀x. α x ⟷ β x"
abbreviation univSet :: "wo" (‹⊤›) where "⊤ ≡ λw. True"
abbreviation emptySet :: "wo" (‹⊥›) where "⊥ ≡ λw. False"

subsubsection ‹Set-Theoretic Conditions for DDL›

consts
av::"w⇒wo"   ― ‹ set of worlds that are open alternatives (aka. actual versions) of w ›
pv::"w⇒wo"   ― ‹ set of worlds that are possible alternatives (aka. potential versions) of w ›
ob::"wo⇒wo⇒bool" ― ‹ set of propositions which are obligatory in a given context (of type wo)  ›

axiomatization where
sem_3a: "∀w. ℐ(av w)" and ― ‹  av is serial: in every situation there is always an open alternative ›
sem_4a: "∀w. av w ⊑ pv w" and ― ‹  open alternatives are possible alternatives ›
sem_4b: "∀w. pv w w" and ― ‹  pv is reflexive: every situation is a possible alternative to itself ›
sem_5a: "∀X. ¬(ob X ⊥)" and ― ‹  contradictions cannot be obligatory ›
sem_5b: "∀X Y Z. (X ⊓ Y) =⇩_s (X ⊓ Z) ⟶ (ob X Y ⟷ ob X Z)" and
sem_5c: "∀X Y Z. ℐ(X ⊓ Y ⊓ Z) ∧ ob X Y ∧ ob X Z ⟶ ob X (Y ⊓ Z)" and
sem_5d: "∀X Y Z. (Y ⊑ X ∧ ob X Y ∧ X ⊑ Z) ⟶ ob Z ((Z ⊓ (∼X)) ⊔ Y)" and
sem_5e: "∀X Y Z. Y ⊑ X ∧ ob X Z ∧ ℐ(Y ⊓ Z) ⟶ ob Y Z"

lemma True nitpick[satisfy] oops ― ‹ model found: axioms are consistent ›

subsubsection ‹Verifying Semantic Conditions›

lemma sem_5b1: "ob X Y ⟶ ob X (Y ⊓ X)" by (metis (no_types, lifting) sem_5b)
lemma sem_5b2: "(ob X (Y ⊓ X) ⟶ ob X Y)" by (metis (no_types, lifting) sem_5b) 
lemma sem_5ab: "ob X Y ⟶ ℐ(X ⊓ Y)" by (metis (full_types) sem_5a sem_5b)
lemma sem_5bd1: "Y ⊑ X ∧ ob X Y ∧ X ⊑ Z ⟶ ob Z ((∼X) ⊔ Y)" using sem_5b sem_5d by smt
lemma sem_5bd2: "ob X Y ∧ X ⊑ Z ⟶ ob Z ((Z ⊓ (∼X)) ⊔ Y)"  using sem_5b sem_5d  by (smt (z3) sem_5b1)  
lemma sem_5bd3: "ob X Y ∧ X ⊑ Z ⟶ ob Z ((∼X) ⊔ Y)"  by (smt (z3) sem_5bd2 sem_5b) 
lemma sem_5bd4: "ob X Y ∧ X ⊑ Z ⟶ ob Z ((∼X) ⊔ (X ⊓  Y))" using sem_5bd3 by auto
lemma sem_5bcd: "(ob X Z ∧ ob Y Z) ⟶ ob (X ⊔ Y) Z" using sem_5b sem_5c sem_5d oops

(* 5e and 5ab justify redefinition of @{cite "O⟨φ|σ⟩"} as (ob A B)*)
lemma "ob A B ⟷  (ℐ(A ⊓ B) ∧ (∀X. X ⊑ A ∧ ℐ(X ⊓ B) ⟶ ob X B))" using sem_5e sem_5ab by blast

subsection ‹(Shallow) Semantic Embedding of DDL›

subsubsection ‹Basic Propositional Logic›
abbreviation pand::"m⇒m⇒m" (infixr‹❙∧› 51) where "φ❙∧ψ ≡ λc w. (φ c w)∧(ψ c w)"
abbreviation por::"m⇒m⇒m" (infixr‹❙∨› 50) where "φ❙∨ψ ≡ λc w. (φ c w)∨(ψ c w)"
abbreviation pimp::"m⇒m⇒m" (infix‹❙→› 49) where "φ❙→ψ ≡ λc w. (φ c w)⟶(ψ c w)"
abbreviation pequ::"m⇒m⇒m" (infix‹❙↔› 48) where "φ❙↔ψ ≡ λc w. (φ c w)⟷(ψ c w)"
abbreviation pnot::"m⇒m" (‹❙¬_› [52]53) where "❙¬φ ≡ λc w. ¬(φ c w)"

subsubsection ‹Modal Operators›
abbreviation cjboxa :: "m⇒m" (‹❙□⇩_a_› [52]53) where "❙□⇩_aφ ≡ λc w. ∀v. (av w) v ⟶ (φ c v)"
abbreviation cjdiaa :: "m⇒m" (‹❙◇⇩_a_› [52]53) where "❙◇⇩_aφ ≡ λc w. ∃v. (av w) v ∧ (φ c v)"
abbreviation cjboxp :: "m⇒m" (‹❙□⇩_p_› [52]53) where "❙□⇩_pφ ≡ λc w. ∀v. (pv w) v ⟶ (φ c v)"
abbreviation cjdiap :: "m⇒m" (‹❙◇⇩_p_› [52]53) where "❙◇⇩_pφ ≡ λc w. ∃v. (pv w) v ∧ (φ c v)"
abbreviation cjtaut :: "m" (‹❙⊤›) where "❙⊤ ≡ λc w. True"
abbreviation cjcontr :: "m" (‹❙⊥›) where "❙⊥ ≡ λc w. False"

subsubsection ‹Deontic Operators›
abbreviation cjod :: "m⇒m⇒m" (‹❙O⟨_|_⟩›54) where "❙O⟨φ|σ⟩ ≡ λc w. ob (σ c) (φ c)"
abbreviation cjoa :: "m⇒m" (‹❙O⇩_a_› [53]54) where "❙O⇩_aφ ≡ λc w. (ob (av w)) (φ c) ∧ (∃x. (av w) x ∧ ¬(φ c x))"
abbreviation cjop :: "m⇒m" (‹❙O⇩_i_› [53]54) where "❙O⇩_iφ ≡ λc w. (ob (pv w)) (φ c) ∧ (∃x. (pv w) x ∧ ¬(φ c x))"

subsubsection ‹Logical Validity (Classical)›
abbreviation modvalidctx :: "m⇒c⇒bool" (‹⌊_⌋⇧^M›) where "⌊φ⌋⇧^M ≡ λc. ∀w. φ c w" ― ‹ context-dependent modal validity ›
abbreviation modvalid :: "m⇒bool" (‹⌊_⌋›) where "⌊φ⌋ ≡ ∀c. ⌊φ⌋⇧^M c" ― ‹ general modal validity (modally valid in each context) ›

(*
If we introduce the alternative definition of logical validity below (from Kaplan's LD) instead of the previous one,
we can prove valid most of the following theorems excepting only CJ_7 and CJ_8 and the necessitation rule.

consts World::"c⇒w"  ― ‹ function retrieving the world corresponding to context c (Kaplanian contexts are world-centered) ›        
abbreviation ldtruectx::"m⇒c⇒bool" ("⌊_⌋⇩_{_}") where "⌊φ⌋⇩_c ≡ φ c (World c)" ― ‹  truth in the given context ›
abbreviation ldvalid::"m⇒bool" ("⌊_⌋") where "⌊φ⌋ ≡ ∀c. ⌊φ⌋⇩_c"    ― ‹  LD validity (true in every context) ›
*)

subsection ‹Verifying the Embedding›

subsubsection ‹Avoiding Modal Collapse›
lemma "⌊P ❙→ ❙O⇩_aP⌋" nitpick oops ― ‹ (actual) deontic modal collapse is countersatisfiable ›
lemma "⌊P ❙→ ❙O⇩_iP⌋" nitpick oops ― ‹ (ideal) deontic modal collapse is countersatisfiable ›
lemma "⌊P ❙→ ❙□⇩_aP⌋" nitpick oops ― ‹ alethic modal collapse is countersatisfiable (implies all other necessity operators) ›

subsubsection ‹Necessitation Rule›
lemma NecDDLa: "⌊A⌋ ⟹ ⌊❙□⇩_aA⌋"  by simp (* Valid only using classical (not LD) validity*)
lemma NecDDLp:  "⌊A⌋ ⟹ ⌊❙□⇩_pA⌋" by simp (* Valid only using classical (not LD) validity*)

subsubsection ‹Lemmas for Semantic Conditions› (* extracted from Benzmüller et al. paper @{cite "BenzmuellerDDL"}*)

abbreviation mboxS5 :: "m⇒m" (‹❙□⇧^S⇧⁵_› [52]53) where "❙□⇧^S⇧⁵φ ≡ λc w. ∀v. φ c v"
abbreviation mdiaS5 :: "m⇒m" (‹❙◇⇧^S⇧⁵_› [52]53) where "❙◇⇧^S⇧⁵φ ≡ λc w. ∃v. φ c v"

lemma C_2: "⌊❙O⟨A | B⟩ ❙→ ❙◇⇧^S⇧⁵(B ❙∧ A)⌋" by (simp add: sem_5ab)
lemma C_3:  "⌊((❙◇⇧^S⇧⁵(A ❙∧ B ❙∧ C)) ❙∧ ❙O⟨B|A⟩ ❙∧ ❙O⟨C|A⟩) ❙→ ❙O⟨(B ❙∧ C)| A⟩⌋" by (simp add: sem_5c)
lemma C_4: "⌊(❙□⇧^S⇧⁵(A ❙→ B) ❙∧ ❙◇⇧^S⇧⁵(A ❙∧ C) ❙∧ ❙O⟨C|B⟩) ❙→ ❙O⟨C|A⟩⌋" using sem_5e by blast
lemma C_5: "⌊❙□⇧^S⇧⁵(A ❙↔ B) ❙→ (❙O⟨C|A⟩ ❙→ ❙O⟨C|B⟩)⌋" using C_2 sem_5e by blast
lemma C_6: "⌊❙□⇧^S⇧⁵(C ❙→ (A ❙↔ B)) ❙→ (❙O⟨A|C⟩ ❙↔ ❙O⟨B|C⟩)⌋" by (metis sem_5b)
lemma C_7: "⌊❙O⟨B|A⟩ ❙→ ❙□⇧^S⇧⁵❙O⟨B|A⟩⌋" by blast 
lemma C_8: "⌊❙O⟨B|A⟩ ❙→ ❙O⟨A ❙→ B| ❙⊤⟩⌋" using sem_5bd4 by presburger

subsubsection ‹Verifying Axiomatic Characterisation›

text‹\noindent{The following theorems have been taken from the original Carmo and Jones' paper (\<^cite>‹"CJDDL"› p.293ff).}›

lemma CJ_3: "⌊❙□⇩_pA ❙→ ❙□⇩_aA⌋" by (simp add: sem_4a)
lemma CJ_4: "⌊❙¬❙O⟨❙⊥|A⟩⌋" by (simp add: sem_5a)

lemma CJ_5: "⌊(❙O⟨B|A⟩ ❙∧ ❙O⟨C|A⟩) ❙→ ❙O⟨B❙∧C|A⟩⌋" nitpick oops ― ‹ countermodel found ›
lemma CJ_5_minus: "⌊❙◇⇧^S⇧⁵(A ❙∧ B ❙∧ C) ❙∧ (❙O⟨B|A⟩ ❙∧ ❙O⟨C|A⟩) ❙→ ❙O⟨B❙∧C|A⟩⌋" by (simp add: sem_5c)

lemma CJ_6: "⌊❙O⟨B|A⟩ ❙→ ❙O⟨B|A❙∧B⟩⌋" by (smt (z3) C_2 C_4)
lemma CJ_7: "⌊A ❙↔ B⌋ ⟶ ⌊❙O⟨C|A⟩ ❙↔ ❙O⟨C|B⟩⌋" using sem_5ab sem_5e by blast (* Valid only using classical (not Kaplan's indexical) validity*)
lemma CJ_8: "⌊C ❙→ (A ❙↔ B)⌋ ⟶ ⌊❙O⟨A|C⟩ ❙↔ ❙O⟨B|C⟩⌋" using C_6 by simp (* Valid only using classical (not Kaplan's indexical) validity*)

lemma CJ_9a: "⌊❙◇⇩_p❙O⟨B|A⟩ ❙→ ❙□⇩_p❙O⟨B|A⟩⌋" by simp
lemma CJ_9p: "⌊❙◇⇩_a❙O⟨B|A⟩ ❙→ ❙□⇩_a❙O⟨B|A⟩⌋" by simp
lemma CJ_9_var_a: "⌊❙O⟨B|A⟩ ❙→ ❙□⇩_a❙O⟨B|A⟩⌋" by simp
lemma CJ_9_var_b: "⌊❙O⟨B|A⟩ ❙→ ❙□⇩_p❙O⟨B|A⟩⌋" by simp
lemma CJ_10: "⌊❙◇⇩_p(A ❙∧ B ❙∧ C) ❙∧ ❙O⟨C|B⟩ ❙→ ❙O⟨C|A❙∧B⟩⌋" by (smt (z3) C_4)

lemma CJ_11a: "⌊(❙O⇩_aA ❙∧ ❙O⇩_aB) ❙→ ❙O⇩_a(A ❙∧ B)⌋" nitpick oops ― ‹  countermodel found ›
lemma CJ_11a_var: "⌊❙◇⇩_a(A ❙∧ B) ❙∧ (❙O⇩_aA ❙∧ ❙O⇩_aB) ❙→ ❙O⇩_a(A ❙∧ B)⌋" using sem_5c by auto

lemma CJ_11p: "⌊(❙O⇩_iA ❙∧ ❙O⇩_iB) ❙→ ❙O⇩_i(A ❙∧ B)⌋" nitpick oops ― ‹  countermodel found ›
lemma CJ_11p_var: "⌊❙◇⇩_p(A ❙∧ B) ❙∧ (❙O⇩_iA ❙∧ ❙O⇩_iB) ❙→ ❙O⇩_i(A ❙∧ B)⌋" using sem_5c by auto

lemma CJ_12a: "⌊❙□⇩_aA ❙→ (❙¬❙O⇩_aA ❙∧ ❙¬❙O⇩_a(❙¬A))⌋" using sem_5ab by blast (*using C_2 by blast *)
lemma CJ_12p: "⌊❙□⇩_pA ❙→ (❙¬❙O⇩_iA ❙∧ ❙¬❙O⇩_i(❙¬A))⌋" using sem_5ab by blast (*using C_2 by blast*) 

lemma CJ_13a: "⌊❙□⇩_a(A ❙↔ B) ❙→ (❙O⇩_aA ❙↔ ❙O⇩_aB)⌋" using sem_5b by metis (*using C_6 by blast *)
lemma CJ_13p: "⌊❙□⇩_p(A ❙↔ B) ❙→ (❙O⇩_iA ❙↔ ❙O⇩_iB)⌋" using sem_5b by metis (*using C_6 by blast *)

lemma CJ_O_O: "⌊❙O⟨B|A⟩ ❙→ ❙O⟨A ❙→ B|❙⊤⟩⌋" using sem_5bd4 by presburger

text‹\noindent{An ideal obligation which is actually possible both to fulfill and to violate entails an actual obligation (\<^cite>‹"CJDDL"› p.319).}›
lemma CJ_Oi_Oa: "⌊(❙O⇩_iA ❙∧ ❙◇⇩_aA ❙∧ ❙◇⇩_a(❙¬A)) ❙→ ❙O⇩_aA⌋" using sem_5e sem_4a by blast

text‹\noindent{Bridge relations between conditional obligations and actual/ideal obligations:}›
lemma CJ_14a: "⌊❙O⟨B|A⟩ ❙∧ ❙□⇩_aA ❙∧ ❙◇⇩_aB ❙∧ ❙◇⇩_a❙¬B ❙→ ❙O⇩_aB⌋" using sem_5e by blast
lemma CJ_14p: "⌊❙O⟨B|A⟩ ❙∧ ❙□⇩_pA ❙∧ ❙◇⇩_pB ❙∧ ❙◇⇩_p❙¬B ❙→ ❙O⇩_iB⌋" using sem_5e by blast

lemma CJ_15a: "⌊(❙O⟨B|A⟩ ❙∧ ❙◇⇩_a(A ❙∧ B) ❙∧ ❙◇⇩_a(A ❙∧ ❙¬B)) ❙→  ❙O⇩_a(A ❙→ B)⌋" using CJ_O_O sem_5e by fastforce (*using CJ_O_O CJ_14a by blast*)
lemma CJ_15p: "⌊(❙O⟨B|A⟩ ❙∧ ❙◇⇩_p(A ❙∧ B) ❙∧ ❙◇⇩_p(A ❙∧ ❙¬B)) ❙→  ❙O⇩_i(A ❙→ B)⌋" using CJ_O_O sem_5e by fastforce (*using CJ_O_O CJ_14p by blast*)

(*<*)
end
(*>*)