Ren-June Wang

In this paper, we explore modal logics over FDE from the point of view of both the Australian plan models with the Routley star operator and the American plan models with four semantic values. We show that, in general, the Australian plan modal logics are weaker, although the addition of a frame condition allows us to prove an equivalence between the two approaches. We then consider different S5-type logics, using accessibility relations that are equivalence relations or universal relations, on the two different plans. We show that there are three different logics that result. Next, we provide sequent systems for all of the logics and show that two of the systems enjoy cut elimination. Then, we show soundness and completeness with respect to appropriate classes of models for all the logics. Finally, we discuss some features of the logics and close by highlighting two open problems.

In this paper a complete proper subclass of Hilbert-style S4 proofs, named non-circular, will be determined. This study originates from an investigation into the formal connection between S4, as Logic of Provability and Logic of Knowledge, and Artemov's innovative Logic of Proofs, LP, which later developed into Logic of Justification. The main result concerning the formal connection is the realization theorem , which states that S4 theorems are precisely the formulas which can be converted to LP theorems with proper justificational objects substituting for modal knowledge operators. We extend this result by showing that on the proof level, non-circular proofs are exactly the class of S4 proofs which can be realized to LP proofs. In turn, this study provides an alternative algorithm to achieve the realization theorem, and a novel logical system, called S4ΔS4Δ, is introduced, which, under an adequate interpretation, is worth studying for its own sake