Cut Elimination in Hypersequent Calculi for S? Soudabe Farhadi February,?? ???? Ph.D. Thesis (in Farsi) Department of Mathematical Sciences Isfahan University of Technology, Isfahan ?????-????, Iran Supervisor: Dr. Mojtaba Aghaei Advisor: Dr. Ahmad Karimi ???? MSC: ??F??,??B?? . Keywords: cut-elimination, Hypersequent Calculi, Modal Logic. : This M. S.c. thesis is based on the following paper • Bednarska, K. and. Indrzejczak, A., “Hypersequent calculi for S?: The methods of cut elimination”.Logic and Logical Philosophy ?? (????), ???-?? In logic and philosophy, S? is one of five systems of modal logic proposed by Clarence Irving Lewis and Cooper Harold Langford in their ???? book Symbolic Logic. It is a normal modal logic, and one of the oldest systems of modal logic of any kind. S? can be axiomatize by adding to all (modal) instances of some system of ?, ..., n) is a sequent. The standard interpretation of the “|” symbol is usually disjunctive. A Hypersequent is true in a Kripke’s model if and only if one of its sequent is true in that model.That is, it’s true in each world in the model. The thesis is structured as follows. Chapter ? contains history and introduction of modal logic as well as some of elementary definitions. In chapter ?, we consider S?-basic facts and basic hypersequent calculus. Moreover we mention structural rules and logical rules for hypersequent caculus and we prove soundness lemma for it. The aim of this thesis is to compare proposed solutions, focusing on the proofs of cut elimination for six hypersequent calculi proposed for S? by Pottinger, Avron, Restall, Poggiolesi, Lahav, Kurokawa and revisited Pottinger’s system which proposed by Kaja Bednarska and Andrzej Indrzejczak in the main reference of the thesis. So in chapter ?, we introduce and compare these systems. Finally, in chapter ?, we prove cut elimination in detail for two systems Avron and revisited Pottinger’s system. In the appendix, we give deductions of several examples in each of the mentioned hypersequent calculi for S?. The contribution of the thesis, in addition of the examples given in the appendix, is to give lemmas and their proofs for a complete comparsion of the mentioned hypersequent systems for S?, and comparison of different versions of the cut rules. In addition the complete proofs of admissibility of the cut rules are given, and soundness of all the systems are proved. کلیدواژه فارسی
