Theory DDLcube

section  ‹Shallow Embedding of \AA qvist's system {\bf E}›

  text ‹This is Aqvist's system E from the 2019 IfColog paper \cite{J45}.›

subsection  ‹System {\bf E}›

theory DDLcube 
  imports Main  (*** Benzmueller/Parent 2024 ***)

begin  
nitpick_params [user_axioms,show_all,format=2]  ―‹Settings for model finder Nitpick›

typedecl i  ―‹Possible worlds›
type_synonym σ = "(i⇒bool)"
type_synonym α = "i⇒σ"  ―‹Type of betterness relation between worlds›
type_synonym τ = "σ⇒σ"

consts aw::i  ―‹Actual world›
abbreviation etrue  :: "σ" ("❙⊤") where "❙⊤ ≡ λw. True" 
abbreviation efalse :: "σ" ("❙⊥")  where "❙⊥ ≡ λw. False"   
abbreviation enot :: "σ⇒σ" ("❙¬_"[52]53)  where "❙¬φ ≡ λw. ¬φ(w)" 
abbreviation eand :: "σ⇒σ⇒σ" (infixr"❙∧"51) where "φ❙∧ψ ≡ λw. φ(w)∧ψ(w)"   
abbreviation eor  :: "σ⇒σ⇒σ" (infixr"❙∨"50) where "φ❙∨ψ ≡ λw. φ(w)∨ψ(w)"   
abbreviation eimpf :: "σ⇒σ⇒σ" (infixr"❙→"49) where "φ❙→ψ ≡ λw. φ(w)⟶ψ(w)"  
abbreviation eimpb :: "σ⇒σ⇒σ" (infixr"❙←"49) where "φ❙←ψ ≡ λw. ψ(w)⟶φ(w)"  
abbreviation eequ :: "σ⇒σ⇒σ" (infixr"❙↔"48) where "φ❙↔ψ ≡ λw. φ(w)⟷ψ(w)" 

abbreviation ebox :: "σ⇒σ" ("□") where "□φ ≡ λw. ∀v. φ(v)"  
abbreviation ddediomond  :: "σ⇒σ" ("◇") where "◇φ ≡ λw. ∃v. φ(v)"

abbreviation evalid :: "σ⇒bool" ("⌊_⌋"[8]109)  ―‹Global validity›
  where "⌊p⌋ ≡ ∀w. p w"
abbreviation ecjactual :: "σ⇒bool" ("⌊_⌋⇩l"[7]105)  ―‹Local validity — in world aw›
  where "⌊p⌋⇩l ≡ p(aw)"

consts r :: "α" (infixr "❙r" 70)  ―‹Betterness relation›

abbreviation esubset :: "σ⇒σ⇒bool" (infix "❙⊆" 53)
  where "φ ❙⊆ ψ ≡ ∀x. φ x ⟶ ψ x"

  text ‹We introduce the opt and max rules. These express two candidate truth-conditions for
conditional obligation and permission.›

abbreviation eopt  :: "σ⇒σ" ("opt<_>")  ―‹opt rule›
  where "opt<φ> ≡ (λv. ( (φ)(v) ∧ (∀x. ((φ)(x) ⟶ v ❙r x) )) )" 
abbreviation econdopt :: "σ⇒σ⇒σ" ("⊙<_|_>")
  where "⊙<ψ|φ> ≡  λw. opt<φ> ❙⊆ ψ"
abbreviation eperm :: "σ⇒σ⇒σ" ("𝒫<_|_>") 
  where "𝒫<ψ|φ> ≡ ❙¬⊙<❙¬ψ|φ>" ―‹permission is the dual of obligation›

abbreviation emax  :: "σ⇒σ" ("max<_>")  ―‹max rule›
  where "max<φ> ≡ (λv. ( (φ)(v) ∧ (∀x. ((φ)(x) ⟶ (x ❙r v ⟶  v ❙r x)) )) )" 
abbreviation econd  :: "σ⇒σ⇒σ" ("○<_|_>")
  where "○<ψ|φ> ≡  λw. max<φ> ❙⊆ ψ"
abbreviation euncobl :: "σ⇒σ" ("❙○<_>")   
  where "❙○<φ> ≡ ○<φ|❙⊤>" 
abbreviation ddeperm :: "σ⇒σ⇒σ" ("P<_|_>") 
  where "P<ψ|φ> ≡❙¬○<❙¬ψ|φ>"

  text ‹A first consistency check is performed.›

