Commit 08009842 authored by Rene Thiemann's avatar Rene Thiemann
Browse files

new entry: Topological_Semantics

parent cd33914660a2
......@@ -163,8 +163,8 @@ Fermat3_4
FileRefinement
FinFun
Finger-Trees
Finite_Automata_HF
Finite-Map-Extras
Finite_Automata_HF
First_Order_Terms
First_Welfare_Theorem
Fishburn_Impossibility
......@@ -527,6 +527,7 @@ Tail_Recursive_Functions
Tarskis_Geometry
Taylor_Models
Timed_Automata
Topological_Semantics
Topology
TortoiseHare
Transcendence_Series_Hancl_Rucki
......
chapter AFP
session "Topological_Semantics" (AFP) = "HOL" +
options [timeout = 600]
theories
sse_boolean_algebra
sse_boolean_algebra_quantification
sse_operation_positive
sse_operation_positive_quantification
sse_operation_negative
sse_operation_negative_quantification
topo_operators_basic
topo_operators_derivative
topo_alexandrov
topo_frontier_algebra
topo_negation_conditions
topo_negation_fixedpoints
ex_LFIs
topo_strict_implication
ex_subminimal_logics
topo_derivative_algebra
ex_LFUs
topo_border_algebra
topo_closure_algebra
topo_interior_algebra
document_files
"root.tex"
"root.bib"
@article{J23,
keywords = {Higher Order Logic, Semantic Embedding, Modal
Logics, Henkin Semantics},
author = {C. Benzm{\"u}ller and L.C. Paulson},
title = {Quantified Multimodal Logics in Simple Type Theory},
journal = {Logica Universalis (Special Issue on Multimodal
Logics)},
year = 2013,
volume = 7,
number = 1,
pages = {7-20},
doi = {10.1007/s11787-012-0052-y},
Note = {Preprint:
\url{http://christoph-benzmueller.de/papers/J23.pdf}}
}
@article{J41,
author = {Christoph Benzm{\"u}ller},
title = {Universal (Meta-)Logical Reasoning: Recent
Successes},
journal = {Science of Computer Programming},
year = 2019,
volume = 172,
pages = {48-62},
Note = {Preprint:
\url{http://doi.org/10.13140/RG.2.2.11039.61609/2}},
doi = {10.1016/j.scico.2018.10.008},
}
@book{Hausdorff,
title={Grundz{\"u}ge der {M}engenlehre},
author={Hausdorff, Felix},
volume={7},
year={1914},
publisher={von Veit}
}
@article{AOT,
title={The algebra of topology},
author={McKinsey, John Charles Chenoweth and Tarski, Alfred},
journal={Annals of mathematics},
pages={141--191},
year={1944},
publisher={JSTOR}
}
@article{Zarycki1,
title={Quelques notions fondamentales de l'Analysis Situs au point de vue de l'Alg{\`e}bre de la Logique},
author={Zarycki, Miron},
journal={Fundamenta Mathematicae},
volume={9},
number={1},
pages={3--15},
year={1927},
publisher={Institute of Mathematics Polish Academy of Sciences},
Note = {English translation by Mark Bowron:
\url{https://www.researchgate.net/scientific-contributions/Miron-Zarycki-2016157096}}
}
@article{Zarycki2,
title={Allgemeine {E}igenschaften der Cantorschen {K}oh{\"a}renzen},
author={Zarycki, Miron},
journal={Transactions of the American Mathematical Society},
volume={30},
number={3},
pages={498--506},
year={1928},
publisher={JSTOR},
Note = {English translation by Mark Bowron:
\url{https://www.researchgate.net/scientific-contributions/Miron-Zarycki-2016157096}}
}
@article{Zarycki3,
title={Some Properties of the Derived Set Operation in Abstract Spaces.},
author={Zarycki, Miron},
journal={Nauk. Zap. Ser. Fiz.-Mat.},
volume={5},
pages={22-33},
year={1947},
Note = {English translation by Mark Bowron:
\url{https://www.researchgate.net/scientific-contributions/Miron-Zarycki-2016157096}}
}
@article{Kuratowski1,
title={Sur l'op{\'e}ration \={A} de l'analysis situs},
author={Kuratowski, Kazimierz},
journal={Fundamenta Mathematicae},
volume={3},
number={1},
pages={182--199},
year={1922}
}
@article{JML,
title={Der {M}inimalkalk{\"u}l, ein reduzierter intuitionistischer {F}ormalismus},
author={Johansson, Ingebrigt},
journal={Compositio mathematica},
volume={4},
pages={119--136},
year={1937}
}
@book{Kuratowski2,
title={Topology: Volume I},
author={Kuratowski, Kazimierz},
volume={1},
year={2014},
publisher={Elsevier}
}
@article{Esakia,
title={Intuitionistic logic and modality via topology},
author={Esakia, Leo},
journal={Annals of Pure and Applied Logic},
volume={127},
number={1-3},
pages={155--170},
year={2004},
publisher={Elsevier}
}
@incollection{LFI,
title={Logics of formal inconsistency},
author={Carnielli, Walter and Coniglio, Marcelo E and Marcos, Joao},
booktitle={Handbook of philosophical logic},
pages={1--93},
year={2007},
publisher={Springer}
}
@article{RLFI,
title={Logics of Formal Inconsistency enriched with replacement: an algebraic and modal account},
author={Walter Carnielli and Marcelo E. Coniglio and David Fuenmayor},
year={2020},
number={2003.09522},
journal={arXiv},
volume={math.LO}
}
@article{LFU,
title={Nearly every normal modal logic is paranormal},
author={Marcos, Joao},
journal={Logique et Analyse},
volume={48},
number={189/192},
pages={279--300},
year={2005},
publisher={JSTOR}
}
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
%\usepackage{a4wide}
\usepackage{fullpage}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage{eurosym}
%for \<euro>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
%\<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
\begin{document}
\title{Topological semantics for paraconsistent and paracomplete logics}
\author{David Fuenmayor}
\maketitle
\begin{abstract}
We introduce a generalized topological semantics for paraconsistent and paracomplete logics by drawing upon early works on topological Boolean algebras (cf.~works by Kuratowski, Zarycki, McKinsey \& Tarski, etc.). In particular, this work exemplarily illustrates the shallow semantical embeddings approach (SSE) employing the proof assistant Isabelle/HOL. By means of the SSE technique we can effectively harness theorem provers, model finders and `hammers' for reasoning with quantified non-classical logics.
\end{abstract}
\tableofcontents
\vspace*{40pt}
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
% generated text of all theories
\input{session}
% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
theory ex_LFIs
imports topo_negation_conditions
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)
section \<open>Example application: Logics of Formal Inconsistency (LFIs)\<close>
text\<open>\noindent{The LFIs @{cite LFI} @{cite RLFI} are a family of paraconsistent logics featuring a 'consistency'
operator @{text "\<^bold>\<circ>"} that can be used to recover some classical properties of negation (in particular ECQ).
We show how to semantically embed LFIs as extensions of Boolean algebras (here as frontier algebras).}\<close>
text\<open>\noindent{Logical validity can be defined as truth in all worlds/points (i.e. as denoting the top element)}\<close>
abbreviation gtrue::"\<sigma>\<Rightarrow>bool" ("[\<^bold>\<turnstile> _]") where "[\<^bold>\<turnstile> A] \<equiv> \<forall>w. A w"
lemma gtrue_def: "[\<^bold>\<turnstile> A] \<equiv> A \<^bold>\<approx> \<^bold>\<top>" by (simp add: top_def)
text\<open>\noindent{When defining a logic over an existing algebra we have two choices: a global (truth preserving)
and a local (truth-degree preserving) notion of logical consequence. For LFIs we prefer the latter.}\<close>
abbreviation conseq_global1::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_ \<^bold>\<turnstile>\<^sub>g _]") where "[A \<^bold>\<turnstile>\<^sub>g B] \<equiv> [\<^bold>\<turnstile> A] \<longrightarrow> [\<^bold>\<turnstile> B]"
abbreviation conseq_global2::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_ \<^bold>\<turnstile>\<^sub>g _]") where "[A\<^sub>1, A\<^sub>2 \<^bold>\<turnstile>\<^sub>g B] \<equiv> [\<^bold>\<turnstile> A\<^sub>1] \<and> [\<^bold>\<turnstile> A\<^sub>2] \<longrightarrow> [\<^bold>\<turnstile> B]"
abbreviation conseq_global3::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_,_ \<^bold>\<turnstile>\<^sub>g _]") where "[A\<^sub>1, A\<^sub>2, A\<^sub>3 \<^bold>\<turnstile>\<^sub>g B] \<equiv> [\<^bold>\<turnstile> A\<^sub>1] \<and> [\<^bold>\<turnstile> A\<^sub>2] \<and> [\<^bold>\<turnstile> A\<^sub>3] \<longrightarrow> [\<^bold>\<turnstile> B]"
abbreviation conseq_local1::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_ \<^bold>\<turnstile> _]") where "[A \<^bold>\<turnstile> B] \<equiv> A \<^bold>\<preceq> B"
abbreviation conseq_local2::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_ \<^bold>\<turnstile> _]") where "[A\<^sub>1, A\<^sub>2 \<^bold>\<turnstile> B] \<equiv> A\<^sub>1 \<^bold>\<and> A\<^sub>2 \<^bold>\<preceq> B"
abbreviation conseq_local3::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_,_ \<^bold>\<turnstile> _]") where "[A\<^sub>1, A\<^sub>2, A\<^sub>3 \<^bold>\<turnstile> B] \<equiv> A\<^sub>1 \<^bold>\<and> A\<^sub>2 \<^bold>\<and> A\<^sub>3 \<^bold>\<preceq> B"
(*add more as the need arises...*)
text\<open>\noindent{For LFIs we use the (paraconsistent) closure-based negation previously defined (taking frontier as primitive). }\<close>
abbreviation cneg::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<not>") where "\<^bold>\<not>A \<equiv> \<^bold>\<not>\<^sup>CA"
text\<open>\noindent{In terms of the frontier operator the negation looks as follows:}\<close>
lemma "\<^bold>\<not>A \<^bold>\<approx> \<^bold>\<midarrow>A \<^bold>\<or> \<F>(\<^bold>\<midarrow>A)" by (simp add: neg_C_def pC2)
lemma cneg_prop: "Fr_2 \<F> \<Longrightarrow> \<^bold>\<not>A \<^bold>\<approx> \<^bold>\<midarrow>A \<^bold>\<or> \<F>(A)" using pC2 pF2 unfolding conn by blast
text\<open>\noindent{This negation is of course boldly paraconsistent.}\<close>
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile> b]" nitpick oops (*countermodel*)
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile> \<^bold>\<not>b]" nitpick oops (*countermodel*)
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g b]" nitpick oops (*countermodel*)
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g \<^bold>\<not>b]" nitpick oops (*countermodel*)
text\<open>\noindent{We define two pairs of in/consistency operators and show how they relate to each other.
Using LFIs terminology, the minimal logic so encoded corresponds to 'RmbC-ciw' (cf. @{cite RLFI}).}\<close>
abbreviation op_inc_a::"\<sigma>\<Rightarrow>\<sigma>" ("\<bullet>\<^sup>A_" [57]58) where "\<bullet>\<^sup>AA \<equiv> A \<^bold>\<and> \<^bold>\<not>A"
abbreviation op_con_a::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<circ>\<^sup>A_" [57]58) where "\<^bold>\<circ>\<^sup>AA \<equiv> \<^bold>\<midarrow>\<bullet>\<^sup>AA"
abbreviation op_inc_b::"\<sigma>\<Rightarrow>\<sigma>" ("\<bullet>\<^sup>B_" [57]58) where "\<bullet>\<^sup>BA \<equiv> \<B> A"
abbreviation op_con_b::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<circ>\<^sup>B_" [57]58) where "\<^bold>\<circ>\<^sup>BA \<equiv> \<B>\<^sup>c A"
text\<open>\noindent{Observe that assumming condition Fr-2 are we allowed to exchange A and B variants.}\<close>
lemma pincAB: "Fr_2 \<F> \<Longrightarrow> \<bullet>\<^sup>AA \<^bold>\<approx> \<bullet>\<^sup>BA" using Br_fr_def Cl_fr_def pF2 conn by auto
lemma pconAB: "Fr_2 \<F> \<Longrightarrow> \<^bold>\<circ>\<^sup>AA \<^bold>\<approx> \<^bold>\<circ>\<^sup>BA" using pincAB unfolding conn by simp
text\<open>\noindent{Variants A and B give us slightly different properties.}\<close>
lemma Prop1: "\<^bold>\<circ>\<^sup>BA \<^bold>\<approx> \<I>\<^sup>f\<^sup>p A" using fp1 unfolding conn equal_op_def by metis
lemma "\<^bold>\<circ>\<^sup>AA \<^bold>\<approx> A \<^bold>\<rightarrow> \<I> A" nitpick oops (*countermodel*)
lemma Prop2: "Cl A \<longleftrightarrow> \<^bold>\<circ>\<^sup>A\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<top>" using pC2 unfolding conn by auto
lemma "Cl A \<longrightarrow> \<^bold>\<circ>\<^sup>B\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<top>" nitpick oops (*countermodel*)
lemma Prop3: "Cl A \<longleftrightarrow> \<bullet>\<^sup>A\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<bottom>" using Cl_fr_def unfolding conn by auto
lemma "Cl A \<longrightarrow> \<bullet>\<^sup>B\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<bottom>" nitpick oops (*countermodel*)
lemma Prop4: "Op A \<longleftrightarrow> \<^bold>\<circ>\<^sup>BA \<^bold>\<approx> \<^bold>\<top>" using Op_Bzero unfolding conn by simp
lemma "Op A \<longrightarrow> \<^bold>\<circ>\<^sup>AA \<^bold>\<approx> \<^bold>\<top>" nitpick oops (*countermodel*)
lemma Prop5: "Op A \<longleftrightarrow> \<bullet>\<^sup>BA \<^bold>\<approx> \<^bold>\<bottom>" using Op_Bzero by simp
lemma "Op A \<longrightarrow> \<bullet>\<^sup>AA \<^bold>\<approx> \<^bold>\<bottom>" nitpick oops (*countermodel*)
text\<open>\noindent{Importantly, LFIs must satisfy the so-called 'principle of gentle explosion'. Only variant A works here:}\<close>
lemma "[\<^bold>\<circ>\<^sup>Aa, a, \<^bold>\<not>a \<^bold>\<turnstile> b]" using compl_def meet_def by auto
lemma "[\<^bold>\<circ>\<^sup>Aa, a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g b]" using compl_def meet_def by auto
lemma "[\<^bold>\<circ>\<^sup>Ba, a, \<^bold>\<not>a \<^bold>\<turnstile> b]" nitpick oops (*countermodel*)
lemma "[\<^bold>\<circ>\<^sup>Ba, a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g b]" nitpick oops (*countermodel*)
text\<open>\noindent{In what follows we employ the (minimal) A-variant and verify some properties.}\<close>
abbreviation op_inc :: "\<sigma>\<Rightarrow>\<sigma>" ("\<bullet>_" [57]58) where "\<bullet>A \<equiv> \<bullet>\<^sup>AA"
abbreviation op_con :: "\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<circ>_" [57]58) where "\<^bold>\<circ>A \<equiv> \<^bold>\<midarrow>\<bullet>A"
lemma "TND(\<^bold>\<not>)" by (simp add: TND_C)
lemma "ECQm(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> LNC(\<^bold>\<not>)" by (simp add: LNC_C PF6)
lemma "\<FF> \<F> \<Longrightarrow> DNI(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<FF> \<F> \<Longrightarrow> DNE(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> CoPw(\<^bold>\<not>)" by (simp add: CoPw_C PF6)
lemma "\<FF> \<F> \<Longrightarrow> CoP1(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<FF> \<F> \<Longrightarrow> CoP2(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<FF> \<F> \<Longrightarrow> CoP3(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1a \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> DM3(\<^bold>\<not>)" by (simp add: DM3_C)
lemma "\<FF> \<F> \<Longrightarrow> DM4(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "nNor(\<^bold>\<not>)" by (simp add: nNor_C)
lemma "Fr_3 \<F> \<Longrightarrow> nDNor(\<^bold>\<not>)" by (simp add: nDNor_C)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> MT0(\<^bold>\<not>)" by (simp add: MT0_C PF6)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> MT1(\<^bold>\<not>)" by (simp add: MT1_C PF6)
lemma "\<FF> \<F> \<Longrightarrow> MT2(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> MT3(\<^bold>\<not>)" using MT3_C by auto
text\<open>\noindent{We show how all local contraposition variants (lCoP) can be recovered using the consistency operator.
Observe that we can recover in the same way other (weaker) properties: CoP, MT and DNI/DNE (local \& global).}\<close>
lemma "\<FF> \<F> \<Longrightarrow> lCoPw(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop1: "[\<^bold>\<circ>b, a \<^bold>\<rightarrow> b \<^bold>\<turnstile> \<^bold>\<not>b \<^bold>\<rightarrow> \<^bold>\<not>a]" using Cl_fr_def conn by auto
lemma "\<FF> \<F> \<Longrightarrow> lCoP1(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop2: "[\<^bold>\<circ>b, a \<^bold>\<rightarrow> \<^bold>\<not>b \<^bold>\<turnstile> b \<^bold>\<rightarrow> \<^bold>\<not>a]" using Cl_fr_def conn by auto
lemma "\<FF> \<F> \<Longrightarrow> lCoP2(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop3: "[\<^bold>\<circ>b, \<^bold>\<not>a \<^bold>\<rightarrow> b \<^bold>\<turnstile> \<^bold>\<not>b \<^bold>\<rightarrow> a]" using Cl_fr_def conn by auto
lemma "\<FF> \<F> \<Longrightarrow> lCoP3(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop4: "[\<^bold>\<circ>b, \<^bold>\<not>a \<^bold>\<rightarrow> \<^bold>\<not>b \<^bold>\<turnstile> b \<^bold>\<rightarrow> a]" using Cl_fr_def conn by auto
text\<open>\noindent{Disjunctive syllogism (DS).}\<close>
lemma "\<FF> \<F> \<Longrightarrow> DS1(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_ds1: "[\<^bold>\<circ>a, a \<^bold>\<or> b \<^bold>\<turnstile> \<^bold>\<not>a \<^bold>\<rightarrow> b]" using conn by auto
lemma "DS2(\<^bold>\<rightarrow>)(\<^bold>\<not>)" by (metis Cl_fr_def DS2_def compl_def impl_def join_def neg_C_def)
text\<open>\noindent{Further properties.}\<close>
lemma "[a \<^bold>\<and> \<^bold>\<not>a \<^bold>\<turnstile> \<^bold>\<not>(\<^bold>\<circ>a)]" by (simp add: pC2 conn)
lemma "\<FF> \<F> \<Longrightarrow> [\<^bold>\<not>(\<^bold>\<circ>a) \<^bold>\<turnstile> a \<^bold>\<and> \<^bold>\<not>a]" nitpick oops (* countermodel found *)
lemma "[\<^bold>\<circ>a \<^bold>\<turnstile> \<^bold>\<not>(a \<^bold>\<and> \<^bold>\<not>a)]" by (simp add: pC2 conn)
lemma "\<FF> \<F> \<Longrightarrow> [\<^bold>\<not>(a \<^bold>\<and> \<^bold>\<not>a) \<^bold>\<turnstile> \<^bold>\<circ>a]" nitpick oops (* countermodel found *)
text\<open>\noindent{The following axioms are commonly employed in the literature on LFIs to obtain stronger logics.
We explore under which conditions they can be assumed while keeping the logic boldly paraconsistent.}\<close>
abbreviation cf where "cf \<equiv> DNE(\<^bold>\<not>)"
abbreviation ce where "ce \<equiv> DNI(\<^bold>\<not>)"
abbreviation ciw where "ciw \<equiv> \<forall>P. [\<^bold>\<turnstile> \<^bold>\<circ>P \<^bold>\<or> \<bullet>P]"
abbreviation ci where "ci \<equiv> \<forall>P. [\<^bold>\<not>(\<^bold>\<circ>P) \<^bold>\<turnstile> \<bullet>P]"
abbreviation cl where "cl \<equiv> \<forall>P. [\<^bold>\<not>(\<bullet>P) \<^bold>\<turnstile> \<^bold>\<circ>P]"
abbreviation ca_conj where "ca_conj \<equiv> \<forall>P Q. [\<^bold>\<circ>P,\<^bold>\<circ>Q \<^bold>\<turnstile> \<^bold>\<circ>(P \<^bold>\<and> Q)]"
abbreviation ca_disj where "ca_disj \<equiv> \<forall>P Q. [\<^bold>\<circ>P,\<^bold>\<circ>Q \<^bold>\<turnstile> \<^bold>\<circ>(P \<^bold>\<or> Q)]"
abbreviation ca_impl where "ca_impl \<equiv> \<forall>P Q. [\<^bold>\<circ>P,\<^bold>\<circ>Q \<^bold>\<turnstile> \<^bold>\<circ>(P \<^bold>\<rightarrow> Q)]"
abbreviation ca where "ca \<equiv> ca_conj \<and> ca_disj \<and> ca_impl"
text\<open>\noindent{cf}\<close>
lemma "\<FF> \<F> \<Longrightarrow> cf" nitpick oops
lemma "\<FF> \<F> \<and> cf \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
text\<open>\noindent{ce}\<close>
lemma "\<FF> \<F> \<Longrightarrow> ce" nitpick oops
lemma "Fr_1 \<F> \<and> Fr_2 \<F> \<and> Fr_4 \<F> \<and> ce \<and> \<sim>ECQ(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> ce \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1a \<F> \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> ce \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> ce \<longrightarrow> ECQm(\<^bold>\<not>)" unfolding Defs using CoP1_XCoP CoP1_def2 CoPw_C DNI_def ECQw_def PF6 XCoP_def2 by auto
text\<open>\noindent{ciw}\<close>
lemma ciw by (simp add:conn)
text\<open>\noindent{ci}\<close>
lemma "\<FF> \<F> \<Longrightarrow> ci" nitpick oops
lemma "\<FF> \<F> \<and> ci \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
text\<open>\noindent{cl}\<close>
lemma "\<FF> \<F> \<Longrightarrow> cl" nitpick oops
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1a \<F> \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> cl \<longrightarrow> ECQ(\<^bold>\<not>)" unfolding Defs by (metis BC_rel Br_Border Br_cl_def bottom_def compl_def eq_ext' meet_def neg_C_def)
text\<open>\noindent{ca-conj/disj}\<close>
lemma "Fr_1a \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> ca_conj" using DM3_C DM3_def conn by auto
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> ca_disj" using ADDI_b_def MONO_ADDIb monI pB1 pincAB unfolding conn by metis
lemma "\<FF> \<F> \<Longrightarrow> ca_impl" nitpick oops
text\<open>\noindent{ca-impl}\<close>
lemma "ca_impl \<and> \<sim>ECQ(\<^bold>\<not>)" (*nitpick[satisfy]*) oops (*cannot find finite model*)
lemma "ca_impl \<longrightarrow> ECQm(\<^bold>\<not>)" oops (*nor proof yet*)
text\<open>\noindent{cf \& ci}\<close>
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> ci \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> ci \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<and> Fr_2 \<F> \<and> cf \<and> ci \<and> \<sim>ECQ(\<^bold>\<not>)" (*nitpick[satisfy]*) oops (*cannot find finite model*)
lemma "\<FF> \<F> \<and> cf \<and> ci \<longrightarrow> ECQm(\<^bold>\<not>)" oops (*nor proof yet*)
text\<open>\noindent{cf \& cl}\<close>
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<and> Fr_2 \<F> \<and> cf \<and> cl \<longrightarrow> ECQ(\<^bold>\<not>)" unfolding Defs by (smt Br_fr_def Fr_1b_def Prop2 Prop3 pF3 cneg_prop conn)
end
theory ex_LFUs
imports topo_derivative_algebra sse_operation_negative
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)
section \<open>Example application: Logics of Formal Undeterminedness (LFUs)\<close>
text\<open>\noindent{The LFUs @{cite LFU} @{cite LFI} are a family of paracomplete logics featuring a 'determinedness'
operator @{text "\<^bold>\<circ>"} that can be used to recover some classical properties of negation (in particular TND).
LFUs behave in a sense dually to LFIs. Both can be semantically embedded as extensions of Boolean algebras.
Here we show how to semantically embed LFUs as derivative algebras.}\<close>
text\<open>\noindent{(We rename (classical) meta-logical negation to avoid terminological confusion)}\<close>
abbreviation cneg::"bool\<Rightarrow>bool" ("\<sim>_" [40]40) where "\<sim>\<phi> \<equiv> \<not>\<phi>"
text\<open>\noindent{Logical validity can be defined as truth in all worlds/points (i.e. as denoting the top element)}\<close>
abbreviation gtrue::"\<sigma>\<Rightarrow>bool" ("[\<^bold>\<turnstile> _]") where "[\<^bold>\<turnstile> A] \<equiv> \<forall>w. A w"
lemma gtrue_def: "[\<^bold>\<turnstile> A] \<equiv> A \<^bold>\<approx> \<^bold>\<top>" by (simp add: top_def)
text\<open>\noindent{As for LFIs, we focus on the local (truth-degree preserving) notion of logical consequence.}\<close>
abbreviation conseq_local1::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_ \<^bold>\<turnstile> _]") where "[A \<^bold>\<turnstile> B] \<equiv> A \<^bold>\<preceq> B"
abbreviation conseq_local2::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_ \<^bold>\<turnstile> _]") where "[A\<^sub>1, A\<^sub>2 \<^bold>\<turnstile> B] \<equiv> A\<^sub>1 \<^bold>\<and> A\<^sub>2 \<^bold>\<preceq> B"
abbreviation conseq_local12::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_ \<^bold>\<turnstile> _,_]") where "[A \<^bold>\<turnstile> B\<^sub>1, B\<^sub>2] \<equiv> A \<^bold>\<preceq> B\<^sub>1 \<^bold>\<or> B\<^sub>2"
(*add more as the need arises...*)
text\<open>\noindent{For LFUs we use the interior-based negation previously defined (taking derivative as primitive). }\<close>
definition ineg::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<not>") where "\<^bold>\<not>A \<equiv> \<I>(\<^bold>\<midarrow>A)"
declare ineg_def[conn]
text\<open>\noindent{In terms of the derivative operator the negation looks as follows:}\<close>
lemma ineg_prop: "\<^bold>\<not>A \<^bold>\<approx> \<^bold>\<midarrow>(\<D> A) \<^bold>\<leftharpoonup> A" using Cl_der_def IB_rel Int_br_def eq_ext' pB4 conn by fastforce
text\<open>\noindent{This negation is of course paracomplete.}\<close>
lemma "[\<^bold>\<turnstile> a \<^bold>\<or> \<^bold>\<not>a]" nitpick oops (*countermodel*)
text\<open>\noindent{We define two pairs of in/determinedness operators and show how they relate to each other.}\<close>
abbreviation op_det::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<circ>_" [57]58) where "\<^bold>\<circ>A \<equiv> \<B>\<^sup>d A"
abbreviation op_ind::"\<sigma>\<Rightarrow>\<sigma>" ("\<bullet>_" [57]58) where "\<bullet>A \<equiv> \<^bold>\<midarrow>\<^bold>\<circ>A"
lemma op_det_def: "\<^bold>\<circ>a \<^bold>\<approx> a \<^bold>\<or> \<^bold>\<not>a" by (simp add: compl_def diff_def dual_def ineg_def join_def pB1)
lemma Prop1: "\<^bold>\<circ>A \<^bold>\<approx> \<C>\<^sup>f\<^sup>p A" by (metis dimp_def eq_ext' fp3)
lemma Prop2: "Op A \<longleftrightarrow> \<^bold>\<circ>\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<top>" by (metis dual_def dual_symm pB1 pI1 top_def compl_def diff_def)
lemma Prop3: "Op A \<longleftrightarrow> \<bullet>\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<bottom>" by (metis Op_Bzero dual_def dual_symm)
lemma Prop4: "Cl A \<longleftrightarrow> \<^bold>\<circ>A \<^bold>\<approx> \<^bold>\<top>" by (metis Prop1 dimp_def top_def)
lemma Prop5: "Cl A \<longleftrightarrow> \<bullet>A \<^bold>\<approx> \<^bold>\<bottom>" by (simp add: Prop4 bottom_def compl_def top_def)
text\<open>\noindent{Analogously as for LFIs, LFUs provide means for recovering the principle of excluded middle.}\<close>
lemma "[\<Gamma> \<^bold>\<turnstile> \<bullet>a, a \<^bold>\<or> \<^bold>\<not>a]" using IB_rel Int_br_def compl_def diff_def dual_def eq_ext' ineg_def join_def by fastforce
lemma "[\<Gamma>, \<^bold>\<circ>a \<^bold>\<turnstile> a \<^bold>\<or> \<^bold>\<not>a]" using dual_def pB1 unfolding conn by auto
lemma "TNDm(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "ECQ(\<^bold>\<not>)" by (simp add: ECQ_def bottom_def diff_def ineg_prop meet_def)
lemma "Der_3 \<D> \<Longrightarrow> LNC(\<^bold>\<not>)" using ineg_prop ECQ_def ID3 LNC_def dNOR_def unfolding conn by auto
lemma "\<DD> \<D> \<Longrightarrow> DNI(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<DD> \<D> \<Longrightarrow> DNE(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Der_1b \<D> \<Longrightarrow> CoPw(\<^bold>\<not>)" by (smt CoPw_def MONO_ADDIb PD1 compl_def ineg_def monI)
lemma "\<DD> \<D> \<Longrightarrow> CoP1(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<DD> \<D> \<Longrightarrow> CoP2(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<DD> \<D> \<Longrightarrow> CoP3(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<DD> \<D> \<Longrightarrow> DM3(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Der_1a \<D> \<Longrightarrow> DM4(\<^bold>\<not>)" unfolding Defs using ADDI_a_def ineg_prop compl_def diff_def join_def meet_def by auto
lemma "Der_3 \<D> \<Longrightarrow> nNor(\<^bold>\<not>)" by (simp add: NOR_def ineg_prop nNor_def bottom_def compl_def diff_def top_def)
lemma "nDNor(\<^bold>\<not>)" by (simp add: bottom_def diff_def ineg_prop nDNor_def top_def)
lemma "Der_1b \<D> \<Longrightarrow> MT0(\<^bold>\<not>)" unfolding Defs by (metis (mono_tags, hide_lams) CD1b Disj_I OpCldual PD1 bottom_def compl_def ineg_def meet_def top_def)
lemma "Der_1b \<D> \<Longrightarrow> Der_3 \<D> \<Longrightarrow> MT1(\<^bold>\<not>)" unfolding Defs by (metis (full_types) NOR_def PD1 bottom_def compl_def diff_def ineg_prop top_def)
lemma "\<DD> \<D> \<Longrightarrow> MT2(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<DD> \<D> \<Longrightarrow> MT3(\<^bold>\<not>)" nitpick oops (*countermodel*)
text\<open>\noindent{We show how all local contraposition variants (lCoP) can be recovered using the determinedness operator.
Observe that we can recover in the same way other (weaker) properties: CoP, MT and DNI/DNE (local \& global).}\<close>
lemma "\<DD> \<D> \<Longrightarrow> lCoPw(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma det_lcop1: "[\<^bold>\<circ>a, a \<^bold>\<rightarrow> b \<^bold>\<turnstile> \<^bold>\<not>b \<^bold>\<rightarrow> \<^bold>\<not>a]" using dual_def pI1 conn by auto
lemma "\<DD> \<D> \<Longrightarrow> lCoP1(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma det_lcop2: "[\<^bold>\<circ>a, a \<^bold>\<rightarrow> \<^bold>\<not>b \<^bold>\<turnstile> b \<^bold>\<rightarrow> \<^bold>\<not>a]" using dual_def pI1 conn by auto
lemma "\<DD> \<D> \<Longrightarrow> lCoP2(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma det_lcop3: "[\<^bold>\<circ>a, \<^bold>\<not>a \<^bold>\<rightarrow> b \<^bold>\<turnstile> \<^bold>\<not>b \<^bold>\<rightarrow> a]" using dual_def pI1 conn by auto
lemma "\<DD> \<D> \<Longrightarrow> lCoP3(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma det_lcop4: "[\<^bold>\<circ>a, \<^bold>\<not>a \<^bold>\<rightarrow> \<^bold>\<not>b \<^bold>\<turnstile> b \<^bold>\<rightarrow> a]" using dual_def pI1 conn by auto
text\<open>\noindent{Disjunctive syllogism (DS).}\<close>
lemma "DS1(\<^bold>\<rightarrow>)(\<^bold>\<not>)" by (simp add: DS1_def diff_def impl_def ineg_prop join_def)
lemma "\<DD> \<D> \<Longrightarrow> DS2(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma det_ds2: "[\<^bold>\<circ>a, \<^bold>\<not>a \<^bold>\<rightarrow> b \<^bold>\<turnstile> a \<^bold>\<or> b]" using pB1 dual_def conn by auto
end
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 \<open>Example application: Subintuitionistic and subminimal logics\<close>
text\<open>\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.}\<close>
text\<open>\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 "\<F>'"}.}\<close>
consts Q::"\<sigma>"
abbreviation "\<F>' \<equiv> \<lambda>X. Q"
abbreviation "\<I>' \<equiv> \<I>\<^sub>F \<F>'"
abbreviation "\<C>' \<equiv> \<C>\<^sub>F \<F>'"
abbreviation "\<B>' \<equiv> \<B>\<^sub>F \<F>'"
text\<open>\noindent{As defined, @{text "\<F>'"} (and its corresponding closure operation) satisfies several semantic conditions.}\<close>
lemma "Fr_1 \<F>' \<and> Fr_2 \<F>' \<and> Fr_4 \<F>'" by (simp add: Fr_1_def Fr_2_def Fr_4_def conn)
lemma "Cl_1 \<C>' \<and> Cl_2 \<C>' \<and> Cl_4 \<C>'" using ADDI_def CF2 IDEMb_def Cl_fr_def PC4 unfolding conn by auto
text\<open>\noindent{However Fr-3 is not valid. In fact, adding it by hand would collapse into classical logic (making all sets clopen).}\<close>
lemma "Fr_3 \<F>'" nitpick oops (*counterexample found*)
lemma "Cl_3 \<C>'" nitpick oops (*counterexample found*)
lemma "Fr_3 \<F>' \<Longrightarrow> \<forall>A. \<F>'(A) \<^bold>\<approx> \<^bold>\<bottom>" by (simp add: NOR_def)
text\<open>\noindent{In order to obtain a paracomplete logic not validating ECQ, we define negation as follows,}\<close>
abbreviation neg_IC::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<not>") where "\<^bold>\<not>A \<equiv> \<C>'(\<I>(\<^bold>\<midarrow>A))"
text\<open>\noindent{and observe that some plausible semantic properties obtain:}\<close>
lemma Q_def1: "\<forall>A. Q \<^bold>\<approx> \<^bold>\<not>A \<^bold>\<and> \<^bold>\<not>(\<^bold>\<not>A)" using Cl_fr_def IF2 dEXP_def conn by auto
lemma Q_def2: "Fr_1b \<F> \<Longrightarrow> \<forall>A. Q \<^bold>\<approx> \<^bold>\<not>(A \<^bold>\<or> \<^bold>\<not>A)" by (smt Cl_fr_def IF2 dEXP_def MONO_def monI conn)
lemma neg_Idef: "\<forall>A. \<^bold>\<not>A \<^bold>\<approx> \<I>(\<^bold>\<midarrow>A) \<^bold>\<or> Q" by (simp add: Cl_fr_def)
lemma neg_Cdef: "Fr_2 \<F> \<Longrightarrow> \<forall>A. \<^bold>\<not>A \<^bold>\<approx> \<C>(A) \<^bold>\<rightarrow> Q" using Cl_fr_def Fr_2_def Int_fr_def conn by auto
text\<open>\noindent{The negation so defined validates some properties corresponding to a (rather weak) paracomplete logic:}\<close>
lemma "\<FF> \<F> \<Longrightarrow> TND \<^bold>\<not>" nitpick oops (*counterexample found: negation is paracomplete*)
lemma "\<FF> \<F> \<Longrightarrow> TNDw \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> TNDm \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> ECQ \<^bold>\<not>" nitpick oops (*counterexample found: negation is paraconsistent...*)
lemma ECQw: "ECQw \<^bold>\<not>" using Cl_fr_def Disj_I ECQw_def unfolding conn by auto (*...but not 'boldly' paraconsistent*)
lemma ECQm: "ECQm \<^bold>\<not>" using Cl_fr_def Disj_I ECQm_def unfolding conn by auto
lemma "\<FF> \<F> \<Longrightarrow> LNC \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> DNI \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>" nitpick oops
lemma CoPw: "Fr_1b \<F> \<Longrightarrow> CoPw \<^bold>\<not>" using Cl_fr_def MONO_def monI unfolding Defs conn by smt
lemma "\<FF> \<F> \<Longrightarrow> CoP1 \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> CoP2 \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> CoP3 \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> XCoP \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> DM3 \<^bold>\<not>" nitpick oops
lemma DM4: "Fr_1a \<F> \<Longrightarrow> DM4 \<^bold>\<not>" using ADDI_a_def Cl_fr_def DM4_def IC1b IF1b dual_def unfolding conn by smt
lemma Nor: "Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> nNor \<^bold>\<not>" using Cl_fr_def nNor_I nNor_def unfolding conn by auto
lemma "\<FF> \<F> \<Longrightarrow> nDNor \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> lCoPw(\<^bold>\<rightarrow>) \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> lCoP1(\<^bold>\<rightarrow>) \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> lCoP2(\<^bold>\<rightarrow>) \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> lCoP3(\<^bold>\<rightarrow>) \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> DS1(\<^bold>\<rightarrow>) \<^bold>\<not>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> DS2(\<^bold>\<rightarrow>) \<^bold>\<not>" nitpick oops
text\<open>\noindent{Moreover, we cannot have both DNI and DNE without validating ECQ (thus losing paraconsistency).}\<close>
lemma "DNI \<^bold>\<not> \<and> DNE \<^bold>\<not> \<longrightarrow> ECQ \<^bold>\<not>" using DNE_def ECQ_def Int_fr_def neg_Idef unfolding conn by (metis (no_types, lifting))
text\<open>\noindent{However, we can have all of De Morgan laws while keeping (non-bold) paraconsistency.}\<close>
lemma "\<sim>ECQ \<^bold>\<not> \<and> DM1 \<^bold>\<not> \<and> DM2 \<^bold>\<not> \<and> DM3 \<^bold>\<not> \<and> DM4 \<^bold>\<not> \<and> \<FF> \<F>" nitpick[satisfy,card w=3] oops (*(weakly paraconsistent) model found*)
text\<open>\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). }\<close>
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (\<^bold>\<not>a \<^bold>\<Rightarrow> (a \<^bold>\<Rightarrow> b)) \<^bold>\<approx> \<^bold>\<top>" nitpick oops (*counterexample found*)
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (\<^bold>\<not>a \<^bold>\<rightarrow> (a \<^bold>\<rightarrow> b)) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a \<^bold>\<Rightarrow> b) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a \<^bold>\<rightarrow> b) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> (b \<^bold>\<or> \<^bold>\<not>b)) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<rightarrow> (b \<^bold>\<or> \<^bold>\<not>b)) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (a \<^bold>\<Rightarrow> \<^bold>\<not>a) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (a \<^bold>\<rightarrow> \<^bold>\<not>a) \<^bold>\<rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a) \<^bold>\<Rightarrow> b \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a) \<^bold>\<rightarrow> b \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. a \<^bold>\<Rightarrow> (b \<^bold>\<or> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. a \<^bold>\<rightarrow> (b \<^bold>\<or> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<leftrightarrow> b) \<^bold>\<Rightarrow> (\<^bold>\<not>a \<^bold>\<leftrightarrow> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<leftrightarrow> b) \<^bold>\<rightarrow> (\<^bold>\<not>a \<^bold>\<leftrightarrow> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> b) \<^bold>\<and> (a \<^bold>\<Rightarrow> \<^bold>\<not>b) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<rightarrow> b) \<^bold>\<and> (a \<^bold>\<rightarrow> \<^bold>\<not>b) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a \<^bold>\<Rightarrow> \<^bold>\<bottom>) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a \<^bold>\<rightarrow> \<^bold>\<bottom>) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a \<^bold>\<Rightarrow> \<^bold>\<not>(\<^bold>\<not>\<^bold>\<top>)) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a \<^bold>\<rightarrow> \<^bold>\<not>(\<^bold>\<not>\<^bold>\<top>)) \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. \<^bold>\<not>(\<^bold>\<not>(\<^bold>\<not>a)) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>" nitpick oops
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. \<^bold>\<not>(\<^bold>\<not>(\<^bold>\<not>a)) \<^bold>\<rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>" nitpick oops
text\<open>\noindent{The (weak) local contraposition axiom is indeed valid under appropriate conditions.}\<close>
lemma lCoPw: "Fr_1 \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> Fr_4 \<F> \<Longrightarrow> lCoPw(\<^bold>\<Rightarrow>) \<^bold>\<not>" proof -