Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Formalizations for the consequence relation of visser's propositional logic

Sasaki K.

Reports on Mathematical Logic

1999

No. 33

65-78

Visser's propositional logic (VPL) was first considered in Visser [5] as the propositional logic embedded into the model logic K4 by Godel's translation. He gave a natural dedudtion system -v for the consequence relation of VPL. An essential difference from the consequence relation () of intuitionistic propositional logic is {a,a ) b} Hv b while {a,a )b} -1 b. In other words, in -v , modus ponens does not hold in general. So, we may well say that systems for the consequence relation of VPL are obtained from the systems for -1 by replacing the inference rule, which corresponds to modus ponens, by other inference rules. For instance, Visser's system -v was obtained from Gentzen's natural deduction system -N J by replacing implication elimination rule [ ) E} by three other inference rules. Ardeshir [1] and [2] gave sequent style systems for -v by replacing the inference rule [ ) ->] in Gentzen's sequent system LJ by other inference rules. However, it seems difficult to give a finite Hilbert style system for the consequence relation of VPL because modus pones in Hilbert style system for -1 has the role of translating axioms into inference rules, and so, we have to find another inference rule having the same role in -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 for -1 has. Using the restricted modus ponens and adjunction, we give a formalization for -v, and at the same time we show that -v can not be formalized by any systems with a restricted modus ponens as only one inference rule.