Theory logics_negation
theory logics_negation
imports logics_consequence conditions_relativized
begin
subsection ‹Properties of negation(-like) operators›
text‹To avoid visual clutter we introduce convenient notation for type for properties of operators.›
type_synonym 'w Ω = "('w σ ⇒ 'w σ) ⇒ bool"
named_theorems neg
subsubsection ‹Principles of excluded middle, contradiction and explosion›
text‹TND: tertium non datur, aka. law of excluded middle (resp. strong, weak, minimal).›
abbreviation pTND (‹TND⇧_ _›) where "TND⇧a η ≡ [⊢ a ❙∨ η a]"
abbreviation pTNDw (‹TNDw⇧_ _›) where "TNDw⇧a η ≡ ∀b. [η b ⊢ a, η a]"
abbreviation pTNDm (‹TNDm⇧_ _›) where "TNDm⇧a η ≡ [η ❙⊥ ⊢ a, η a]"
definition TND ::"'w Ω" where "TND η ≡ ∀φ. TND⇧φ η"
definition TNDw::"'w Ω" where "TNDw η ≡ ∀φ. TNDw⇧φ η"
definition TNDm::"'w Ω" where "TNDm η ≡ ∀φ. TNDm⇧φ η"
declare TND_def[neg] TNDw_def[neg] TNDm_def[neg]
text‹Explore some (non)entailment relations.›
lemma "TND η ⟹ TNDw η" unfolding neg conn order by simp
lemma "TNDw η ⟹ TND η" nitpick oops
lemma "TNDw η ⟹ TNDm η" unfolding neg by simp
lemma "TNDm η ⟹ TNDw η" nitpick oops
text‹ECQ: ex contradictione (sequitur) quodlibet (variants: strong, weak, minimal).›
abbreviation pECQ (‹ECQ⇧_ _›) where "ECQ⇧a η ≡ [a, η a ⊢ ❙⊥]"
abbreviation pECQw (‹ECQw⇧_ _›) where "ECQw⇧a η ≡ ∀b. [a, η a ⊢ η b]"
abbreviation pECQm (‹ECQm⇧_ _›) where "ECQm⇧a η ≡ [a, η a ⊢ η ❙⊤]"
definition ECQ ::"'w Ω" where "ECQ η ≡ ∀a. ECQ⇧a η"
definition ECQw::"'w Ω" where "ECQw η ≡ ∀a. ECQw⇧a η"
definition ECQm::"'w Ω" where "ECQm η ≡ ∀a. ECQm⇧a η"
declare ECQ_def[neg] ECQw_def[neg] ECQm_def[neg]
text‹Explore some (non)entailment relations.›
lemma "ECQ η ⟹ ECQw η" unfolding neg conn order by blast
lemma "ECQw η ⟹ ECQ η" nitpick oops
lemma "ECQw η ⟹ ECQm η" unfolding neg by simp
lemma "ECQm η ⟹ ECQw η" nitpick oops
text‹LNC: law of non-contradiction.›
abbreviation pLNC (‹LNC⇧_ _›) where "LNC⇧a η ≡ [⊢ η(a ❙∧ η a)]"
definition LNC::"'w Ω" where "LNC η ≡ ∀a. LNC⇧a η"
declare LNC_def[neg]
text‹ECQ and LNC are in general independent.›
lemma "ECQ η ⟹ LNC η" nitpick oops
lemma "LNC η ⟹ ECQm η" nitpick oops
subsubsection ‹Contraposition rules›
text‹CoP: contraposition (weak 'rule-like' variants).
Variant 0 is antitonicity (ANTI). Variants 1-3 are stronger.›
abbreviation pCoP1 (‹CoP1⇧_⇧_ _›) where "CoP1⇧a⇧b η ≡ [a ⊢ η b] ⟶ [b ⊢ η a]"
abbreviation pCoP2 (‹CoP2⇧_⇧_ _›) where "CoP2⇧a⇧b η ≡ [η a ⊢ b] ⟶ [η b ⊢ a]"
abbreviation pCoP3 (‹CoP3⇧_⇧_ _›) where "CoP3⇧a⇧b η ≡ [η a ⊢ η b] ⟶ [b ⊢ a]"
abbreviation CoP0 ::"'w Ω" where "CoP0 η ≡ ANTI η"
definition CoP1 ::"'w Ω" where "CoP1 η ≡ ∀a b. CoP1⇧a⇧b η"
definition CoP2 ::"'w Ω" where "CoP2 η ≡ ∀a b. CoP2⇧a⇧b η"
definition CoP3 ::"'w Ω" where "CoP3 η ≡ ∀a b. CoP3⇧a⇧b η"
declare CoP1_def[neg] CoP2_def[neg] CoP3_def[neg]
text‹Explore some (non)entailment relations.›
lemma "CoP1 η ⟹ CoP0 η" unfolding ANTI_def CoP1_def using subset_char1 by blast
lemma "CoP0 η ⟹ CoP1 η" nitpick oops
lemma "CoP2 η ⟹ CoP0 η" unfolding ANTI_def CoP2_def using subset_char1 by blast
lemma "CoP0 η ⟹ CoP2 η" nitpick oops
lemma "CoP3 η ⟹ CoP0 η" oops
lemma "CoP0 η ⟹ CoP3 η" nitpick oops
text‹All three strong variants are pairwise independent. However, CoP3 follows from CoP1 plus CoP2.›
lemma CoP123: "CoP1 η ⟹ CoP2 η ⟹ CoP3 η" unfolding neg order by smt
text‹Taking all CoP together still leaves room for a boldly paraconsistent resp. paracomplete logic.›
lemma "CoP1 η ⟹ CoP2 η ⟹ ECQm η" nitpick oops
lemma "CoP1 η ⟹ CoP2 η ⟹ TNDm η" nitpick oops
subsubsection ‹Modus tollens rules›
text‹MT: modus (tollendo) tollens (weak 'rule-like' variants).›
abbreviation pMT0 (‹MT0⇧_⇧_ _›) where "MT0⇧a⇧b η ≡ [a ⊢ b] ∧ [⊢ η b] ⟶ [⊢ η a]"
abbreviation pMT1 (‹MT1⇧_⇧_ _›) where "MT1⇧a⇧b η ≡ [a ⊢ η b] ∧ [⊢ b] ⟶ [⊢ η a]"
abbreviation pMT2 (‹MT2⇧_⇧_ _›) where "MT2⇧a⇧b η ≡ [η a ⊢ b] ∧ [⊢ η b] ⟶ [⊢ a]"
abbreviation pMT3 (‹MT3⇧_⇧_ _›) where "MT3⇧a⇧b η ≡ [η a ⊢ η b] ∧ [⊢ b] ⟶ [⊢ a]"
definition MT0::"'w Ω" where "MT0 η ≡ ∀a b. MT0⇧a⇧b η"
definition MT1::"'w Ω" where "MT1 η ≡ ∀a b. MT1⇧a⇧b η"
definition MT2::"'w Ω" where "MT2 η ≡ ∀a b. MT2⇧a⇧b η"
definition MT3::"'w Ω" where "MT3 η ≡ ∀a b. MT3⇧a⇧b η"
declare MT0_def[neg] MT1_def[neg] MT2_def[neg] MT3_def[neg]
text‹Again, all MT variants are pairwise independent. We explore some (non)entailment relations.›
lemma "CoP0 η ⟹ MT0 η" unfolding neg order cond conn by blast
lemma "CoP1 η ⟹ MT1 η" unfolding neg order conn by blast
lemma "CoP2 η ⟹ MT2 η" unfolding neg order conn by blast
lemma "CoP3 η ⟹ MT3 η" unfolding neg order conn by blast
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ CoP0 η" nitpick oops
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ ECQm η" nitpick oops
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ TNDm η" nitpick oops
lemma MT123: "MT1 η ⟹ MT2 η ⟹ MT3 η" unfolding neg order conn by metis
subsubsection ‹Double negation introduction and elimination›
text‹DNI/DNE: double negation introduction/elimination (strong 'axiom-like' variants).›
abbreviation pDNI (‹DNI⇧_ _›) where "DNI⇧a η ≡ [a ⊢ η(η a)]"
abbreviation pDNE (‹DNE⇧_ _›) where "DNE⇧a η ≡ [η(η a) ⊢ a]"
definition DNI::"'w Ω" where "DNI η ≡ ∀a. DNI⇧a η"
definition DNE::"'w Ω" where "DNE η ≡ ∀a. DNE⇧a η"
declare DNI_def[neg] DNE_def[neg]
text‹CoP1 (resp. CoP2) can alternatively be defined as CoPw plus DNI (resp. DNE).›
lemma "DNI η ⟹ CoP1 η" nitpick oops
lemma CoP1_def2: "CoP1 η = (CoP0 η ∧ DNI η)" unfolding neg cond using subset_char2 by blast
lemma "DNE η ⟹ CoP2 η" nitpick oops
lemma CoP2_def2: "CoP2 η = (CoP0 η ∧ DNE η)" unfolding neg cond using subset_char1 by blast
text‹Explore some non-entailment relations:›
lemma "DNI η ⟹ DNE η ⟹ CoP0 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ TNDm η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ ECQm η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT0 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT1 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT2 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT3 η" nitpick oops
text‹DNI/DNE: double negation introduction/elimination (weak 'rule-like' variants).›
abbreviation prDNI (‹rDNI⇧_ _›) where "rDNI⇧a η ≡ [⊢ a] ⟶ [⊢ η(η a)]"
abbreviation prDNE (‹rDNE⇧_ _›) where "rDNE⇧a η ≡ [⊢ η(η a)] ⟶ [⊢ a]"
definition rDNI::"'w Ω" where "rDNI η ≡ ∀a. rDNI⇧a η"
definition rDNE::"'w Ω" where "rDNE η ≡ ∀a. rDNE⇧a η"
declare rDNI_def[neg] rDNE_def[neg]
text‹The 'rule-like' variants for DNI/DNE are strictly weaker than the 'axiom-like' ones.›
lemma "DNI η ⟹ rDNI η" unfolding neg order conn by simp
lemma "rDNI η ⟹ DNI η" nitpick oops
lemma "DNE η ⟹ rDNE η" unfolding neg order conn by blast
lemma "rDNE η ⟹ DNE η" nitpick oops
text‹The 'rule-like' variants for DNI/DNE follow already from modus tollens.›
lemma MT1_rDNI: "MT1 η ⟹ rDNI η" unfolding neg order by blast
lemma MT2_rDNE: "MT2 η ⟹ rDNE η" unfolding neg order by blast
subsubsection ‹(Anti)Normality and its dual›
text‹nNORM (resp. nDNRM) is entailed by CoP1 (resp. CoP2). ›
lemma CoP1_NORM: "CoP1 η ⟹ nNORM η" unfolding neg cond conn order by simp
lemma CoP2_DNRM: "CoP2 η ⟹ nDNRM η" unfolding neg cond conn by (smt (verit) setequ_char subset_def)
lemma "DNI η ⟹ nNORM η" nitpick oops
lemma "DNE η ⟹ nDNRM η" nitpick oops
text‹nNORM and nDNRM together entail the rule variant of DNI (rDNI).›
lemma nDNRM_rDNI: "nNORM η ⟹ nDNRM η ⟹ rDNI η" unfolding neg cond by (simp add: gtrue_def setequ_ext)
lemma "nNORM η ⟹ nDNRM η ⟹ rDNE η" nitpick oops
subsubsection ‹De Morgan laws›
text‹De Morgan laws correspond to anti-additivity and anti-multiplicativity).›
text‹DM3 (resp. DM4) are entailed by CoP0/ANTI together with DNE (resp. DNI).›
lemma CoP0_DNE_nMULTb: "CoP0 η ⟹ DNE η ⟹ nMULT⇧b η" unfolding neg cond by (metis ANTI_def ANTI_nADDIb L12 nADDI_b_def subset_char1)
lemma CoP0_DNI_nADDIa: "CoP0 η ⟹ DNI η ⟹ nADDI⇧a η" unfolding neg cond by (metis ANTI_def ANTI_nMULTa L11 nMULT_a_def subset_char2)
text‹From this follows that DM3 (resp. DM4) is entailed by CoP2 (resp. CoP1).›
lemma CoP2_nMULTb: "CoP2 η ⟹ nMULT⇧b η" by (simp add: CoP0_DNE_nMULTb CoP2_def2)
lemma CoP1_nADDIa: "CoP1 η ⟹ nADDI⇧a η" by (simp add: CoP0_DNI_nADDIa CoP1_def2)
text‹Explore some non-entailment relations:›
lemma "CoP0 η ⟹ nADDI⇧a η ⟹ nMULT⇧b η ⟹ nNORM η ⟹ nDNRM η ⟹ DNI η" nitpick oops
lemma "CoP0 η ⟹ nADDI⇧a η ⟹ nMULT⇧b η ⟹ nNORM η ⟹ nDNRM η ⟹ DNE η" nitpick oops
lemma "CoP0 η ⟹ nADDI⇧a η ⟹ nMULT⇧b η ⟹ DNI η ⟹ DNE η ⟹ ECQm η" nitpick oops
lemma "CoP0 η ⟹ nADDI⇧a η ⟹ nMULT⇧b η ⟹ DNI η ⟹ DNE η ⟹ TNDm η" nitpick oops
subsubsection ‹Strong contraposition (axiom-like)›
text‹Observe that the definitions below take implication as an additional parameter: @{text "ι"}.›
text‹lCoP: (local) contraposition (strong 'axiom-like' variants, using local consequence).›
abbreviation plCoP0 (‹lCoP0⇧_⇧_ _ _›) where "lCoP0⇧a⇧b ι η ≡ [ι a b ⊢ ι (η b) (η a)]"
abbreviation plCoP1 (‹lCoP1⇧_⇧_ _ _›) where "lCoP1⇧a⇧b ι η ≡ [ι a (η b) ⊢ ι b (η a)]"
abbreviation plCoP2 (‹lCoP2⇧_⇧_ _ _›) where "lCoP2⇧a⇧b ι η ≡ [ι (η a) b ⊢ ι (η b) a]"
abbreviation plCoP3 (‹lCoP3⇧_⇧_ _ _›) where "lCoP3⇧a⇧b ι η ≡ [ι (η a) (η b) ⊢ ι b a]"
definition lCoP0::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lCoP0 ι η ≡ ∀a b. lCoP0⇧a⇧b ι η"
definition lCoP1::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lCoP1 ι η ≡ ∀a b. lCoP1⇧a⇧b ι η"
definition lCoP2::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lCoP2 ι η ≡ ∀a b. lCoP2⇧a⇧b ι η"
definition lCoP3::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lCoP3 ι η ≡ ∀a b. lCoP3⇧a⇧b ι η"
declare lCoP0_def[neg] lCoP1_def[neg] lCoP2_def[neg] lCoP3_def[neg]
text‹All these contraposition variants are in general independent from each other.
However if we employ classical implication we can verify some relationships.›
lemma lCoP1_def2: "lCoP1(❙→) η = (lCoP0(❙→) η ∧ DNI η)" unfolding neg conn order by metis
lemma lCoP2_def2: "lCoP2(❙→) η = (lCoP0(❙→) η ∧ DNE η)" unfolding neg conn order by blast
lemma "lCoP1(❙→) η ⟹ lCoP0(❙→) η" unfolding neg conn order by blast
lemma "lCoP0(❙→) η ⟹ lCoP1(❙→) η" nitpick oops
lemma "lCoP2(❙→) η ⟹ lCoP0(❙→) η" unfolding neg conn order by blast
lemma "lCoP0(❙→) η ⟹ lCoP2(❙→) η" nitpick oops
lemma "lCoP3(❙→) η ⟹ lCoP0(❙→) η" unfolding neg conn order by blast
lemma "lCoP0(❙→) η ⟹ lCoP3(❙→) η" nitpick oops
lemma lCoP123: "lCoP1(❙→) η ∧ lCoP2(❙→) η ⟹ lCoP3(❙→) η" unfolding neg conn order by metis
text‹Strong/axiom-like variants imply weak/rule-like ones as expected.›
lemma "lCoP0(❙→) η ⟹ CoP0 η" unfolding neg cond conn order by blast
lemma "lCoP1(❙→) η ⟹ CoP1 η" unfolding neg conn order by blast
lemma "lCoP2(❙→) η ⟹ CoP2 η" unfolding neg conn order by blast
lemma "lCoP3(❙→) η ⟹ CoP3 η" unfolding neg conn order by blast
text‹Explore some (non)entailment relations.›
lemma lCoP1_TND: "lCoP1(❙→) η ⟹ TND η" unfolding neg conn by (smt (verit, best) setequ_char subset_def)
lemma "TND η ⟹ lCoP1(❙→) η" nitpick oops
lemma lCoP2_ECQ: "lCoP2(❙→) η ⟹ ECQ η" unfolding neg conn by (smt (verit) setequ_def subset_def)
lemma "ECQ η ⟹ lCoP2(❙→) η" nitpick oops
subsubsection ‹Local modus tollens axioms›
text‹lMT: (local) Modus tollens (strong, 'axiom-like' variants, using local consequence).›
abbreviation plMT0 (‹lMT0⇧_⇧_ _ _›) where "lMT0⇧a⇧b ι η ≡ [ι a b, η b ⊢ η a]"
abbreviation plMT1 (‹lMT1⇧_⇧_ _ _›) where "lMT1⇧a⇧b ι η ≡ [ι a (η b), b ⊢ η a]"
abbreviation plMT2 (‹lMT2⇧_⇧_ _ _›) where "lMT2⇧a⇧b ι η ≡ [ι (η a) b, η b ⊢ a]"
abbreviation plMT3 (‹lMT3⇧_⇧_ _ _›) where "lMT3⇧a⇧b ι η ≡ [ι (η a) (η b), b ⊢ a]"
definition lMT0::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lMT0 ι η ≡ ∀a b. lMT0⇧a⇧b ι η"
definition lMT1::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lMT1 ι η ≡ ∀a b. lMT1⇧a⇧b ι η"
definition lMT2::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lMT2 ι η ≡ ∀a b. lMT2⇧a⇧b ι η"
definition lMT3::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "lMT3 ι η ≡ ∀a b. lMT3⇧a⇧b ι η"
declare lMT0_def[neg] lMT1_def[neg] lMT2_def[neg] lMT3_def[neg]
text‹All these MT variants are in general independent from each other and also from (strong) CoP instances.
However if we take classical implication we can verify that local MT and CoP are indeed equivalent.›
lemma "lMT0(❙→) η = lCoP0(❙→) η" unfolding neg conn order by blast
lemma "lMT1(❙→) η = lCoP1(❙→) η" unfolding neg conn order by blast
lemma "lMT2(❙→) η = lCoP2(❙→) η" unfolding neg conn order by blast
lemma "lMT3(❙→) η = lCoP3(❙→) η" unfolding neg conn order by blast
subsubsection ‹Disjunctive syllogism›
text‹DS: disjunctive syllogism.›
abbreviation pDS1 (‹DS1⇧_⇧_ _ _›) where "DS1⇧a⇧b ι η ≡ [a ❙∨ b ⊢ ι (η a) b]"
abbreviation pDS2 (‹DS2⇧_⇧_ _ _›) where "DS2⇧a⇧b ι η ≡ [ι (η a) b ⊢ a ❙∨ b]"
abbreviation pDS3 (‹DS3⇧_⇧_ _ _›) where "DS3⇧a⇧b ι η ≡ [η a ❙∨ b ⊢ ι a b]"
abbreviation pDS4 (‹DS4⇧_⇧_ _ _›) where "DS4⇧a⇧b ι η ≡ [ι a b ⊢ η a ❙∨ b]"
definition DS1::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "DS1 ι η ≡ ∀a b. DS1⇧a⇧b ι η"
definition DS2::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "DS2 ι η ≡ ∀a b. DS2⇧a⇧b ι η"
definition DS3::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "DS3 ι η ≡ ∀a b. DS3⇧a⇧b ι η"
definition DS4::"('w σ⇒'w σ⇒'w σ) ⇒ 'w Ω" where "DS4 ι η ≡ ∀a b. DS4⇧a⇧b ι η"
declare DS1_def[neg] DS2_def[neg] DS3_def[neg] DS4_def[neg]
text‹All DS variants are in general independent from each other. However if we take classical implication
we can verify that the pairs DS1-DS3 and DS2-DS4 are indeed equivalent. ›
lemma "DS1(❙→) η = DS3(❙→) η" unfolding neg conn order by blast
lemma "DS2(❙→) η = DS4(❙→) η" unfolding neg conn order by blast
text‹Explore some (non)entailment relations.›
lemma DS1_nDNor: "DS1(❙→) η ⟹ nDNRM η" unfolding neg cond conn order by metis
lemma DS2_nNor: "DS2(❙→) η ⟹ nNORM η" unfolding neg cond conn order by metis
lemma lCoP2_DS1: "lCoP2(❙→) η ⟹ DS1(❙→) η" unfolding neg conn order by blast
lemma lCoP1_DS2: "lCoP1(❙→) η ⟹ DS2(❙→) η" unfolding neg conn order by blast
lemma "CoP2 η ⟹ DS1(❙→) η" nitpick oops
lemma "CoP1 η ⟹ DS2(❙→) η" nitpick oops
end