lemma True 
  nitpick [expect=genuine,satisfy] ―‹model found›
  oops

  text ‹We show that the max-rule and opt-rule do not coincide.›

lemma "⊙<ψ|φ> ≡ ○<ψ|φ>" 
  nitpick [expect=genuine,card i=1] ―‹counterexample found›
  oops

  text ‹David Lewis's truth conditions for the deontic modalities are introduced.›

abbreviation lewcond :: "σ⇒σ⇒σ"  ("∘<_|_>")
  where "∘<ψ|φ> ≡ λv. (¬(∃x. (φ)(x))∨  
        (∃x. ((φ)(x)∧(ψ)(x) ∧ (∀y. ((y ❙r x) ⟶ (φ)(y)⟶(ψ)(y))))))"
abbreviation lewperm :: "σ⇒σ⇒σ" ("∫<_|_>") 
  where "∫<ψ|φ> ≡❙¬∘<❙¬ψ|φ>"

  text ‹Kratzer's truth conditions for the deontic modalities are introduced.›

abbreviation kratcond :: "σ⇒σ⇒σ"  ("⊖<_|_>")
  where "⊖<ψ|φ> ≡ λv. ((∀x. ((φ)(x) ⟶ 
     (∃y. ((φ)(y)∧(y ❙r x) ∧ ((∀z. ((z ❙r y) ⟶ (φ)(z) ⟶ (ψ)(z)))))))))"
abbreviation kratperm :: "σ⇒σ⇒σ" ("×<_|_>") 
  where "×<ψ|φ> ≡❙¬⊖<❙¬ψ|φ>"


subsection ‹Properties›

  text ‹Extensions of {\bf E} are obtained by putting suitable constraints on the betterness relation.›

  text ‹These are the standard properties of the betterness relation.›

abbreviation "reflexivity  ≡ (∀x. x ❙r x)"
abbreviation "transitivity ≡ (∀x y z. (x ❙r y ∧ y ❙r z) ⟶ x ❙r z)"
abbreviation "totality ≡ (∀x y. (x ❙r y ∨ y ❙r x))"

  text ‹4 versions of Lewis's limit assumption can be distinguished.›

abbreviation "mlimitedness ≡ (∀φ. (∃x. (φ)x) ⟶ (∃x. max<φ>x))"

abbreviation "msmoothness ≡
   (∀φ x. ((φ)x ⟶ (max<φ>x ∨ (∃y. (y ❙r x ∧ ¬(x ❙r y) ∧ max<φ>y)))))"

abbreviation "olimitedness ≡ (∀φ. (∃x. (φ)x) ⟶ (∃x. opt<φ>x))"

abbreviation "osmoothness ≡
   (∀φ x. ((φ)x ⟶ (opt<φ>x ∨ (∃y. (y ❙r x ∧ ¬(x ❙r y) ∧ opt<φ>y)))))"

  text ‹Weaker forms of transitivity can be defined. They require the notion of
transitive closure.›

definition transitive :: "α⇒bool"
  where "transitive Rel ≡ ∀x y z. Rel x y ∧  Rel y z ⟶ Rel x z"

definition sub_rel :: "α⇒α⇒bool" 
  where "sub_rel Rel1 Rel2 ≡ ∀u v. Rel1 u v ⟶ Rel2 u v"

definition assfactor::"α⇒α"
  where "assfactor Rel ≡ λu v. Rel u v ∧ ¬Rel v u "

  text ‹In HOL the transitive closure of a relation can be defined in a single line - Here 
we apply the construction to the betterness relation and its strict variant.›

definition tcr  
  where "tcr ≡ λx y. ∀Q. transitive Q ⟶ (sub_rel r Q ⟶ Q x y)"

definition tcr_strict
  where "tcr_strict ≡ λx y. ∀Q. transitive Q 
                               ⟶ (sub_rel (λu v. u ❙r v ∧ ¬v ❙r u) Q ⟶ Q x y)"

  text ‹Quasi-transitivity requires the strict betterness relation is transitive.›

abbreviation Quasitransit 
  where "Quasitransit  ≡ ∀x y z. (assfactor r x y ∧  
                    assfactor r y z) ⟶ assfactor r x z"

  text ‹Suzumura consistency requires that cycles with at least  one  non-strict betterness link are ruled out.›

