# 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) in ℐ A ❙≼ 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