##
Reports on Mathematical Logic

###
No. 33

Katsumi SASAKI:

FORMALIZATIONS FOR THE CONSEQUENCE RELATION OF VISSER'S PROPOSITIONAL
LOGIC
A b s t r a c t.
Visser's propositional logic ({\bf VPL}) 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 ($\supset E$) by
three other inference rules. Ardeshir [1] and [2]
gave sequent style systems for $\vdash_V$ by replacing the inference
rule ($\supset\ya$) 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.

Back to Main Menu