abbreviation Suzumura  
  where "Suzumura ≡ ∀x y. tcr x y ⟶ (y ❙r x ⟶ x ❙r y)"

theorem T1: "Suzumura ≡ ∀x y. tcr x y ⟶ ¬ (y ❙r x ∧ ¬ (x ❙r y))" by simp

  text ‹Acyclicity requires that cycles where all the links are strict are ruled out.›

abbreviation loopfree
  where "loopfree ≡ ∀x y. tcr_strict x y ⟶ (y ❙r x ⟶ x ❙r y)"

  text ‹Interval order is the combination of reflexivity and Ferrers.›
 
abbreviation Ferrers
  where "Ferrers ≡ (∀x y z u. (x ❙r u ∧ y ❙r z) ⟶ (x ❙r z ∨ y ❙r u))"

theorem T2:
  assumes Ferrers and reflexivity  ―‹fact overlooked in the literature›
  shows totality
  ―‹sledgehammer›
  by (simp add: assms(1) assms(2)) 

  text ‹We study the relationships between these candidate weakenings of transitivity.›

theorem T3: 
  assumes transitivity 
  shows "Suzumura"
  ―‹sledgehammer›
  by (metis assms sub_rel_def tcr_def transitive_def)
 
theorem T4:
  assumes transitivity 
  shows Quasitransit
  ―‹sledgehammer›
  by (metis assfactor_def assms) 

theorem T5:
  assumes Suzumura
  shows loopfree
  ―‹sledgehammer›
  by (metis (no_types, lifting) assms sub_rel_def tcr_def tcr_strict_def)

theorem T6: 
  assumes Quasitransit 
  shows loopfree
  ―‹sledgehammer›
  by (smt (verit, best) assfactor_def assms sub_rel_def tcr_strict_def transitive_def)

theorem T7: 
  assumes reflexivity and Ferrers 
  shows Quasitransit
  ―‹sledgehammer› 
  by (metis assfactor_def assms) 

section  ‹Meta-Logical Study›

subsection ‹Correspondence - Max rule›

  text ‹The inference rules of {\bf E} preserve validity in all models.›

lemma MP: "⟦⌊φ⌋; ⌊φ ❙→ ψ⌋⟧ ⟹ ⌊ψ⌋" 
  ―‹sledgehammer› 
  by simp

lemma NEC: "⌊φ⌋ ⟹ ⌊□φ⌋" 
    ―‹sledgehammer› 
  by simp

  text ‹@{term "□"} is an S5 modality›

lemma C_1_refl: "⌊□φ ❙→ φ⌋" 
  ―‹sledgehammer› 
  by simp

lemma C_1_trans: "⌊□φ ❙→ (□(□φ))⌋" 
  ―‹sledgehammer› 
  by simp

lemma C_1_sym: "⌊φ ❙→ (□(◇φ))⌋"  
  ―‹sledgehammer› 
  by simp

  text ‹All the axioms of {\bf E} hold - they do not correspond to a property of the betterness relation.›

lemma Abs: "⌊○<ψ|φ> ❙→ □○<ψ|φ>⌋" 
  ―‹sledgehammer›
  by blast 

lemma Nec: "⌊□ψ ❙→ ○<ψ|φ>⌋" 
  ―‹sledgehammer›
  by blast 

lemma Ext: "⌊□(φ⇩1❙↔φ⇩2) ❙→ (○<ψ|φ⇩1> ❙↔ ○<ψ|φ⇩2>)⌋"  
  ―‹sledgehammer›
  by simp

lemma Id: "⌊○<φ|φ>⌋"  
  ―‹sledgehammer›
  by blast 

lemma Sh: "⌊○<ψ|φ⇩1❙∧φ⇩2> ❙→ ○<(φ⇩2❙→ψ)|φ⇩1>⌋" 
  ―‹sledgehammer›
  by blast 

lemma COK:"⌊○<(ψ⇩1❙→ψ⇩2)|φ> ❙→ (○<ψ⇩1|φ> ❙→ ○<ψ⇩2|φ>)⌋" 
  ―‹sledgehammer›
  by blast

  text ‹The axioms of the stronger systems do not hold in general.›

lemma "⌊◇φ ❙→ (○<ψ|φ> ❙→ P<ψ|φ>)⌋" 
  nitpick [expect=genuine,card i=3]  ―‹counterexample found›
  oops 

