Syntactical investigations intoBI logic andBB′I logic

Abstract

In this note, we will study four implicational logicsB, BI, BB′ and BB′I. In [5], Martin and Meyer proved that a formula α is provable inBB′ if and only if α is provable inBB′I and α is not of the form of β » β. Though it gave a positive solution to theP - W problem, their method was semantical and not easy to grasp. We shall give a syntactical proof of the syntactical relation betweenBB′ andBB′I logics. It also includes a syntactical proof of Powers and Dwyer's theorem that is proved semantically in [5]. Moreover, we shall establish the same relation betweenB andBI logics asBB′ andBB′I logics. This relation seems to say thatB logic is meaningful, and so we think thatB logic is the weakest among meaningful logics. Therefore, by Theorem 1.1, our Gentzentype system forBI logic may be regarded as the most basic among all meaningful logics. It should be mentioned here that the first syntactical proof ofP - W problem is given by Misao Nagayama [6].