Abstract

Visser's propositional logic was first considered in Visser [5] as the propositional logic embedded into the modal logic {\bf K4} by G\"odel's translation. He gave a natural deduction system $\vdash_V$ for the consequence relation of {\bf VPL}. An essential difference from the consequence relation $\vdash_I$ of intuitionistic propositional logic is $\{a,a\supset b\}\not \vdash_Vb$ while $\{ a,a\supset b\}\vdash_Ib$. In other words, in $\vdash_V$, modus ponens does not hold in general. So, we may well say that systems for the consequence relation of {\bf VPL} are obtained from the systems for $\vdash_I$ by replacing the inference rule, which corresponds to modus ponens, by other inference rules. For instance, Visser's system $ \vdash_V$ was obtained from Gentzen's natural deduction system $\vdash_{ NJ}$ by replacing implication elimination rule by three other inference rules. Ardeshir [1] and [2] gave sequent style systems for $\vdash_V$ by replacing the inference rule in Gentzen's sequent system {\bf LJ} by other inference rules. However, it seems difficult to give a finite Hilbert style system for the consequence relation of {\bf VPL} because modus pones in Hilbert style system for $\vdash_I$ has the role of translating axioms into inference rules, and so, we have to find another inference rule having the same role in $\vdash_V$. This problem was raised in Suzuki, Wolter and Zakharyaschev [4]. Here we introduce a restricted modus ponens, which mostly has the same role as modus ponens in Hilbert style system for $\vdash_I$ has. Using the restricted modus ponens and adjunction, we give a formalization for $ \vdash_V$, and at the same time we show that $\vdash_V$ can not be formalized by any systems with a restricted modus ponens as only one inference rule.