lemma "⌊(○<ψ|φ> ❙∧ ○<χ|φ>) ❙→ ○<χ|φ❙∧ψ>⌋"
  nitpick [expect=genuine,card i=3]  ―‹counterexample found›
  oops 

lemma "⌊○<χ|(φ❙∨ψ)> ❙→ ((○<χ|φ>) ❙∨ (○<χ|ψ>))⌋"
  nitpick [expect=genuine,card i=3]  ―‹counterexample found›
  oops 

  text ‹Now we identify a number of correspondences under the max rule. Only the direction property => axiom is verified.›

  text ‹Max-limitedness corresponds to D*, the distinctive axiom of {\bf F}. The first implies the second,
but not the other around.›

theorem T8: 
  assumes mlimitedness
  shows  "D*": "⌊◇φ ❙→ ○<ψ|φ> ❙→ P<ψ|φ>⌋"  
  ―‹sledgehammer›
  by (metis assms)

lemma 
  assumes "D*": "⌊◇φ ❙→ ❙¬(○<ψ|φ> ❙∧ ○<❙¬ψ|φ>)⌋"
  shows mlimitedness 
  nitpick [expect=genuine,card i=3]  ―‹counterexample found›
  oops

  text ‹Smoothness implies cautious monotony, the distinctive axiom of {\bf F}+(CM), but not the other
way around.›

theorem T9: 
  assumes msmoothness    
  shows CM: "⌊(○<ψ|φ> ❙∧ ○<χ|φ>) ❙→ ○<χ|φ❙∧ψ>⌋" 
  ―‹sledgehammer›
  using assms by force 

lemma 
  assumes CM: "⌊(○<ψ|φ> ❙∧ ○<χ|φ>) ❙→ ○<χ|φ❙∧ψ>⌋"
  shows  msmoothness
  nitpick [expect=genuine,card i=3]  ―‹counterexample found›
  oops  

  text ‹Interval order corresponds to disjunctive rationality, the distinctive axiom of {\bf F}+(DR), but not the
other way around.›

lemma 
  assumes reflexivity
  shows  DR: "⌊○<χ|φ❙∨ψ> ❙→ (○<χ|φ> ❙∨ ○<χ|ψ>)⌋" 
  nitpick [expect=genuine,card i=3]  ―‹counterexample found›
  oops 

theorem T10: 
  assumes reflexivity and Ferrers
  shows  DR: "⌊○<χ|(φ❙∨ψ)> ❙→ (○<χ|φ> ❙∨ ○<χ|ψ>)⌋" 
  ―‹sledgehammer›
  by (metis assms(1) assms(2))
  
lemma 
  assumes DR: "⌊○<χ|φ❙∨ψ> ❙→ (○<χ|φ> ❙∨ ○<χ|ψ>)⌋" 
  shows reflexivity 
  nitpick [expect=genuine,card i=1]  ―‹counterexample found› 
  oops 

lemma 
  assumes DR: "⌊○<χ|φ❙∨ψ>❙→(○<χ|φ> ❙∨ ○<χ|ψ>)⌋" 
  shows Ferrers  
  nitpick [expect=genuine,card i=2]  ―‹counterexample found›
  oops 

  text ‹Transitivity and totality jointly correspond to the Spohn axiom (Sp), the distinctive axiom of system  {\bf G}, but not vice-versa. They also jointly correspond to a
 principle of transitivity for the betterness relation on formulas, but the converse fails.›

lemma 
  assumes transitivity
  shows  Sp: "⌊( P<ψ|φ> ❙∧ ○<(ψ❙→χ)|φ>) ❙→ ○<χ|(φ❙∧ψ)>⌋" 
  nitpick [expect=genuine,card i=3] ―‹counterexample found› 
  oops

lemma 
  assumes totality
  shows  Sp: "⌊( P<ψ|φ> ❙∧ ○<(ψ❙→χ)|φ>) ❙→ ○<χ|(φ❙∧ψ)>⌋" 
  nitpick [expect=genuine,card i=3] ―‹counterexample found›
  oops

theorem T11: 
  assumes transitivity and totality
  shows  Sp: "⌊( P<ψ|φ> ❙∧ ○<(ψ❙→χ)|φ>) ❙→ ○<χ|(φ❙∧ψ)>⌋" 
  ―‹sledgehammer›
  by (metis assms)

