{"id":7852,"date":"2025-01-19T01:20:15","date_gmt":"2025-01-18T17:20:15","guid":{"rendered":"http:\/\/tsinghualogic.net\/JRC\/?page_id=7852"},"modified":"2025-06-17T10:37:23","modified_gmt":"2025-06-17T02:37:23","slug":"introduction-to-categorical-logic","status":"publish","type":"page","link":"http:\/\/tsinghualogic.net\/JRC\/introduction-to-categorical-logic\/","title":{"rendered":"<strong><strong>Introduction to Categorical Logic<\/strong><\/strong>"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"7852\" class=\"elementor elementor-7852\" 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-83e517a elementor-section-content-middle elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"83e517a\" 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-50 elementor-top-column elementor-element elementor-element-3f36b11\" data-id=\"3f36b11\" 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-f47351d elementor-widget elementor-widget-text-editor\" data-id=\"f47351d\" 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 style=\"caret-color: #000000; color: #000000;\"><li>Time: 13:30-16:05, June 23<sup>rd<\/sup>-27<sup>th<\/sup><\/li><li>Location: Room 4201, Teaching Building No.4 (\u56db\u6559).<\/li><li>Lecturer:\u00a0Ivan Di Liberti\u00a0(G\u00f6teborgs Universitet) and\u00a0Lingyuan Ye\u00a0(University of Cambridge)<span style=\"font-family: var( --e-global-typography-text-font-family ), Sans-serif; font-size: 1.2em; text-align: inherit;\">\u00a0<\/span><\/li><li>TA\uff1aZhongqin Gao \uff08gaozq21@mails.tsinghua.edu.cn\uff09<\/li><li>Course webpage\uff1a<a href=\"https:\/\/diliberti.notion.site\/Introduction-to-Categorical-Logic-ea235c2094874a8ba5d05e2bb563483c\">Introduction-to-Categorical-Logic<\/a><\/li><li>A WeChat group has been created for announcements, room changes, and social events. If you haven&#8217;t received invitation, \u00a0please contact the TA.\u00a0<\/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-25 elementor-top-column elementor-element elementor-element-e9420a6\" data-id=\"e9420a6\" 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-f964c0e elementor-widget elementor-widget-text-editor\" data-id=\"f964c0e\" 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-7854 \" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/ivan.jpg\" alt=\"\" width=\"193\" height=\"254\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/ivan.jpg 554w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2025\/01\/ivan-152x200.jpg 152w\" sizes=\"(max-width: 193px) 100vw, 193px\" \/><\/p><p style=\"text-align: center;\"><a href=\"https:\/\/diliberti.github.io\/\">Ivan Di Liberti<\/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<div class=\"elementor-column elementor-col-25 elementor-top-column elementor-element elementor-element-2323f19\" data-id=\"2323f19\" 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-a5768d6 elementor-widget elementor-widget-text-editor\" data-id=\"a5768d6\" 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=\"wp-image-5826 aligncenter\" src=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2023\/05\/B88F5F95-BCD1-496E-AA36-2E2F1CA690F5_1_105_c-e1737220915133.jpeg\" alt=\"\" width=\"267\" height=\"258\" srcset=\"http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2023\/05\/B88F5F95-BCD1-496E-AA36-2E2F1CA690F5_1_105_c-e1737220915133.jpeg 452w, http:\/\/tsinghualogic.net\/JRC\/wp-content\/uploads\/2023\/05\/B88F5F95-BCD1-496E-AA36-2E2F1CA690F5_1_105_c-e1737220915133-200x193.jpeg 200w\" sizes=\"(max-width: 267px) 100vw, 267px\" \/><\/p><p style=\"text-align: center;\">\u00a0<a href=\"https:\/\/yelingyuan.fr\/\">Lingyuan Ye<\/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-ce5b4a4 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"ce5b4a4\" 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-3ebc005\" data-id=\"3ebc005\" 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-84d53da elementor-widget elementor-widget-heading\" data-id=\"84d53da\" 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-9ce04d7 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"9ce04d7\" 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-8d1b460\" data-id=\"8d1b460\" 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-afdbf2c elementor-widget elementor-widget-text-editor\" data-id=\"afdbf2c\" 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>Categorical Logic, and Functorial semantics more specifically, emerged in the 1960s as an alternative framework to capture universal algebra. The framework offers a collection of advantages, including a more flexible and modular approach to semantics, which delivers a perfect correspondence with syntax. These tools offer a more quantitative and conceptual take on completeness results and definability-type theorems.<\/p><p>After a brief introduction to the language of categories, we focus on universal algebra and functorial semantics. We capture the notion of algebraic theory via categories with products (Lawvere theories) and present a syntax-semantics duality between varieties and Lawvere theories. The course ends with some vistas on the theory of sketches which offers a much more general framework, covering the leap from universal algebra to infinitary first order logic.<\/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-855b207 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"855b207\" 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-dfe119e\" data-id=\"dfe119e\" 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-16e5138 elementor-widget elementor-widget-heading\" data-id=\"16e5138\" 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\">Tentative Schedule<\/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-bef79f7 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"bef79f7\" 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-f0c305a\" data-id=\"f0c305a\" 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-76abe9d elementor-widget elementor-widget-text-editor\" data-id=\"76abe9d\" 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: center;\"><b>TBA.<\/b><\/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-7ca3d1c elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"7ca3d1c\" 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-44bc430\" data-id=\"44bc430\" 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-4a5cb5a elementor-widget elementor-widget-heading\" data-id=\"4a5cb5a\" 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-c581092 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"c581092\" 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-8c0c46a\" data-id=\"8c0c46a\" 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-6894d9d elementor-widget elementor-widget-text-editor\" data-id=\"6894d9d\" 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 audience is expected to be familiar and have played with the basic definitions of one of following objects: vector space, monoid, group, ring, module, set equipped with operations.<\/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-77efb51 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"77efb51\" 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-0cafdc3\" data-id=\"0cafdc3\" 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-027d64a elementor-widget elementor-widget-heading\" data-id=\"027d64a\" 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\">Slides and Exercises<\/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-f7a0c32 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"f7a0c32\" 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-8ba32a2\" data-id=\"8ba32a2\" 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-dcb1f8e elementor-widget elementor-widget-text-editor\" data-id=\"dcb1f8e\" 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: center;\"><b>TBA.<\/b><\/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-5056112 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"5056112\" 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-6cfc7e2\" data-id=\"6cfc7e2\" 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: 13:30-16:05, June 23rd-27th Location: Room 4201,  [&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\/7852"}],"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=7852"}],"version-history":[{"count":25,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7852\/revisions"}],"predecessor-version":[{"id":8183,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7852\/revisions\/8183"}],"wp:attachment":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/media?parent=7852"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}