Syntactical investigations into BI logic and BB′I logic.

Autor: Komori, Yuichi
Zdroj: Studia Logica; Sep1994, Vol. 53 Issue 3, p397-416, 20p
Abstrakt: In this note, we will study four implicational logics B, BI, BB′ and BB′I. In [5], Martin and Meyer proved that a formula α is provable in BB′ if and only if α is provable in BB′I and α is not of the form of β » β. Though it gave a positive solution to the P - W problem, their method was semantical and not easy to grasp. We shall give a syntactical proof of the syntactical relation between BB′ and BB′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 between B and BI logics as BB′ and BB′I logics. This relation seems to say that B logic is meaningful, and so we think that B logic is the weakest among meaningful logics. Therefore, by Theorem 1.1, our Gentzentype system for BI logic may be regarded as the most basic among all meaningful logics. It should be mentioned here that the first syntactical proof of P - W problem is given by Misao Nagayama [6]. [ABSTRACT FROM AUTHOR]
Databáze: Complementary Index