theorem T12: 
  assumes transitivity and totality
  shows  transit: "⌊( P<φ|φ❙∨ψ> ❙∧ P<ψ|ψ❙∨χ>) ❙→ P<φ|(φ❙∨χ)>⌋" 
  ―‹sledgehammer›
  by (metis assms(1) assms(2))
                                                          
lemma 
  assumes  Sp: "⌊( P<ψ|φ> ❙∧ ○<(ψ❙→χ)|φ>) ❙→ ○<χ|(φ❙∧ψ)>⌋" 
  shows totality   
  nitpick [expect=genuine,card i=1] ―‹counterexample found› 
  oops

lemma 
  assumes  Sp: "⌊( P<ψ|φ> ❙∧ ○<(ψ❙→χ)|φ>) ❙→ ○<χ|(φ❙∧ψ)>⌋" 
  shows transitivity 
  nitpick [expect=genuine,card i=2] ―‹counterexample found› 
  oops 

subsection ‹Correspondence - Opt Rule›

  text ‹Opt-limitedness corresponds to D, but not vice-versa.›

theorem T13: 
  assumes olimitedness   
  shows  D: "⌊◇φ ❙→ ⊙<ψ|φ> ❙→ 𝒫<ψ|φ>⌋"   
  ―‹sledgehammer› 
  by (simp add: assms) 

lemma 
  assumes D: "⌊◇φ ❙→ ⊙<ψ|φ> ❙→ 𝒫<ψ|φ>⌋"         
  shows olimitedness   
  nitpick [expect=genuine,card i=1] ―‹counterexample found›  
  oops 

  text ‹Smoothness implies cautious monotony, but not vice-versa.›

theorem T14: 
  assumes osmoothness   
  shows CM': "⌊( ⊙<ψ|φ> ❙∧ ⊙<χ|φ> ) ❙→ ⊙<χ|φ❙∧ψ>⌋"   
  ―‹sledgehammer› 
  using assms by force 

lemma 
  assumes CM: "⌊( ⊙<ψ|φ> ❙∧ ⊙<χ|φ> ) ❙→ ⊙<χ|φ❙∧ψ>⌋" 
  shows  osmoothness 
  nitpick [expect=genuine,card i=1] ―‹counterexample found›
  oops
 
  text ‹Transitivity (on worlds) implies Sp and transitivity (on formulas), but not vice-versa.›

theorem T15: 
  assumes transitivity   
  shows  Sp': "⌊( 𝒫<ψ|φ> ❙∧ ⊙<(ψ❙→χ)|φ>) ❙→ ⊙<χ|(φ❙∧ψ)>⌋"   
  ―‹sledgehammer› 
  by (metis assms) 

theorem T16: 
  assumes transitivity    
  shows  Trans': "⌊( 𝒫<φ|φ❙∨ψ> ❙∧ 𝒫<ψ|ψ❙∨ξ> )❙→ 𝒫<φ|φ❙∨ξ>⌋"   
  ―‹sledgehammer› 
  by (metis assms) 

lemma 
  assumes Sp: "⌊( 𝒫<ψ|φ> ❙∧ ⊙<(ψ❙→χ)|φ> ) ❙→ ⊙<χ|(φ❙∧ψ)>⌋"
  assumes Trans: "⌊( 𝒫<φ|φ❙∨ψ> ❙∧ 𝒫<ψ|ψ❙∨ξ> ) ❙→ 𝒫<φ|φ❙∨ξ>⌋"
  shows transitivity    
  nitpick [expect=genuine,card i=2] ―‹counterexample found›
  oops 

  text ‹Interval order implies disjunctive rationality, but not vice-versa.›

lemma 
  assumes reflexivity
  shows  DR': "⌊⊙<χ|φ❙∨ψ> ❙→ (⊙<χ|φ> ❙∨ ⊙<χ|ψ>)⌋"   
  nitpick [expect=genuine,card i=3] ―‹counterexample found›   
  oops 

theorem T17: 
  assumes reflexivity and Ferrers
  shows  DR': "⌊⊙<χ|φ❙∨ψ> ❙→ (⊙<χ|φ> ❙∨ ⊙<χ|ψ>)⌋"   
  ―‹sledgehammer› 
  by (metis assms(2))
 
lemma 
  assumes DR: "⌊⊙<χ|φ❙∨ψ> ❙→ (⊙<χ|φ> ❙∨ ⊙<χ|ψ>)⌋" 
  shows reflexivity   
  nitpick [expect=genuine,card i=1] ―‹counterexample found›  
  oops 

