Classifying material implications over minimal logic (Q2204373): Difference between revisions

Minimal logic (ML) can be formulated by deleting the EFQ-axiom from a standard axiomatization of intuitionistic logic (H) such as, e.g., that in [\textit J. Moschovakis, ``Intuitionistic logic'', in: E. N. Zalta (ed.), The Stanford encyclopedia of philosophy (Winter 2018). \url{https://plato.stanford.edu/archives/win2018/entries/logic-intuitionistic}]. The authors define the lattice of a series of ``paradoxes of material implication'' (in Lewis' sense -- cf. [\textit{C. I. Lewis} and \textit{C. H. Langford}, Symbolic logic. 2nd ed., corrected and unabridged republ. of the first ed. New York: Dover Publications, Inc (1959; Zbl 0087.00802)]) in the context of ML and w.r.t. eight prominent ones: \(\lnot \lnot \varphi \rightarrow \varphi \) (DNE), \( \lnot \varphi \rightarrow (\varphi \rightarrow \psi )\) (EFQ), \(((\varphi \rightarrow \psi )\rightarrow \varphi )\rightarrow \varphi \) (PP), \(\varphi \vee \lnot \varphi \) (LEM), \((\varphi \rightarrow \psi )\vee (\psi \rightarrow \varphi )\) (DGP), \(\lnot \varphi \rightarrow \lnot \lnot (\varphi \rightarrow \psi )\) (WT), \(\lnot \varphi \vee \lnot \lnot \varphi \) (WLEM) and \(\lnot (\varphi \rightarrow \psi )\rightarrow \lnot \lnot (\psi \rightarrow \varphi )\) (DGP\(^{\rightarrow }\)). All paradoxes considered are of course unprovable in ML, while only \( (\varphi \wedge \lnot \varphi )\rightarrow \psi \) (ECQ), \(\lnot \varphi \rightarrow (\varphi \rightarrow \psi )\) (EFQ) and some forms of the De Morgan laws (\(\lnot (\varphi \vee \psi )\leftrightarrow (\lnot \varphi \wedge \lnot \psi )\), \((\varphi \vee \psi )\rightarrow \lnot (\lnot \varphi \wedge \lnot \psi )\) and \((\varphi \wedge \psi )\rightarrow \lnot (\lnot \varphi \vee \lnot \psi )\)) are provable in H. The authors use Kripke semantics in order to show the uniqueness of the implications stated in the lattice referred to above. Nevertheless, I think that the same result can automatically be obtained by using \textit{J. Slaney}'s program MaGIC (cf. [``MaGIC: matrix generator for implication connectives'', \url{http://users.cecs.anu.edu.au/~jks/magic.html}]).