Syntactical investigations intoBI logic andBB′I logic

Studia Logica 53 (3):397 - 416 (1994)
  Copy   BIBTEX


In this note, we will study four implicational logicsB, BI, BB and BBI. In [5], Martin and Meyer proved that a formula is provable inBB if and only if is provable inBBI 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 andBBI 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 andBBI 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].



    Upload a copy of this work     Papers currently archived: 93,031

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

39 (#421,117)

6 months
10 (#308,797)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

On Equational Completeness Theorems.Tommaso Moraschini - 2022 - Journal of Symbolic Logic 87 (4):1522-1575.
A lambda proof of the p-w theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
A note on Decision problems for Implicational Sequent Calculi.Norihiro Kamide - 2001 - Bulletin of the Section of Logic 30 (3):129-138.

Add more citations

References found in this work

Untersuchungen über das logische Schließen. I.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 35:176–210.
Logics without the contraction rule.Hiroakira Ono & Yuichi Komori - 1985 - Journal of Symbolic Logic 50 (1):169-201.
Untersuchungen über das logische Schließen. II.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 39:405–431.
Solution to the P − W problem.E. P. Martin & R. K. Meyer - 1982 - Journal of Symbolic Logic 47 (4):869-887.
Predicate logics without the structure rules.Yuichi Komori - 1986 - Studia Logica 45 (4):393 - 404.

View all 6 references / Add more references