lemma 
  assumes DR: "⌊⊙<χ|φ❙∨ψ> ❙→ (⊙<χ|φ> ❙∨ ⊙<χ|ψ>)⌋" 
  shows Ferrers  
  nitpick [expect=genuine,card i=2] ―‹counterexample found›
  oops 

subsection ‹Correspondence - Lewis' rule›

  text ‹We have deontic explosion under the max rule.›

theorem DEX: "⌊(◇φ ❙∧ ○<ψ|φ> ❙∧ ○<❙¬ψ|φ>) ❙→ ○<χ|φ>⌋" 
  ―‹sledgehammer› 
  by blast  

  text ‹But no deontic explosion under Lewis' rule.›

lemma DEX: "⌊(◇φ ❙∧ ∘<ψ|φ> ❙∧ ∘<❙¬ψ|φ>) ❙→ ∘<χ|φ>⌋"
  nitpick [expect=genuine,card i=2] ―‹counterexample found› 
  oops

  text ‹The three rules are equivalent when the betterness relation  meets all the standard properties.›

theorem T18:
  assumes mlimitedness and transitivity and totality
  shows "⌊∘<ψ|φ>❙↔⊙<ψ|φ>⌋"   
  ―‹sledgehammer›
  by (smt (z3) assms)

theorem T19: 
  assumes mlimitedness and transitivity and totality
  shows "⌊∘<ψ|φ>❙↔○<ψ|φ>⌋" 
  ―‹sledgehammer›
  by (smt (z3) assms) 


  text ‹These are the axioms of {\bf E} that do not call for a property.›

theorem Abs': "⌊∘<ψ|φ> ❙→ □∘<ψ|φ>⌋"   
  ―‹sledgehammer› 
  by auto

theorem Nec': "⌊□ψ ❙→ ∘<ψ|φ>⌋"  
  ―‹sledgehammer›
  by auto

theorem Ext': "⌊□(φ⇩1❙↔φ⇩2) ❙→ (∘<ψ|φ⇩1> ❙↔ ∘<ψ|φ⇩2>)⌋"  
  ―‹sledgehammer› 
  by auto

theorem Id': "⌊∘<φ|φ>⌋" 
  ―‹sledgehammer› 
  by auto

theorem Sh': "⌊∘<ψ|φ⇩1❙∧φ⇩2> ❙→ ∘<(φ⇩2❙→ψ)|φ⇩1>⌋" 
  ―‹sledgehammer› 
  by auto

  text ‹One axiom of {\bf E}, and the distinctive axioms of its extensions are invalidated in the absence of 
a property of the betterness relation.›

lemma D: "⌊◇φ ❙→ (∘<ψ|φ> ❙→ ∫<ψ|φ>)⌋"
  nitpick [expect=genuine,card i=2] ―‹counterexample found› 
  oops

lemma Sp: "⌊( ∫<ψ|φ> ❙∧ ∘<(ψ❙→χ)|φ>) ❙→ ∘<χ|(φ❙∧ψ)>⌋" 
  nitpick [expect=genuine,card i=3] ―‹counterexample found› 
  oops 

lemma COK:"⌊∘<(ψ⇩1❙→ψ⇩2)|φ> ❙→ (∘<ψ⇩1|φ> ❙→ ∘<ψ⇩2|φ>)⌋" 
  nitpick [expect=genuine,card i=2] ―‹counterexample found› 
  oops 

lemma CM: "⌊(∘<ψ|φ>❙∧∘<χ|φ>)❙→ ∘<χ|φ❙∧ψ>⌋" 
  nitpick [expect=genuine,card i=2] ―‹counterexample found› 
  oops 

  text ‹Totality implies the distinctive axiom of {\bf F}, but not vice-versa.›

theorem T20:
  assumes totality
  shows "⌊◇φ ❙→ (∘<ψ|φ> ❙→ ∫<ψ|φ>)⌋" 
  ―‹sledgehammer› 
  using assms by blast

lemma  
  assumes  "⌊◇φ ❙→ (∘<ψ|φ> ❙→ ∫<ψ|φ>)⌋" 
  shows totality
  nitpick [expect=genuine,card i=3] ―‹counterexample found› 
  oops 

  text ‹Transitivity implies the distinctive axioms of {\bf G}, but not vice-versa.›

