### 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 language | English |
---|---|

Pages (from-to) | 1403-1414 |

Number of pages | 12 |

Journal | Journal of Symbolic Logic |

Volume | 68 |

Issue number | 4 |

Publication status | Published - 2003 Dec |

### Fingerprint

### ASJC Scopus subject areas

- Logic

### Cite this

*Journal of Symbolic Logic*,

*68*(4), 1403-1414.

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

Research output: Contribution to journal › Article

*Journal of Symbolic Logic*, vol. 68, no. 4, pp. 1403-1414.

}

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 -