Logic Journal of IGPL Advance Access published online on May 15, 2007
Logic Journal of IGPL, doi:10.1093/jigpal/jzm004
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
A Tree-Sequent Calculus for a Natural Predicate Extension of Visser's Propositional Logic
Department of Mathematical and Computing Sciences, Tokyo Institute of Technology, O-okayama, Meguro, Tokyo 152-8522, Japan. E-mail: ZAN35044{at}nifty.com
Research Institute of Electrical Communication, Tohuku University, Katahira, Aoba, Sendai 980-8577, Japan. E-mail: kentaro{at}nue.riec.tohoku.ac.jp
| Abstract |
|---|
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.
Key Words: Tree-sequent calculus predicate logic Visser's propositional logic Kripke models
Received for publication 8 September 2005.
![]()
CiteULike
Connotea
Del.icio.us What's this?