{"id":7732,"date":"2024-12-14T22:19:48","date_gmt":"2024-12-14T14:19:48","guid":{"rendered":"http:\/\/tsinghualogic.net\/JRC\/?page_id=7732"},"modified":"2024-12-14T23:51:46","modified_gmt":"2024-12-14T15:51:46","slug":"the-15th-tsinghua-logic-colloquium","status":"publish","type":"page","link":"http:\/\/tsinghualogic.net\/JRC\/the-15th-tsinghua-logic-colloquium\/","title":{"rendered":"The 15th Tsinghua Logic Colloquium"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"7732\" class=\"elementor elementor-7732\" 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-3e0106a4 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"3e0106a4\" 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-7cc8431b\" data-id=\"7cc8431b\" 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-3cc8d286 elementor-widget elementor-widget-text-editor\" data-id=\"3cc8d286\" 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<p><!-- wp:cover {\"url\":\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/12.19-1-scaled.jpg\",\"id\":7734,\"dimRatio\":50,\"isDark\":false,\"align\":\"wide\"} --><\/p>\n<div class=\"wp-block-cover alignwide is-light\"><p><span aria-hidden=\"true\" class=\"wp-block-cover__background has-background-dim\"><\/span><img decoding=\"async\" loading=\"lazy\" width=\"2560\" height=\"1607\" class=\"wp-block-cover__image-background wp-image-7734\" alt=\"\" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/12.19-1-scaled.jpg\" data-object-fit=\"cover\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/12.19-1-scaled.jpg 2560w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/12.19-1-200x126.jpg 200w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/12.19-1-768x482.jpg 768w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/12.19-1-1536x964.jpg 1536w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/12.19-1-2048x1286.jpg 2048w\" sizes=\"(max-width: 2560px) 100vw, 2560px\" \/><\/p>\n<div class=\"wp-block-cover__inner-container\"><p><!-- wp:paragraph {\"align\":\"center\",\"placeholder\":\"\u7f16\u5199\u6807\u9898\u2026\",\"style\":{\"typography\":{\"fontStyle\":\"normal\",\"fontWeight\":\"600\"}},\"textColor\":\"white\",\"fontSize\":\"x-large\"} --><\/p>\n<p class=\"has-text-align-center has-white-color has-text-color has-x-large-font-size\" style=\"font-style:normal;font-weight:600\">&nbsp;Theoretical Topics on Formal Systems&nbsp;<\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:paragraph {\"align\":\"center\",\"textColor\":\"white\",\"fontSize\":\"medium\"} --><\/p>\n<p class=\"has-text-align-center has-white-color has-text-color has-medium-font-size\">December 19, 2024, Beijing, China&nbsp;<\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:paragraph {\"align\":\"center\",\"textColor\":\"white\",\"fontSize\":\"medium\"} --><\/p>\n<p class=\"has-text-align-center has-white-color has-text-color has-medium-font-size\">Tsinghua University<\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p><!-- \/wp:paragraph --><\/p><\/div>\n<\/div>\n<p><!-- \/wp:cover --><\/p>\n<p><!-- wp:columns --><\/p>\n<div class=\"wp-block-columns\"><p><br><\/p><div class=\"wp-block-column\"><ul>\n<p><!-- \/wp:list-item --><\/p><\/ul>\n<p><!-- \/wp:list --><\/p><\/div>\n<p><!-- \/wp:column --><\/p><\/div>\n<p><!-- \/wp:columns --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p><!-- \/wp:paragraph --><\/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-152fea8 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"152fea8\" 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-e01b072\" data-id=\"e01b072\" 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-f500d12 elementor-widget elementor-widget-text-editor\" data-id=\"f500d12\" 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<ul>\n<li><strong>Time<\/strong>: 13:00-17:30, December 19, 2024<\/li>\n<li><strong>Venue<\/strong>: Room 329, School of Humanities, Tsinghua University.<\/li>\n<\/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\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-5487594 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"5487594\" 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-c095207\" data-id=\"c095207\" 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-20c78f5 elementor-widget-divider--view-line elementor-widget elementor-widget-divider\" data-id=\"20c78f5\" data-element_type=\"widget\" data-widget_type=\"divider.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-divider{--divider-border-style:none;--divider-border-width:1px;--divider-color:#2c2c2c;--divider-icon-size:20px;--divider-element-spacing:10px;--divider-pattern-height:24px;--divider-pattern-size:20px;--divider-pattern-url:none;--divider-pattern-repeat:repeat-x}.elementor-widget-divider .elementor-divider{display:-webkit-box;display:-ms-flexbox;display:flex}.elementor-widget-divider .elementor-divider__text{font-size:15px;line-height:1;max-width:95%}.elementor-widget-divider .elementor-divider__element{margin:0 var(--divider-element-spacing);-ms-flex-negative:0;flex-shrink:0}.elementor-widget-divider .elementor-icon{font-size:var(--divider-icon-size)}.elementor-widget-divider .elementor-divider-separator{display:-webkit-box;display:-ms-flexbox;display:flex;margin:0;direction:ltr}.elementor-widget-divider--view-line_icon .elementor-divider-separator,.elementor-widget-divider--view-line_text .elementor-divider-separator{-webkit-box-align:center;-ms-flex-align:center;align-items:center}.elementor-widget-divider--view-line_icon .elementor-divider-separator:after,.elementor-widget-divider--view-line_icon .elementor-divider-separator:before,.elementor-widget-divider--view-line_text .elementor-divider-separator:after,.elementor-widget-divider--view-line_text .elementor-divider-separator:before{display:block;content:\"\";border-bottom:0;-webkit-box-flex:1;-ms-flex-positive:1;flex-grow:1;border-top:var(--divider-border-width) var(--divider-border-style) var(--divider-color)}.elementor-widget-divider--element-align-left .elementor-divider .elementor-divider-separator>.elementor-divider__svg:first-of-type{-webkit-box-flex:0;-ms-flex-positive:0;flex-grow:0;-ms-flex-negative:100;flex-shrink:100}.elementor-widget-divider--element-align-left .elementor-divider-separator:before{content:none}.elementor-widget-divider--element-align-left .elementor-divider__element{margin-left:0}.elementor-widget-divider--element-align-right .elementor-divider .elementor-divider-separator>.elementor-divider__svg:last-of-type{-webkit-box-flex:0;-ms-flex-positive:0;flex-grow:0;-ms-flex-negative:100;flex-shrink:100}.elementor-widget-divider--element-align-right .elementor-divider-separator:after{content:none}.elementor-widget-divider--element-align-right .elementor-divider__element{margin-right:0}.elementor-widget-divider:not(.elementor-widget-divider--view-line_text):not(.elementor-widget-divider--view-line_icon) .elementor-divider-separator{border-top:var(--divider-border-width) var(--divider-border-style) var(--divider-color)}.elementor-widget-divider--separator-type-pattern{--divider-border-style:none}.elementor-widget-divider--separator-type-pattern.elementor-widget-divider--view-line .elementor-divider-separator,.elementor-widget-divider--separator-type-pattern:not(.elementor-widget-divider--view-line) .elementor-divider-separator:after,.elementor-widget-divider--separator-type-pattern:not(.elementor-widget-divider--view-line) .elementor-divider-separator:before,.elementor-widget-divider--separator-type-pattern:not([class*=elementor-widget-divider--view]) .elementor-divider-separator{width:100%;min-height:var(--divider-pattern-height);-webkit-mask-size:var(--divider-pattern-size) 100%;mask-size:var(--divider-pattern-size) 100%;-webkit-mask-repeat:var(--divider-pattern-repeat);mask-repeat:var(--divider-pattern-repeat);background-color:var(--divider-color);-webkit-mask-image:var(--divider-pattern-url);mask-image:var(--divider-pattern-url)}.elementor-widget-divider--no-spacing{--divider-pattern-size:auto}.elementor-widget-divider--bg-round{--divider-pattern-repeat:round}.rtl .elementor-widget-divider .elementor-divider__text{direction:rtl}<\/style>\t\t<div class=\"elementor-divider\">\n\t\t\t<span class=\"elementor-divider-separator\">\n\t\t\t\t\t\t<\/span>\n\t\t<\/div>\n\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-0f38236 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"0f38236\" 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-755e2d5\" data-id=\"755e2d5\" 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-f44ee6e elementor-widget elementor-widget-heading\" data-id=\"f44ee6e\" 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><h2 class=\"elementor-heading-title elementor-size-default\">Program<\/h2>\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-dbd18ea elementor-section-content-middle elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"dbd18ea\" 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-33 elementor-top-column elementor-element elementor-element-1e4c979\" data-id=\"1e4c979\" 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-c3cbe71 elementor-widget elementor-widget-image\" data-id=\"c3cbe71\" data-element_type=\"widget\" data-widget_type=\"image.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-image{text-align:center}.elementor-widget-image a{display:inline-block}.elementor-widget-image a img[src$=\".svg\"]{width:48px}.elementor-widget-image img{vertical-align:middle;display:inline-block}<\/style>\t\t\t\t\t\t\t\t\t<figure class=\"wp-caption\">\n\t\t\t\t\t\t\t\t\t\t<img decoding=\"async\" width=\"200\" height=\"200\" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/s200_rick.sommer.jpeg\" class=\"attachment-large size-large\" alt=\"\" loading=\"lazy\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/s200_rick.sommer.jpeg 200w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/s200_rick.sommer-80x80.jpeg 80w\" sizes=\"(max-width: 200px) 100vw, 200px\" \/>\t\t\t\t\t\t\t\t\t\t\t<figcaption class=\"widget-image-caption wp-caption-text\">Rick Sommer (Stanford University, USA)<\/figcaption>\n\t\t\t\t\t\t\t\t\t\t<\/figure>\n\t\t\t\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-66 elementor-top-column elementor-element elementor-element-54e533c\" data-id=\"54e533c\" 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-19d5a25 elementor-widget elementor-widget-toggle\" data-id=\"19d5a25\" data-element_type=\"widget\" data-widget_type=\"toggle.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-toggle{text-align:left}.elementor-toggle .elementor-tab-title{font-weight:700;line-height:1;margin:0;padding:15px;border-bottom:1px solid #d4d4d4;cursor:pointer;outline:none}.elementor-toggle .elementor-tab-title .elementor-toggle-icon{display:inline-block;width:1em}.elementor-toggle .elementor-tab-title .elementor-toggle-icon svg{-webkit-margin-start:-5px;margin-inline-start:-5px;width:1em;height:1em}.elementor-toggle .elementor-tab-title .elementor-toggle-icon.elementor-toggle-icon-right{float:right;text-align:right}.elementor-toggle .elementor-tab-title .elementor-toggle-icon.elementor-toggle-icon-left{float:left;text-align:left}.elementor-toggle .elementor-tab-title .elementor-toggle-icon .elementor-toggle-icon-closed{display:block}.elementor-toggle .elementor-tab-title .elementor-toggle-icon .elementor-toggle-icon-opened{display:none}.elementor-toggle .elementor-tab-title.elementor-active{border-bottom:none}.elementor-toggle .elementor-tab-title.elementor-active .elementor-toggle-icon-closed{display:none}.elementor-toggle .elementor-tab-title.elementor-active .elementor-toggle-icon-opened{display:block}.elementor-toggle .elementor-tab-content{padding:15px;border-bottom:1px solid #d4d4d4;display:none}@media (max-width:767px){.elementor-toggle .elementor-tab-title{padding:12px}.elementor-toggle .elementor-tab-content{padding:12px 10px}}<\/style>\t\t<div class=\"elementor-toggle\" role=\"tablist\">\n\t\t\t\t\t\t\t<div class=\"elementor-toggle-item\">\n\t\t\t\t\t<div id=\"elementor-tab-title-2701\" class=\"elementor-tab-title\" data-tab=\"1\" role=\"tab\" aria-controls=\"elementor-tab-content-2701\" aria-expanded=\"false\">\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon elementor-toggle-icon-left\" aria-hidden=\"true\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-closed\"><i class=\"fas fa-caret-right\"><\/i><\/span>\n\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-opened\"><i class=\"elementor-toggle-icon-opened fas fa-caret-up\"><\/i><\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t<a href=\"\" class=\"elementor-toggle-title\">Iterating reflection, fast growing functions, and transfinite induction 13:00-14:20\u00a0<\/a>\n\t\t\t\t\t<\/div>\n\n\t\t\t\t\t<div id=\"elementor-tab-content-2701\" class=\"elementor-tab-content elementor-clearfix\" data-tab=\"1\" role=\"tabpanel\" aria-labelledby=\"elementor-tab-title-2701\"><p>Abstract: In the context of subsystems and extensions of Peano Arithmetic (PA), this talk will explore connections between consistency, computational power, and generalizations of induction axioms. In particular, we begin with a base theory, such as Primitive Recursive Arithmetic (PRA) or Elementary Function Arithmetic (EFA), and we consider hierarchies generated from the base theory in three different ways: (1) extending theories via transfinite iterations of consistency or reflection principles, (2) adding statements of totality of fast-growing functions obtained by transfinite recursion, and (3) including axioms of transfinite induction for recursive ordinals. We will see that these three hierarchies align in surprising ways. This talk will describe the model-theoretic approach used to obtain these results, demonstrating the techniques of model-theoretic ordinal analysis, a powerful tool for measuring the proof-theoretic strength of theories of arithmetic and analysis.<span class=\"Apple-converted-space\">\u00a0<\/span><\/p><\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t\t\t<\/div>\n\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-cdb87a7 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"cdb87a7\" 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-e75c89a\" data-id=\"e75c89a\" 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-bca0d28 elementor-widget-divider--view-line elementor-widget elementor-widget-divider\" data-id=\"bca0d28\" data-element_type=\"widget\" data-widget_type=\"divider.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<div class=\"elementor-divider\">\n\t\t\t<span class=\"elementor-divider-separator\">\n\t\t\t\t\t\t<\/span>\n\t\t<\/div>\n\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-c3161e7 elementor-section-content-middle elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"c3161e7\" 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-33 elementor-top-column elementor-element elementor-element-f573bbc\" data-id=\"f573bbc\" 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-739f09f elementor-widget elementor-widget-image\" data-id=\"739f09f\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t\t\t\t<figure class=\"wp-caption\">\n\t\t\t\t\t\t\t\t\t\t<img decoding=\"async\" width=\"200\" height=\"200\" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2791-200x200.jpg\" class=\"attachment-medium size-medium\" alt=\"\" loading=\"lazy\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2791-200x200.jpg 200w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2791-80x80.jpg 80w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2791-768x768.jpg 768w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2791-510x510.jpg 510w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2791.jpg 1080w\" sizes=\"(max-width: 200px) 100vw, 200px\" \/>\t\t\t\t\t\t\t\t\t\t\t<figcaption class=\"widget-image-caption wp-caption-text\">Han Gao (\u9ad8\u6657, Aix-Marseille University &amp; CNRS, France)<\/figcaption>\n\t\t\t\t\t\t\t\t\t\t<\/figure>\n\t\t\t\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-66 elementor-top-column elementor-element elementor-element-5359a97\" data-id=\"5359a97\" 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-1ee6be4 elementor-widget elementor-widget-toggle\" data-id=\"1ee6be4\" data-element_type=\"widget\" data-widget_type=\"toggle.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<div class=\"elementor-toggle\" role=\"tablist\">\n\t\t\t\t\t\t\t<div class=\"elementor-toggle-item\">\n\t\t\t\t\t<div id=\"elementor-tab-title-3241\" class=\"elementor-tab-title\" data-tab=\"1\" role=\"tab\" aria-controls=\"elementor-tab-content-3241\" aria-expanded=\"false\">\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon elementor-toggle-icon-left\" aria-hidden=\"true\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-closed\"><i class=\"fas fa-caret-right\"><\/i><\/span>\n\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-opened\"><i class=\"elementor-toggle-icon-opened fas fa-caret-up\"><\/i><\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t<a href=\"\" class=\"elementor-toggle-title\">Proof-search and counter-model construction for intuitionistic modal logics 14:30-15:50\u00a0<\/a>\n\t\t\t\t\t<\/div>\n\n\t\t\t\t\t<div id=\"elementor-tab-content-3241\" class=\"elementor-tab-content elementor-clearfix\" data-tab=\"1\" role=\"tabpanel\" aria-labelledby=\"elementor-tab-title-3241\"><p>Abstract: Intuitionistic modal logic as a branch of non-classical logic enjoys a history tracing back to 1940s. In the development since then, two main traditions have emerged, one called intuitionistic modal logic and the other constructive modal logic. These two traditions are motivated by meta-logical properties and applications in computer science respectively. In this talk, we will first give a brief introduction to the general development of the field of intuitionistic modal logic, then introduce FIK, an intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiom system of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a counter-model extraction: from any failed derivation of a given formula, we obtain by the calculus a finite counter-model of it directly. We also show how to restrict the level of nesting and then obtain a 1-level nested, label-free sequent calculus for FIK, which enjoys cut-elimination and shall have good complexity bound for the decision problem. Lastly, we mention some follow-up works and perspectives in the related field.<span class=\"Apple-converted-space\">\u00a0<\/span><\/p><\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t\t\t<\/div>\n\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-8c51e15 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"8c51e15\" 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-5871f2e\" data-id=\"5871f2e\" 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-1a22322 elementor-widget-divider--view-line elementor-widget elementor-widget-divider\" data-id=\"1a22322\" data-element_type=\"widget\" data-widget_type=\"divider.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<div class=\"elementor-divider\">\n\t\t\t<span class=\"elementor-divider-separator\">\n\t\t\t\t\t\t<\/span>\n\t\t<\/div>\n\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-fab4cd2 elementor-section-content-middle elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"fab4cd2\" 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-33 elementor-top-column elementor-element elementor-element-410ac1e\" data-id=\"410ac1e\" 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-2c8d7d7 elementor-widget elementor-widget-image\" data-id=\"2c8d7d7\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t\t\t\t<figure class=\"wp-caption\">\n\t\t\t\t\t\t\t\t\t\t<img decoding=\"async\" width=\"200\" height=\"189\" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2792-200x189.png\" class=\"attachment-medium size-medium\" alt=\"\" loading=\"lazy\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2792-200x189.png 200w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2792-768x726.png 768w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2024\/12\/WechatIMG2792.png 1000w\" sizes=\"(max-width: 200px) 100vw, 200px\" \/>\t\t\t\t\t\t\t\t\t\t\t<figcaption class=\"widget-image-caption wp-caption-text\">Zhe Lin (\u6797\u54f2, Xiamen University, China)<\/figcaption>\n\t\t\t\t\t\t\t\t\t\t<\/figure>\n\t\t\t\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-66 elementor-top-column elementor-element elementor-element-05c7be4\" data-id=\"05c7be4\" 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-88d9a87 elementor-widget elementor-widget-toggle\" data-id=\"88d9a87\" data-element_type=\"widget\" data-widget_type=\"toggle.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<div class=\"elementor-toggle\" role=\"tablist\">\n\t\t\t\t\t\t\t<div class=\"elementor-toggle-item\">\n\t\t\t\t\t<div id=\"elementor-tab-title-1431\" class=\"elementor-tab-title\" data-tab=\"1\" role=\"tab\" aria-controls=\"elementor-tab-content-1431\" aria-expanded=\"false\">\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon elementor-toggle-icon-left\" aria-hidden=\"true\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-closed\"><i class=\"fas fa-caret-right\"><\/i><\/span>\n\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-opened\"><i class=\"elementor-toggle-icon-opened fas fa-caret-up\"><\/i><\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t<a href=\"\" class=\"elementor-toggle-title\">Quasi Boolean algebras with operators and their applications 16:00-17:20<\/a>\n\t\t\t\t\t<\/div>\n\n\t\t\t\t\t<div id=\"elementor-tab-content-1431\" class=\"elementor-tab-content elementor-clearfix\" data-tab=\"1\" role=\"tabpanel\" aria-labelledby=\"elementor-tab-title-1431\"><p>Abstract: This paper studies a family of many-valued modal logics based on the Belnap-Dunn logic. The decidability of the consequence relations is shown for them via strong finite model property proofs. Furthermore, we consider the application of these logics in the domain of formal argumentation, focusing in particular on frameworks that account for context shifts and the evolution of information.<span class=\"Apple-converted-space\">\u00a0<\/span><\/p><\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t\t\t<\/div>\n\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\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>Time: 13:00-17:30, December 19, 2024 Venue: Room 329, S [&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\/7732"}],"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=7732"}],"version-history":[{"count":13,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7732\/revisions"}],"predecessor-version":[{"id":7755,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7732\/revisions\/7755"}],"wp:attachment":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/media?parent=7732"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}