Syntactical investigations into \(BI\) logic and \(BB^ \prime I\) logic (Q1337604)

We will be concerned with four implicational logics. Parentheses will be omitted following the convention that \(\to\) associates to the right. For example \(\alpha_ 1\to \alpha_ 2\to \alpha_ 3\to \alpha_ 4\) denotes \(\alpha_ 1\to (\alpha_ 2\to (\alpha_ 3\to \alpha_ 4))\). The first logic, which we call \(B\), has an axiom scheme \((B)\) \((\beta\to \gamma)\to (\alpha\to \beta)\to \alpha\to \gamma\), and modus ponens as a rule. The second logic, \(BI\), has in addition to the axiom scheme and rule of \(B\) the axiom scheme \((I)\;\alpha\to \alpha\). The third logic, \(BB'\), has in addition to the axiom scheme and rule of \(B\) the axiom scheme \((B')\;(\alpha\to \beta)\to (\beta\to \gamma)\to \alpha\to \gamma\). The fourth logic, \(BB'I\), has in addition to the axiom schemes and rule of \(BB'\) the axiom scheme \(I\). Let \(L\) be any one of logics \(B\), \(BI\), \(BB'\) or \(BB'I\). We write \(L\vdash \alpha\) \((L\not\vdash \alpha)\) to mean that \(\alpha\) is (resp. is not) provable in the logic \(L\). We say that a formula \(\alpha\) is trivial (non-trivial) if \(\alpha\) is (resp. is not) of the form \(\beta\to \beta\). By the syntactical method (Gentzen-type formulation and cut elimination), we have the following three main theorems. Theorem \(B\): For any formula \(\alpha\), \(B\vdash \alpha\) if and only if \(BI\vdash \alpha\) and \(\alpha\) is non-trivial. Theorem \(BB'\): For any formula \(\alpha\), \(BB'\vdash \alpha\) if and only if \(BB'I\vdash \alpha\) and \(\alpha\) is non-trivial. Theorem. The four logics \(B\), \(BI\), \(BB'\) and \(BB'I\) are decidable. \textit{A. R. Anderson} and \textit{N. D. Belnap jun.} asked [Entailment: The logic of relevance and necessity. Vol. I (1975; Zbl 0323.02030), \S 8.11] whether \(\alpha\) and \(\beta\) are the same formula if both formulas \(\alpha\to \beta\) and \(\beta\to \alpha\) are provable in \(BB'I\). This question is known as P-W problem to which \textit{E. P. Martin} and \textit{R. K. Meyer} [J. Symbolic Logic 47, 869-887 (1982; Zbl 0498.03011)] have provided a positive solution by a semantical method. Theorem \(BB'\) gives a syntactical proof of a positive solution for the P-W problem.