An Infinity of Intuitionistic Connexive Logics

Abstract

We develop infinitely many intuitionistic connexive logics $\textsf{C}_{m,n}$ with $m> 0$ and $n\ge 0$ which are obtained from intuitionistic propositional logic by adding the negation sign $\sim$ which admits principles of connexive implication and ${\sim }^{2m+n}p \leftrightarrow {\sim }^n p$. We introduce $\langle m,n \rangle$-connexive logics and show that lattices of these connexive logics are isomorphic to lattices of superintuitionistic logics. Furthermore, we give cut-free G3-style sequent calculi for $\langle m,n \rangle$-connexive logics.

This work was supported by Chinese National Funding of Social Sciences (Grant no. 18ZDA033).

Appendices

Appendix

A Proof of Lemma 11

Proof

Assume $c(\varphi )=0$. Suppose $\varphi =p$. If $k<2m+n$, then ${\sim }^k p,\varGamma \Rightarrow {\sim }^k p$ is an instance of $\mathrm {(Id)}$. Suppose $k\ge 2m+n$. There exist $l\in [0,2m+n)$ and $r\ge 1$ with $k=2rm+l$. Obviously $\vdash {\sim }^l p,\varGamma \Rightarrow {\sim }^l p$. By $({{\sim }^{2m+n}}{\Rightarrow })$ and $({\Rightarrow }{{\sim }^{2m+n}})$, $\vdash {\sim }^k p,\varGamma \Rightarrow {\sim }^k p$. Suppose $\varphi =\bot$. If $k<2m+n$, then ${\sim }^k \bot ,\varGamma \Rightarrow {\sim }^k \bot$ is an instance of $\mathrm {(\bot \!\!\Rightarrow )}$. Suppose $k\ge 2m+n$. There exist $l\in [0,2m+n)$ and $r\ge 1$ with $k=2rm+l$. Then $\vdash {\sim }^l \bot ,\varGamma \Rightarrow {\sim }^l \bot$. By $({{\sim }^{2m+n}}{\Rightarrow })$ and $({\Rightarrow }{{\sim }^{2m+n}})$, $\vdash {\sim }^k\bot ,\varGamma \Rightarrow {\sim }^k\bot$. Assume $c(\varphi )>0$. Suppose $k\ge 2m+n$. There exist $l\in [0,2m+n)$ and $r\ge 1$ with $k=2rm+l$. Clearly $c({\sim }^l\varphi )<c({\sim }^k\varphi )$. By induction hypothesis, $\vdash {\sim }^l\varphi ,\varGamma \Rightarrow {\sim }^l\varphi$. By $({{\sim }^{2m+n}}{\Rightarrow })$ and $({\Rightarrow }{{\sim }^{2m+n}})$, $\vdash {\sim }^k\varphi ,\varGamma \Rightarrow {\sim }^k\varphi$. Suppose $k<2m+n$. Assume $\varphi =\varphi _1\wedge \varphi _2$. Let $\varphi ={\sim }^e(\varphi _1\wedge \varphi _2)$ with $e\in E[0,2m+n)$. Clearly $c({\sim }^e\varphi _1)<c({\sim }^e(\varphi _1\wedge \varphi _2))$ and $c({\sim }^e\varphi _2)<c({\sim }^e(\varphi _1\wedge \varphi _2))$. By induction hypothesis, $\vdash {\sim }^e\varphi _1,{\sim }^e\varphi _2,\varGamma$ $\Rightarrow {\sim }^e\varphi _1$ and $\vdash {\sim }^e\varphi _1,{\sim }^e\varphi _2,\varGamma \Rightarrow {\sim }^e\varphi _2$. By $({\Rightarrow }\wedge )$, $\vdash {\sim }^e\varphi _1,{\sim }^e\varphi _2,\varGamma \Rightarrow {\sim }^e(\varphi _1\wedge \varphi _2)$. By $(\wedge {\Rightarrow })$, $\vdash {\sim }^e(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow {\sim }^e(\varphi _1\wedge \varphi _2)$. Now let $\varphi ={\sim }^o(\varphi _1\wedge \varphi _2)$ with $o\in O[0,2m+n)$. Clearly, $c({\sim }^o\varphi _1)<c({\sim }^o(\varphi _1\wedge \varphi _2))$ and $c({\sim }^o\varphi _2)<c({\sim }^o(\varphi _1\wedge \varphi _2))$. By induction hypothesis, $\vdash {\sim }^o\varphi _1,\varGamma \Rightarrow {\sim }^o\varphi _1$ and $\vdash {\sim }^o\varphi _2,\varGamma \Rightarrow {\sim }^o\varphi _2$. By $({\Rightarrow }{\sim }{\wedge })$, $\vdash {\sim }^o\varphi _1,\varGamma \Rightarrow {\sim }^o(\varphi _1\wedge \varphi _2)$ and $\vdash {\sim }^o\varphi _2,\varGamma \Rightarrow {\sim }^o(\varphi _1\wedge \varphi _2)$. By $({\sim }{\wedge }{\Rightarrow })$, $\vdash {\sim }^o(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow {\sim }^o(\varphi _1\wedge \varphi _2)$. The case $\varphi =\varphi _1\vee \varphi _2$ is shown similarly. Suppose $\varphi = \varphi _1\rightarrow \varphi _2$. Clearly $c(\varphi _1)<c({\sim }^k (\varphi _1\rightarrow \varphi _2))$ and $c(\varphi _2)<c({\sim }^k (\varphi _1\rightarrow \varphi _2))$. By induction hypothesis, $\vdash \varphi _1,{\sim }^k (\varphi _1\rightarrow \varphi _2),\varGamma \Rightarrow \varphi _1$ and $\vdash \varphi _1,{\sim }^k \varphi _2,\varGamma$ $\Rightarrow {\sim }^k \varphi _2$. By $({\rightarrow }{\Rightarrow })$, $\vdash \varphi _1,{\sim }^k (\varphi _1\rightarrow \varphi _2),\varGamma \Rightarrow {\sim }^k \varphi _2$. By $({\Rightarrow }{\rightarrow })$, $\vdash {\sim }^k (\varphi _1\rightarrow \varphi _2),\varGamma \Rightarrow {\sim }^k (\varphi _1\rightarrow \varphi _2)$.    $\square$

B Proof of Lemma 14

Proof

Assume $\vdash _h\varphi ,\varphi ,\varGamma \Rightarrow \psi$. The proof proceeds by induction on h and subinduction on the complexity $c(\varphi )$. The case $h=0$ is trivial. Suppose $h>0$ and $\varphi ,\varphi ,\varGamma \Rightarrow \psi$ is obtained by a rule (R). Suppose $\varphi$ is not principal in (R). Then $\vdash \varphi ,\varGamma \Rightarrow \psi$ by induction hypothesis and (R). For example, let (R) be $\mathrm {(\Rightarrow \wedge )}$ with premisses $\vdash _{h-1}\varphi ,\varphi ,\varGamma \Rightarrow {\sim }^e\psi _1$ and $\vdash _{h-1}\varphi ,\varphi ,\varGamma \Rightarrow {\sim }^e\psi _2$, and conclusion $\vdash _{h}\varphi ,\varphi ,\varGamma \Rightarrow {\sim }^e(\psi _1\wedge \psi _2)$. By induction hypothesis, $\vdash _{h-1}\varphi ,\varGamma \Rightarrow {\sim }^e\psi _1$ and $\vdash _{h-1}\varphi ,\varGamma \Rightarrow {\sim }^e\psi _2$. By $\mathrm {(\Rightarrow \wedge )}$, $\vdash _h\varphi , \varGamma \Rightarrow {\sim }^e(\psi _1\wedge \psi _2)$. Other cases are shown similarly. Suppose $\varphi$ is principal in (R). Assume $\varphi ={\sim }^e(\varphi _1\wedge \varphi _2)$. Let (R) end with premiss $\vdash _{h-1}{\sim }^e\varphi _1,{\sim }^e\varphi _2,{\sim }^e(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow \psi$ and conclusion $\vdash _h{\sim }^e(\varphi _1\wedge \varphi _2),{\sim }^e(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow \psi$. By Lemma 13 (1), $\vdash _{h-1}{\sim }^e\varphi _1,{\sim }^e\varphi _2,{\sim }^e\varphi _1,{\sim }^e\varphi _2,\varGamma \Rightarrow \psi$. By induction hypothesis, $\vdash _{h-1}{\sim }^e\varphi _1,{\sim }^e\varphi _2,\varGamma \Rightarrow \psi$. By $({\wedge }{\Rightarrow })$, $\vdash _h{\sim }^e(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow \psi$. Assume $\varphi ={\sim }^o(\varphi _1\wedge \varphi _2)$. Let (R) end with premisses $\vdash {\sim }^o\varphi _1, {\sim }^o(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow \psi$ and $\vdash {\sim }^o\varphi _2, {\sim }^o(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow \psi$, and conclusion $\vdash _h{\sim }^o(\varphi _1\wedge \varphi _2),{\sim }^o(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow \psi$. By Lemma 13 (4), $\vdash {\sim }^o\varphi _1, {\sim }^o\varphi _1,\varGamma \Rightarrow \psi$ and $\vdash {\sim }^o\varphi _2, {\sim }^o\varphi _2,\varGamma \Rightarrow \psi$. By induction hypothesis, $\vdash {\sim }^o\varphi _1, \varGamma \Rightarrow \psi$ and $\vdash {\sim }^o\varphi _2,\varGamma \Rightarrow \psi$. By $({\sim }{\wedge }{\Rightarrow })$, $\vdash _h {\sim }^o(\varphi _1\wedge \varphi _2),\varGamma \Rightarrow \psi$. Assume $\varphi ={\sim }^e(\varphi _1\vee \varphi _2)$ or ${\sim }^o(\varphi _1\vee \varphi _2)$. The proof is similar to previous cases. Assume $\varphi ={\sim }^{2m+n}\chi$. Let (R) end with premiss $\vdash {\sim }^n\chi ,{\sim }^{2m+n}\chi ,\varGamma \Rightarrow \psi$ and conclusion $\vdash _{h}{\sim }^{2m+n}\chi ,{\sim }^{2m+n}\chi ,\varGamma \Rightarrow \psi$. By Lemma 13 (5), $\vdash {\sim }^n\chi ,{\sim }^n\chi ,\varGamma \Rightarrow \psi$. By induction hypothesis, $\vdash {\sim }^n\chi ,\varGamma \Rightarrow \psi$. By $({\sim }^{2m+n}{\Rightarrow })$, $\vdash _h{\sim }^{2m+n}\chi ,\varGamma \Rightarrow \psi$. Assume $\varphi ={\sim }^k(\varphi _1\rightarrow \varphi _2)$. Let (R) end with premisses $\vdash {\sim }^k(\varphi _1\rightarrow \varphi _2),{\sim }^k(\varphi _1\rightarrow \varphi _2),\varGamma \Rightarrow \varphi _1$ and $\vdash {\sim }^k\varphi _2,\varGamma \Rightarrow \psi$, and conclusion $\vdash _{h}{\sim }^k(\varphi _1\rightarrow \varphi _2),{\sim }^k(\varphi _1\rightarrow \varphi _2),\varGamma \Rightarrow \psi$. By induction hypothesis, $\vdash {\sim }^k(\varphi _1\rightarrow \varphi _2),\varGamma \Rightarrow \varphi _1$. By premiss and $\mathrm {(\rightarrow \Rightarrow )}$, $\vdash _h{\sim }^k(\varphi _1\rightarrow \varphi _2),\varGamma \Rightarrow \psi$.    $\square$

C Proof of Theorem 6

Proof

Assume $\vdash _h\varGamma \Rightarrow \varphi$ and $\vdash _j\varphi ,\varDelta \Rightarrow \psi$. We show $\vdash \varGamma ,\varDelta \Rightarrow \psi$ by simultaneous induction on the cut height $h+j$ and the complexity $c(\varphi )$. Assume $h=0$ or $j=0$. Suppose $h=0$. Suppose $\varGamma \Rightarrow \varphi$ is an instance of $\mathrm {(Id)}$. Then $\varphi \in \varGamma$. By $\vdash \varphi ,\varDelta \Rightarrow \psi$ and $\mathrm {(Wk)}$, $\vdash \varGamma ,\varDelta \Rightarrow \psi$. If $\bot \in \varGamma$, then $\vdash \varGamma ,\varDelta \Rightarrow \psi$. Suppose $j=0$. Let $\varphi ,\varDelta \Rightarrow \psi$ be an instance of $\mathrm {(Id)}$. If $\varphi =\psi$, by $\vdash \varGamma \Rightarrow \varphi$ and $(\textrm{Wk})$, $\vdash \varGamma ,\varDelta \Rightarrow \varphi$. Let $\varphi ,\varDelta \Rightarrow \psi$ be an instance of $\mathrm {(\bot )}$. If $\bot \in \varDelta$, then $\vdash \varGamma ,\varDelta \Rightarrow \psi$. If $\varphi =\bot$, by $\vdash \varGamma \Rightarrow \bot$, Lemma 15 and $(\textrm{Wk})$, $\vdash \varGamma ,\varDelta \Rightarrow \psi$. Now assume $h,j>0$. Let the premisses of $\mathrm {(Cut)}$ be obtained by the rules $\mathrm {(R1)}$ and $\mathrm {(R2)}$ respectively. Suppose $\varphi$ is not principal in $\mathrm {(R1)}$. Then $\mathrm {(R1)}$ is a left rule. We apply $\mathrm {(Cut)}$ to the premiss(es) of $\mathrm {(R1)}$ and $\varphi ,\varDelta \Rightarrow \psi$, and then apply $(\textrm{R1})$. Suppose $\varphi$ is not principal in $\mathrm {(R2)}$. We apply $\mathrm {(Cut)}$ to $\varGamma \Rightarrow \varphi$ and the premiss(es) of $\mathrm {(R2)}$, and then apply $\mathrm {(R2)}$. Suppose $\varphi$ is principal in both $\mathrm {(R1)}$ and $\mathrm {(R2)}$. The proof proceeds by induction on $c(\varphi )$. We have the following cases:

(1) $\varphi ={\sim }^e(\varphi _1\wedge \varphi _2)$ and the derivations end with

$$ \frac{\varGamma \Rightarrow {\sim }^e \varphi _1 \quad \varGamma \Rightarrow {\sim }^e \varphi _2}{\varGamma \Rightarrow {\sim }^e (\varphi _1\wedge \varphi _2)}{({\Rightarrow }\wedge )} \quad \frac{{\sim }^e \varphi _1,{\sim }^e \varphi _2,\varDelta \Rightarrow \psi }{{\sim }^e (\varphi _1\wedge \varphi _2),\varDelta \Rightarrow \psi }{(\wedge {\Rightarrow })} $$

By applying $\mathrm {(Cut)}$ to sequents with cut formula of less complexity, we have

(2) $\varphi ={\sim }^e (\varphi _1\vee \varphi _2)$ and the derivations end with

$$ \frac{\varGamma \Rightarrow {\sim }^e\varphi _i}{\varGamma \Rightarrow {\sim }^e (\varphi _1\vee \varphi _2)}{({\Rightarrow }{\vee })}{(i=1,2)} \quad \frac{{\sim }^e\varphi _1,{\sim }^e\varphi _2,\varDelta \Rightarrow \psi }{{\sim }^e (\varphi _1\vee \varphi _2),\varDelta \Rightarrow \psi }{({\vee }{\Rightarrow })} $$

By applying $\mathrm {(Cut)}$ to sequents with cut formula of less complexity, and by (Ctr), we obtain $\varGamma ,\varDelta \Rightarrow \psi$.

(3) $\varphi ={\sim }^o (\varphi _1\wedge \varphi _2)$ or ${\sim }^o (\varphi _1\vee \varphi _2)$. The proof is similar to (1) or (2).

(4) $\varphi ={\sim }^k (\varphi _1\rightarrow \varphi _2)$ and the derivations end with

$$ \frac{\varphi _1,\varGamma \Rightarrow {\sim }^k \varphi _2}{\varGamma \Rightarrow {\sim }^k (\varphi _1\rightarrow \varphi _2)} ~(\mathrm {\Rightarrow \rightarrow }) \quad \frac{{\sim }^k (\varphi _1\rightarrow \varphi _2),\varDelta \Rightarrow \varphi _1 \quad {\sim }^k \varphi _2,\varDelta \Rightarrow \psi }{{\sim }^k (\varphi _1\rightarrow \varphi _2),\varDelta \Rightarrow \psi }{({\rightarrow }{\Rightarrow })} $$

By applying $\mathrm {(Cut)}$ to sequents with cut formula of less complexity, we have $\vdash {\sim }^k (\varphi _1\rightarrow \varphi _2),\varGamma ,\varDelta ,\varDelta \Rightarrow \psi$. By $(\textrm{Ctr})$, $\vdash {\sim }^k (\varphi _1\rightarrow \varphi _2),\varGamma ,\varDelta \Rightarrow \psi$.

(5) $\varphi ={\sim }^{2m+n} \psi$ and the derivations end with

$$ \frac{\varGamma \Rightarrow {\sim }^{n} \psi }{\varGamma \Rightarrow {\sim }^{2m+n} \psi }{({\Rightarrow }{{\sim }^{2m+n}})} \quad \frac{{\sim }^{n} \psi ,\varDelta \Rightarrow \chi }{{\sim }^{2m+n} \psi ,\varDelta \Rightarrow \chi }{({{\sim }^{2m+n}}{\Rightarrow })} $$

By applying $\mathrm {(Cut)}$ to premisses, we get $\vdash \varGamma ,\varDelta \Rightarrow \chi$.    $\square$