A proof-theoretic study of the correspondence of classical logic and modal logic

H. Kushida, Mitsuhiro Okada

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

Original languageEnglish
Pages (from-to)1403-1414
Number of pages12
JournalJournal of Symbolic Logic
Volume68
Issue number4
Publication statusPublished - 2003 Dec

Fingerprint

Classical Logic
Modal Logic
Correspondence
Predicate Logic
Quantifiers
Operator
Mint

ASJC Scopus subject areas

  • Logic

Cite this

A proof-theoretic study of the correspondence of classical logic and modal logic. / Kushida, H.; Okada, Mitsuhiro.

In: Journal of Symbolic Logic, Vol. 68, No. 4, 12.2003, p. 1403-1414.

Research output: Contribution to journalArticle

@article{a8f7bdb3b91a41e38109938b3fc2919e,
title = "A proof-theoretic study of the correspondence of classical logic and modal logic",
abstract = "It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.",
author = "H. Kushida and Mitsuhiro Okada",
year = "2003",
month = "12",
language = "English",
volume = "68",
pages = "1403--1414",
journal = "Journal of Symbolic Logic",
issn = "0022-4812",
publisher = "Association for Symbolic Logic",
number = "4",

}

TY - JOUR

T1 - A proof-theoretic study of the correspondence of classical logic and modal logic

AU - Kushida, H.

AU - Okada, Mitsuhiro

PY - 2003/12

Y1 - 2003/12

N2 - It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

AB - It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

UR - http://www.scopus.com/inward/record.url?scp=0347592509&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0347592509&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0347592509

VL - 68

SP - 1403

EP - 1414

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

SN - 0022-4812

IS - 4

ER -