theorem T21:
  assumes transitivity
  shows Sp'': "⌊(∫<ψ|φ> ❙∧ ∘<(ψ❙→χ)|φ>) ❙→ ∘<χ|(φ❙∧ψ)>⌋"   
 ―‹sledgehammer›
  using assms by blast 

theorem T22:
  assumes transitivity
  shows  Tr'': "⌊(∫<φ|φ❙∨ψ>❙∧∫<ψ|ψ❙∨χ>)❙→ ∫<φ|φ❙∨χ>⌋" 
  ―‹sledgehammer›
  using assms by blast

lemma
  assumes Sp'': "⌊( ∫<ψ|φ> ❙∧ ∘<(ψ❙→χ)|φ>) ❙→ ∘<χ|(φ❙∧ψ)>⌋"  
  shows transitivity
  nitpick  ―‹counterexample found› 
  oops

lemma
  assumes  Tr'': "⌊(∫<φ|φ❙∨ψ>❙∧∫<ψ|ψ❙∨χ>)❙→ ∫<φ|φ❙∨χ>⌋" 
  shows transitivity
  nitpick  ―‹counterexample found› 
  oops

lemma
  assumes transitivity
  shows COK:"⌊∘<(ψ⇩1❙→ψ⇩2)|φ> ❙→ (∘<ψ⇩1|φ> ❙→ ∘<ψ⇩2|φ>)⌋" 
  nitpick [expect=genuine,card i=2] ―‹counterexample found› 
  oops  

lemma 
  assumes totality
  shows COK:"⌊∘<(ψ⇩1❙→ψ⇩2)|φ> ❙→ (∘<ψ⇩1|φ> ❙→ ∘<ψ⇩2|φ>)⌋" 
  nitpick [expect=genuine,card i=3] ―‹counterexample found› 
  oops 

  text ‹Transitivity and totality imply an axiom of {\bf E} and the distinctive axiom of {\bf F}+CM,
but not vice-versa.›

theorem T23:
  assumes transitivity and totality
  shows COK':"⌊∘<(ψ⇩1❙→ψ⇩2)|φ> ❙→ (∘<ψ⇩1|φ> ❙→ ∘<ψ⇩2|φ>)⌋" 
  ―‹sledgehammer› 
  by (smt (verit, ccfv_SIG) assms(1) assms(2)) 

lemma
  assumes COK':"⌊∘<(ψ⇩1❙→ψ⇩2)|φ> ❙→ (∘<ψ⇩1|φ> ❙→ ∘<ψ⇩2|φ>)⌋" 
  shows transitivity and totality
  nitpick [expect=genuine,card i=3] ―‹counterexample found› 
  oops 

theorem T24:
  assumes transitivity and totality
  shows CM'': "⌊(∘<ψ|φ>❙∧∘<χ|φ>)❙→ ∘<χ|φ❙∧ψ>⌋" 
  ―‹sledgehammer› 
  by (metis assms)

lemma
  assumes  CM'': "⌊(∘<ψ|φ>❙∧∘<χ|φ>)❙→ ∘<χ|φ❙∧ψ>⌋" 
  shows transitivity and totality
  nitpick [expect=genuine,card i=3] ―‹counterexample found› 
  oops 

  text ‹Under the opt rule transitivity alone imply Sp and Trans, but not vice-versa.›

theorem T25:
  assumes transitivity 
  shows "⌊(𝒫<ψ|φ> ❙∧ ⊙<(ψ❙→χ)|φ>) ❙→ ⊙<χ|(φ❙∧ψ)>⌋"   
  ―‹sledgehammer› 
  by (metis assms) 

lemma 
  assumes "transitivity"    
  shows  "⌊(𝒫<φ|φ❙∨ψ> ❙∧ 𝒫<ξ|ψ❙∨ξ>)❙→𝒫<ξ|φ❙∨ξ>⌋"   
  nitpick [expect=genuine,card i=2]  ―‹counterexample found› 
  oops 

lemma 
  assumes Sp: "⌊( 𝒫<ψ|φ> ❙∧ ⊙<(ψ❙→χ)|φ>) ❙→ ⊙<χ|(φ❙∧ψ)>⌋"
          and  Trans: "⌊(𝒫<φ|φ❙∨ψ> ❙∧ 𝒫<ξ|ψ❙∨ξ>)❙→𝒫<ξ|φ❙∨ξ>⌋"
  shows transitivity    
  nitpick [expect=genuine,card i=2]  ―‹counterexample found› 
  oops 

end