{"id":7858,"date":"2025-01-19T01:35:05","date_gmt":"2025-01-18T17:35:05","guid":{"rendered":"http:\/\/tsinghualogic.net\/JRC\/?page_id=7858"},"modified":"2025-07-08T21:50:17","modified_gmt":"2025-07-08T13:50:17","slug":"proof-theory-of-modal-logic","status":"publish","type":"page","link":"http:\/\/tsinghualogic.net\/JRC\/proof-theory-of-modal-logic\/","title":{"rendered":"<strong><strong>Proof Theory of Modal Logic<\/strong><\/strong>"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"7858\" class=\"elementor elementor-7858\" data-elementor-settings=\"[]\">\n\t\t\t\t\t\t\t<div class=\"elementor-section-wrap\">\n\t\t\t\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-7875add elementor-section-content-middle elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"7875add\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-66 elementor-top-column elementor-element elementor-element-4ad20e1\" data-id=\"4ad20e1\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-27b38d0 elementor-widget elementor-widget-text-editor\" data-id=\"27b38d0\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<style>\/*! elementor - v3.5.6 - 28-02-2022 *\/\n.elementor-widget-text-editor.elementor-drop-cap-view-stacked .elementor-drop-cap{background-color:#818a91;color:#fff}.elementor-widget-text-editor.elementor-drop-cap-view-framed .elementor-drop-cap{color:#818a91;border:3px solid;background-color:transparent}.elementor-widget-text-editor:not(.elementor-drop-cap-view-default) .elementor-drop-cap{margin-top:8px}.elementor-widget-text-editor:not(.elementor-drop-cap-view-default) .elementor-drop-cap-letter{width:1em;height:1em}.elementor-widget-text-editor .elementor-drop-cap{float:left;text-align:center;line-height:1;font-size:50px}.elementor-widget-text-editor .elementor-drop-cap-letter{display:inline-block}<\/style>\t\t\t\t<ul><li><strong>Time:<\/strong> 09:50 AM-12:15 AM, July 14<sup>th<\/sup>\u00a0-18<sup>th<\/sup><\/li><li><strong>Location:<\/strong> Room 5105, Teaching Building No. 5<\/li><li><strong>Lecturer:<\/strong> Marianna Girlando (ILLC, University of Amsterdam)<\/li><li><strong>Teaching Assistants:<\/strong><br \/><p style=\"font-weight: 400;\">Sisi Yang (\u6768\u601d\u601d,yangss23@mails.tsinghua.edu.cn)<\/p><p style=\"font-weight: 400;\">Xin Li (\u674e\u946b, lixin24@mails.tsinghua.edu.cn)<\/p><\/li><li><strong>Course Webpage<\/strong>: <a href=\"https:\/\/marianna-girlando.github.io\/marianna-girlando.TOSS2025\/\">Proof theory of modal logic<\/a>. \u00a0This webpage contains the slides, handouts and homeowork assignments for the course Proof Theory of Modal Logic.<\/li><\/ul><ul><li><strong>A WeChat group has been created for announcements, room changes, and social events. If you haven&#8217;t received invitation, \u00a0please contact the TAs.\u00a0<\/strong><\/li><\/ul>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t<div class=\"elementor-column elementor-col-33 elementor-top-column elementor-element elementor-element-7329b7b\" data-id=\"7329b7b\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-a985635 elementor-widget elementor-widget-text-editor\" data-id=\"a985635\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p><img decoding=\"async\" loading=\"lazy\" class=\"aligncenter wp-image-7860 \" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/profile2-scaled.jpeg\" alt=\"\" width=\"362\" height=\"265\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/profile2-scaled.jpeg 2560w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/profile2-200x146.jpeg 200w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/profile2-768x562.jpeg 768w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/profile2-1536x1123.jpeg 1536w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/profile2-2048x1497.jpeg 2048w\" sizes=\"(max-width: 362px) 100vw, 362px\" \/><\/p><p style=\"text-align: center;\"><a href=\"https:\/\/www.mariannagirlando.com\/\">Marianna Girlando<\/a><\/p>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-b791bb5 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"b791bb5\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-07a3582\" data-id=\"07a3582\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-5cd2d04 elementor-widget elementor-widget-heading\" data-id=\"5cd2d04\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<style>\/*! elementor - v3.5.6 - 28-02-2022 *\/\n.elementor-heading-title{padding:0;margin:0;line-height:1}.elementor-widget-heading .elementor-heading-title[class*=elementor-size-]>a{color:inherit;font-size:inherit;line-height:inherit}.elementor-widget-heading .elementor-heading-title.elementor-size-small{font-size:15px}.elementor-widget-heading .elementor-heading-title.elementor-size-medium{font-size:19px}.elementor-widget-heading .elementor-heading-title.elementor-size-large{font-size:29px}.elementor-widget-heading .elementor-heading-title.elementor-size-xl{font-size:39px}.elementor-widget-heading .elementor-heading-title.elementor-size-xxl{font-size:59px}<\/style><h3 class=\"elementor-heading-title elementor-size-default\">Course Description<\/h3>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-0c24005 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"0c24005\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-6c3ed37\" data-id=\"6c3ed37\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-953db1a elementor-widget elementor-widget-text-editor\" data-id=\"953db1a\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p>While proof systems for classical and intuitionistic logic can be defined using sequent calculus, the Gentzen-style formalism does not readily extend to the case of modal logic. And indeed, Gentzen-style sequents fail to meet basic requirements in the case of several modal logics: for instance, no cut-free sequent calculus is known for logic S5. In order to overcome these difficulties, various proof systems extending Gentzen\u2019s sequent calculus have been introduced. Namely, labelled calculi extend the language of the calculi with semantic information, while structured calculi, such as hypersequents or nested sequents, employ additional structural connectives.<\/p><p>In this course we will introduce labelled and structured proof systems and illustrate their main properties, including cut-freeness and modularity. Other than normal modal logics, we will discuss logics with neighbourhood semantics, such as conditional logics, and intuitionistic modal logics. We will showcase how labelled and structured calculi are suitable to obtain decision procedures for these logics. To conclude, we will compare the various proof systems by defining formal translations allowing to convert proofs from one formalism to another.<\/p>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-8172927 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"8172927\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-d814efd\" data-id=\"d814efd\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-37d4d90 elementor-widget elementor-widget-heading\" data-id=\"37d4d90\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h3 class=\"elementor-heading-title elementor-size-default\">Background Knowledge<\/h3>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-180b2da elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"180b2da\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-a6c88fd\" data-id=\"a6c88fd\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-5fb01a5 elementor-widget elementor-widget-text-editor\" data-id=\"5fb01a5\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<p style=\"text-align: left;\">The course assumes some basic familiarity with modal logic and with sequent calculus for classical propositional logic. The main proof-theoretic notions used in the course will be covered in the first lecture.<\/p>\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-14e1a3c elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"14e1a3c\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-ec80e5f\" data-id=\"ec80e5f\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap\">\n\t\t\t\t\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>Time: 09:50 AM-12:15 AM, July 14th\u00a0-18th Location: Room [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7858"}],"collection":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/comments?post=7858"}],"version-history":[{"count":13,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7858\/revisions"}],"predecessor-version":[{"id":8209,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7858\/revisions\/8209"}],"wp:attachment":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/media?parent=7858"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}