Tableaux and Hypersequents for Modal and Justification Logics
Item
-
Title
-
Tableaux and Hypersequents for Modal and Justification Logics
-
Identifier
-
d_2009_2013:3454d03ab814:11482
-
identifier
-
11932
-
Creator
-
Kurokawa, Hidenori,
-
Contributor
-
Sergei Artemov
-
Date
-
2012
-
Language
-
English
-
Publisher
-
City University of New York.
-
Subject
-
Logic | Philosophy | hypersequent | justification logic | modal logic | tableau
-
Abstract
-
In this thesis, we discuss both philosophical and technical issues on proof theory of modal logic and justification logic.;In Chapter 2, we present a view of the foundations of logic, aiming for giving a view of various non-classical logics (called a "structural-reflective view of logic") and answering the question "are modal operators logical constants?" We present a method of introducing logical constants in Gentzen-style sequent calculi, based on abstract consequence relations. We propose a synthesis of Avron's, Dosen's, and Sambin et al's methods of introducing logical constants as positive criteria for a logical constant. In particular, we extend their methods to a certain class of modal logics by adopting the framework of hypersequent calculi and argue that modal operators in these logics are indeed logical constants according to our criterion. In addition, we discuss philosophical repercussions of the method, such as the significance of cut-elimination, the connection of the view with proof-theoretic semantics, Belnap's criteria of logical constant-hood, and the problem of what a good proof system is.;In Chapter 3, we present hypersequent calculi for some of the strict implication logics and modal logics that are introduced in Chapter 1 and related logics. We show the cut-elimination theorem for these logics and proof-theoretically show correctness and faithfulness of modal embeddings of their superintuitionistic counterparts into these logics.;In Chapter 4, we discuss another application of hypersequent calculi to modal logic. In this chapter, we consider logics that combine Artemov's justification logic and traditional modal logics. We formulate combinations of the logic of proofs LP and traditional model logics S4, GL, and Grz, which are studied from the viewpoint of (either formal or informal) "provability." To handle proof systems for these logics uniformly, we need a proof-theoretic framework that is more general than traditional Gentzen-style calculi. We first introduce prefixed tableau systems and then introduce hypersequent sequent calculi for these logics. We show cut-admissibility for all of these systems via a semantic method.
-
Type
-
dissertation
-
Source
-
2009_2013.csv
-
degree
-
Ph.D.
-
Program
-
Philosophy
