Theory ex_subminimal_logics

theory ex_subminimal_logics
  imports topo_negation_conditions topo_strict_implication
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section ‹Example application: Subintuitionistic and subminimal logics›

text‹\noindent{In this section we examine some special paracomplete logics. The idea is to illustrate an approach by
means of which we can obtain logics which are boldly paracomplete and (non-boldly) paraconsistent at the
same time, Johansson's 'minimal logic' @{cite JML} being the paradigmatic case we aim at modelling.}›

text‹\noindent{Drawing upon the literature on Johanson's minimal logic, we introduce an unconstrained propositional
constant Q, which we then employ to define a 'rigid' frontier operation @{text "ℱ'"}.}›
consts Q::"σ"
abbreviation "ℱ'  λX. Q" 
abbreviation "ℐ'  F ℱ'"
abbreviation "𝒞'  𝒞F ℱ'"
abbreviation "ℬ'  F ℱ'"

text‹\noindent{As defined, @{text "ℱ'"} (and its corresponding closure operation) satisfies several semantic conditions.}›
lemma "Fr_1 ℱ'  Fr_2 ℱ'  Fr_4 ℱ'" by (simp add: Fr_1_def Fr_2_def Fr_4_def conn)
lemma "Cl_1 𝒞'  Cl_2 𝒞'  Cl_4 𝒞'" using ADDI_def CF2 IDEMb_def Cl_fr_def PC4 unfolding conn by auto
text‹\noindent{However Fr-3 is not valid. In fact, adding it by hand would collapse into classical logic (making all sets clopen).}›
lemma "Fr_3 ℱ'" nitpick oops (*counterexample found*)
lemma "Cl_3 𝒞'" nitpick oops (*counterexample found*)
lemma "Fr_3 ℱ'  A. ℱ'(A)  "  by (simp add: NOR_def) 

text‹\noindent{In order to obtain a paracomplete logic not validating ECQ, we define negation as follows,}›
abbreviation neg_IC::σ" ("¬")  where  "¬A  𝒞'((A))"

text‹\noindent{and observe that some plausible semantic properties obtain:}›
lemma Q_def1: "A. Q  ¬A  ¬(¬A)" using Cl_fr_def IF2 dEXP_def conn by auto
lemma Q_def2: "Fr_1b ℱ  A. Q  ¬(A  ¬A)" by (smt Cl_fr_def IF2 dEXP_def MONO_def monI conn)
lemma neg_Idef: "A. ¬A (A)  Q" by (simp add: Cl_fr_def)
lemma neg_Cdef: "Fr_2 ℱ  A. ¬A  𝒞(A)  Q" using Cl_fr_def Fr_2_def Int_fr_def conn by auto

text‹\noindent{The negation so defined validates some properties corresponding to a (rather weak) paracomplete logic:}›
lemma "𝔉 ℱ  TND ¬" nitpick oops (*counterexample found: negation is paracomplete*)
lemma "𝔉 ℱ  TNDw ¬" nitpick oops
lemma "𝔉 ℱ  TNDm ¬" nitpick oops
lemma "𝔉 ℱ  ECQ ¬" nitpick oops (*counterexample found: negation is paraconsistent...*)
lemma ECQw: "ECQw ¬" using Cl_fr_def Disj_I ECQw_def unfolding conn by auto (*...but not 'boldly' paraconsistent*) 
lemma ECQm: "ECQm ¬" using Cl_fr_def Disj_I ECQm_def unfolding conn by auto 
lemma "𝔉 ℱ  LNC ¬" nitpick oops
lemma "𝔉 ℱ  DNI ¬" nitpick oops
lemma "𝔉 ℱ  DNE ¬"  nitpick oops
lemma CoPw: "Fr_1b ℱ  CoPw ¬" using Cl_fr_def MONO_def monI unfolding Defs conn by smt
lemma "𝔉 ℱ  CoP1 ¬" nitpick oops
lemma "𝔉 ℱ  CoP2 ¬" nitpick oops
lemma "𝔉 ℱ  CoP3 ¬" nitpick oops
lemma "𝔉 ℱ  XCoP ¬" nitpick oops
lemma "𝔉 ℱ  DM3 ¬" nitpick oops
lemma DM4: "Fr_1a ℱ  DM4 ¬" using ADDI_a_def Cl_fr_def DM4_def IC1b IF1b dual_def unfolding conn by smt
lemma Nor: "Fr_2 ℱ  Fr_3 ℱ  nNor ¬" using Cl_fr_def nNor_I nNor_def unfolding conn by auto
lemma "𝔉 ℱ  nDNor ¬" nitpick oops
lemma "𝔉 ℱ  lCoPw() ¬" nitpick oops
lemma "𝔉 ℱ  lCoP1() ¬" nitpick oops
lemma "𝔉 ℱ  lCoP2() ¬" nitpick oops
lemma "𝔉 ℱ  lCoP3() ¬" nitpick oops
lemma "𝔉 ℱ  DS1() ¬" nitpick oops
lemma "𝔉 ℱ  DS2() ¬" nitpick oops

text‹\noindent{Moreover, we cannot have both DNI and DNE without validating ECQ (thus losing paraconsistency).}›
lemma "DNI ¬  DNE ¬  ECQ ¬" using DNE_def ECQ_def Int_fr_def neg_Idef unfolding conn by (metis (no_types, lifting))
text‹\noindent{However, we can have all of De Morgan laws while keeping (non-bold) paraconsistency.}›
lemma "ECQ ¬  DM1 ¬  DM2 ¬  DM3 ¬  DM4 ¬  𝔉 ℱ" nitpick[satisfy,card w=3] oops (*(weakly paraconsistent) model found*)

text‹\noindent{Below we combine negation with strict implication and verify some interesting properties.
For instance, the following are not valid (and cannot become valid by adding semantic restrictions). }›
lemma "𝔉 ℱ  a b. (¬a  (a  b))  " nitpick oops (*counterexample found*)
lemma "𝔉 ℱ  a b. (¬a  (a  b))  " nitpick oops
lemma "𝔉 ℱ  a b. (a  ¬a  b)  "  nitpick oops
lemma "𝔉 ℱ  a b. (a  ¬a  b)  "  nitpick oops
lemma "𝔉 ℱ  a b. (a  (b  ¬b))  "  nitpick oops
lemma "𝔉 ℱ  a b. (a  (b  ¬b))  "  nitpick oops
lemma "𝔉 ℱ  a. (a  ¬a)  ¬a  " nitpick oops
lemma "𝔉 ℱ  a. (a  ¬a)  ¬a  " nitpick oops
lemma "𝔉 ℱ  a b. (a  ¬a)  b  " nitpick oops 
lemma "𝔉 ℱ  a b. (a  ¬a)  b  " nitpick oops 
lemma "𝔉 ℱ  a b. a  (b  ¬b)  " nitpick oops 
lemma "𝔉 ℱ  a b. a  (b  ¬b)  " nitpick oops 
lemma "𝔉 ℱ  a b. (a  b)  (¬a  ¬b)  " nitpick oops 
lemma "𝔉 ℱ  a b. (a  b)  (¬a  ¬b)  " nitpick oops
lemma "𝔉 ℱ  a b. (a  b)  (a  ¬b)  ¬a  " nitpick oops
lemma "𝔉 ℱ  a b. (a  b)  (a  ¬b)  ¬a  " nitpick oops
lemma "𝔉 ℱ  a. (¬a    )  " nitpick oops 
lemma "𝔉 ℱ  a. (¬a    )  " nitpick oops 
lemma "𝔉 ℱ  a. (¬a  ¬(¬))  " nitpick oops
lemma "𝔉 ℱ  a. (¬a  ¬(¬))  " nitpick oops
lemma "𝔉 ℱ  a. ¬(¬(¬a))  ¬a  " nitpick oops
lemma "𝔉 ℱ  a. ¬(¬(¬a))  ¬a  " nitpick oops

text‹\noindent{The (weak) local contraposition axiom is indeed valid under appropriate conditions.}›
lemma lCoPw: "Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ  Fr_4 ℱ  lCoPw() ¬" proof -
  assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr3: "Fr_3 ℱ" and fr4: "Fr_4 ℱ"
  { fix a b
    from fr2 have "¬b  ¬a  (𝒞 a  𝒞 b)  Q" using Cl_fr_def Fr_2_def Int_fr_def conn by auto
    moreover from fr1 fr2 fr3 have "ℐ(a  b)  𝒞 a  𝒞 b" using IC_imp by simp
    ultimately have "ℐ(a  b)  ¬b  ¬a" unfolding conn by simp   
    moreover from fr1 fr2 fr4 have "let A=(a  b); B=(¬b  ¬a) inA  B A B"
      using PF1 MONO_MULTa IF1a IF4 PI9 Int_9_def by smt
    ultimately have "ℐ(a  b) (¬b  ¬a)" by simp
  } hence "lCoPw() ¬" unfolding Defs conn by blast
  thus ?thesis by simp
qed
lemma lCoPw_strict: "𝔉 ℱ  a b. (a  b)  (¬b  ¬a)  " by (metis (no_types, lifting) DTw2 lCoPw lCoPw_def)

text‹\noindent{However, other (local) contraposition axioms are not valid.}›
lemma "𝔉 ℱ  lCoP1() ¬" nitpick oops (*counterexample found*)
lemma "𝔉 ℱ  lCoP2() ¬" nitpick oops
lemma "𝔉 ℱ  lCoP3() ¬" nitpick oops
text‹\noindent{And this time no variant of disjunctive syllogism is valid.}›
lemma "𝔉 ℱ  DS1() ¬" nitpick oops
lemma "𝔉 ℱ  DS2() ¬" nitpick oops
lemma "𝔉 ℱ  DS2() ¬" nitpick oops
lemma "𝔉 ℱ  DS4() ¬" nitpick oops

text‹\noindent{Interestingly, one of the local contraposition axioms (lCoP1) follows from DNI.}›
lemma DNI_lCoP1: "Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ  Fr_4 ℱ  DNI ¬  lCoP1() ¬" proof -
  assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr3: "Fr_3 ℱ" and fr4: "Fr_4 ℱ"
  { assume dni: "DNI ¬"
    { fix a b
      from fr1 fr2 fr3 fr4 have "lCoPw() ¬"  using lCoPw by simp
      hence 1: "a  ¬b  ¬(¬b)  ¬a" unfolding lCoPw_def by simp
      from fr1 have 2: "let A=b; B=¬(¬b); C=¬a in A  B (B  C) (A  C)" by (simp add: MONO_ant PF1 monI)
      from dni have dnib: "b  ¬(¬b)" unfolding DNI_def by simp
      from 1 2 dnib have "a  ¬b  b  ¬a" unfolding conn by meson
    } hence "lCoP1() ¬" unfolding Defs by blast
  } thus ?thesis by simp
qed
text‹\noindent{This entails some other interesting results.}›
lemma DNI_CoP1: "Fr_1b ℱ  DNI ¬  CoP1 ¬" using CoP1_def2 CoPw by blast
lemma CoP1_LNC: "CoP1 ¬  LNC ¬" using CoP1_def ECQm_def LNC_def  Cl_fr_def Disj_I ECQm_def unfolding conn by smt
lemma DNI_LNC: "Fr_1b ℱ  DNI ¬  LNC ¬" by (simp add: CoP1_LNC DNI_CoP1)

text‹\noindent{The following variants of modus tollens also obtain.}›
lemma MT: "Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ  a b. (a  b)  ¬b  ¬a" using Cl_fr_def Fr_2_def IC_imp Int_fr_def unfolding conn by metis
lemma MT': "Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ  a b. ((a  b)  ¬b)  ¬a  " by (simp add: DTw2 MT)

text‹\noindent{We now semantically characterize (an approximation of) Johansson's Minimal Logic along with some 
exemplary 'subminimal' logics (observing that many more are possible). We check some relevant properties.}›
abbreviation "JML  𝔉 ℱ  DNI ¬"
abbreviation "SML1  𝔉 ℱ" (*Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ*)
abbreviation "SML2  Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ"
abbreviation "SML3  Fr_1 ℱ"
abbreviation "SML4  Fr_1b ℱ"

text‹\noindent{TND:}›
lemma "JML  TND ¬" nitpick oops (*counterexample found*)
lemma "JML  TNDw ¬" nitpick oops
lemma "JML  TNDm ¬" nitpick oops

text‹\noindent{ECQ:}›
lemma "JML  ECQ ¬" nitpick oops
lemma "ECQw ¬" using Cl_fr_def Disj_I ECQw_def unfolding conn by auto  
lemma "ECQm ¬" using Cl_fr_def Disj_I ECQm_def unfolding conn by auto

text‹\noindent{LNC:}›
lemma "JML  LNC ¬" using DNI_LNC PF1 by blast
lemma "SML1  LNC ¬" nitpick oops

text‹\noindent{(r)DNI/DNE:}›
lemma "JML  DNI ¬" using CoP1_def2 by blast
lemma "SML1  rDNI ¬" nitpick oops
lemma "JML  rDNE ¬"  nitpick oops

text‹\noindent{CoP/MT:}›
lemma "SML4  CoPw ¬" unfolding Defs by (smt Cl_fr_def MONO_def monI conn)
lemma "JML  CoP1 ¬" using DNI_CoP1 PF1 by blast
lemma "SML1  MT1 ¬" nitpick oops
lemma "JML  MT2 ¬" nitpick oops
lemma "JML  MT3 ¬" nitpick oops

text‹\noindent{XCoP:}›
lemma "JML  XCoP ¬" nitpick oops

text‹\noindent{DM3/4:}›
lemma "JML  DM3 ¬" nitpick oops
lemma "SML3  DM4 ¬" by (simp add: DM4 PF1)
lemma "SML4  DM4 ¬" nitpick oops

text‹\noindent{nNor/nDNor:}›
lemma "SML2  nNor ¬" using Cl_fr_def nNor_I nNor_def unfolding conn by auto
lemma "SML3  nNor ¬" nitpick oops
lemma "JML  nDNor ¬" nitpick oops

text‹\noindent{lCoP classical:}›
lemma "JML  lCoPw() ¬" nitpick oops
lemma "JML  lCoP1() ¬" nitpick oops
lemma "JML  lCoP2() ¬" nitpick oops
lemma "JML  lCoP3() ¬" nitpick oops

text‹\noindent{DS classical:}›
lemma "JML  DS1() ¬" nitpick oops
lemma "JML  DS2() ¬" nitpick oops

text‹\noindent{lCoP strict:}›
lemma "SML1  lCoPw() ¬" using lCoPw by blast
lemma "SML2  lCoPw() ¬" nitpick oops
lemma "JML  lCoP1() ¬" using CoP1_def2 DNI_lCoP1 by blast
lemma "SML1  lCoP1() ¬" nitpick oops
lemma "JML  lCoP2() ¬" nitpick oops
lemma "JML  lCoP3() ¬" nitpick oops

text‹\noindent{lMT strict:}›
lemma "SML2  lMT0() ¬" unfolding Defs using MT by auto
lemma "SML3  lMT0() ¬"  (*nitpick*) oops (*no countermodel found*)
lemma "SML4  lMT0() ¬"  nitpick oops
lemma "JML  lMT1() ¬"  by (smt DNI_lCoP1 DT1 lCoP1_def lMT1_def)
lemma "SML1  lMT1() ¬" nitpick oops
lemma "JML  lMT2() ¬" nitpick oops
lemma "JML  lMT3() ¬" nitpick oops

text‹\noindent{DS strict:}›
lemma "JML  DS1() ¬" nitpick oops
lemma "JML  DS2() ¬" nitpick oops
lemma "JML  DS3() ¬" nitpick oops
lemma "JML  DS4() ¬" nitpick oops

end