معناشناسي و توقف حساب هاي رشته اي براي دو منطق وجهي شهودي

چكيده انگليسي :

Semantics and Terminating sequent calculi for two intuitionistic modal logics Narges Kimiyavi Moghodam n kimiyavi@math iut ac ir October 12 2020 Master of Science Thesis in Farsi Departement of Mathematical Sciences Isfahan University of Technology Isfahan 84156 8311 IranSupervisor Dr Mojtaba Aghaei aghaei@cc iut ac irAdvisor Mr Mohsen khani mohsen khani@cc iut ac ir2000 MSC 03F05 03F55 03B25 03B45Keywords intuitionistic modal logic sequent calculus Abstract This M Sc thesis is based on the following papers Rosalie Iemhoff Terminating sequent calculi for two intutionistic modal logics Utrecht University Janskerkof 13 3512 BL Utrecht The Netherlands Possible world semantics underlies many of the applications of modal logic in computer science and philosophy Thestandard theory arises from interpreting the semantic definitions in the ordinary meta theory of informal classicalmathematics Classical modal logics are classical in the sense that all are built on top of ordinary classical logic Similarly intu itionistic modal logics are modal logics whose underlying logic is intuitionistic The cut elimination theorem or Gentzen s Hauptsatz is the central result establishing the significance of the sequentcalculus It was originally proved by Gerhard Gentzen in his landmark 1934 paper Investigations in Logical De duction for the systems LJ and LK formalising intuitionistic and classical logic respectively The cut eliminationtheorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also pos sesses a cut free proof that is a proof that does not make use of the cut rule But they are admissible in it standard sequent calculi for the classical propositional logic corresponding calculus tothe intuitionistic propositional by limiting the right side of the sequents to the maximum of a formula But it s nottrue in the well known calculus G3cp There are no structural rules in this calculus and there are admissible in it but limiting the right side of sequents to the maximum of one formula will allow some of the other rules to not beadmissible These fault are solved by slight change in the formulation of some rules and the corresponding sequentcalculus G3cp for intuitionistic logic is achieved without the structural rules But the most important property ofclassical calculus is lost in it The search for proof in the G3ip is no longer stopped The lack of termination makesG3ip unfit for certain proof theoretic arguments about IPC such as the proof that IPC has uniform interpolation In 11 this theorem is proved using a terminating sequent calculus which is developed independently in 4 5 7 Thiscalculus is derived from the following 13 is called G4ip which are obtained from the four implication rules insteadof the left implication in G3ip in this thesis based on 9 terminating calculi for modal logics K and KD without operator proposed that they are derived from the development of G4ip and structural and cut rules are admissiblein them It is proven that these calculi are equivalent to other standard accounts of these logics based on G3ip andstructural rules are admissible in them In this thesis it has been shown that for X K KD the indced calculus G4iX introduced is a terminatingcut free sequent calculus for the intuitionistic modal logic LG3iX in which the structural rules are admissible Theresult is obtained via a syntactic proof of the equivalence between G4iX and the calculus G3iX

كيمياوي مقدم، نرگس

معناشناسي و توقف حساب هاي رشته اي براي دو منطق وجهي شهودي

منطق وجهي شهودي , حساب رشته اي