TY - JOUR

T1 - A tree-sequent calculus for a natural predicate extension of visser's propositional logic

AU - Ishigaki, Ryo

AU - Kikuchi, Kentaro

PY - 2007/3/1

Y1 - 2007/3/1

N2 - We study predicate logic that is interpreted in Kripke models similarly to intuitionistic logic except that the accessibility relation of each model is not necessarily reflexive. Unlike in Ruitenburg's Basic Predicate Calculus, which is previous work on logic of this kind, the notion of formula in our system is the standard one in predicate logic. We give an axiomatization for this logic in the style of tree-sequent calculus (a special form of labelled sequent calculus) and prove its completeness with respect to the class of Kripke models.

AB - We study predicate logic that is interpreted in Kripke models similarly to intuitionistic logic except that the accessibility relation of each model is not necessarily reflexive. Unlike in Ruitenburg's Basic Predicate Calculus, which is previous work on logic of this kind, the notion of formula in our system is the standard one in predicate logic. We give an axiomatization for this logic in the style of tree-sequent calculus (a special form of labelled sequent calculus) and prove its completeness with respect to the class of Kripke models.

KW - Kripke models

KW - Predicate logic

KW - Tree-sequent calculus

KW - Visser's propositional logic

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

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

U2 - 10.1093/jigpal/jzm004

DO - 10.1093/jigpal/jzm004

M3 - Article

AN - SCOPUS:34447552417

VL - 15

SP - 149

EP - 164

JO - Logic Journal of the IGPL

JF - Logic Journal of the IGPL

SN - 1367-0751

IS - 2

ER -