What：数理逻辑是数学的一个分支，是数学基础中不可或缺的组成部分。数理逻辑的研究范围是逻辑中能够被数学形式化描述和推演的部分。其研究对象是对证明和计算这两个直观概念进行符号化之后的形式系统。

Who： 秦逸（南京大学仙林校区计算机科学与技术系楼501室；email）

Where： 仙林校区逸夫楼A-322

When： 每周五2-4节（09:00 -- 12:00），1-16周

Which： 从2025-26年学年春季学期开始，本课程将会进行结构性调整。课程范围将从纯粹的数理逻辑理论，拓展至作为朴素概念的逻辑、作为形式化数学系统的逻辑，以及工程化计算机系统的逻辑这三个部分。此举旨在培养学生针对计算机科学相关信息，具备独立自主的逻辑判断与推理能力。考虑到目前尚无单一教材能够完全契合这一需求，现阶段将以课程讲义作为主要的学习资料。同时，推荐同学们参考相关的经典教材作为课余辅助。

  • 《数理逻辑十二讲》（宋方敏等编著，机械工业出版社）是本课程的传统教材，主要从纯粹的数学视角出发，介绍了数理逻辑的基础理论与重要定理。本课程将基于此书介绍形式化系统及其两个重要的推理框架。由于课堂上不再详细重现重要定理的逐步推导，而是侧重于介绍证明思路与流程，因此对严格数学推导感兴趣的同学可以深入阅读此书。

  • 《数理逻辑引论——计算机科学与系统的天然基础》（刘志明等编著，科学出版社）从计算机科学的视角阐述了数理逻辑的基本概念。本课程将借鉴此书探讨作为朴素概念的逻辑。需要注意的是，该书展示的形式化推理系统与本课程介绍的系统在表述上有所区别，但能力等价，适合用来对比理解形式化系统的核心内涵。

  • 《Software Foundations》第一卷《Logic Foundations》（Benjamin C. Pierce等著）从计算机软件的角度介绍了Coq推理证明器。本课程将以此为基础，介绍工程化计算机系统中的逻辑验证工具。鉴于课程目标是利用Coq辅助逻辑推理而非单纯构建计算机程序，对程序验证感兴趣的同学可将其作为进阶参考。

    课程规则

    本课程的考核由三个部分组成：平时成绩占总评的10%，课程作业占40%，期末考试占50%。

  • 平时成绩：主要依据各项作业的提交情况来评定。

  • 课程作业：分为书面作业与上机作业两部分，各占总评成绩的20%。传统的书面作业将在学期中期布置，形式为课后习题，主要考察学生对数理逻辑基本概念和方法的掌握程度，常规提交期限为一周。上机作业同样于学期中期发布，形式为Coq编程练习，侧重考察利用Coq构建计算机辅助推理系统的实践能力，提交期限设定为期末考试后的一周内。

  • 期末考试：将于学期末进行，采用开卷形式，全面考察本课程所讲授的基础概念、推理方法及证明技巧。

    特别说明： 本课程鼓励学生使用人工智能助手辅助完成加工作业。但是使用此类工具的前提是学生必须对最终提交的内容具有完全的掌握度，并且能够准确解释作业中的所有解题推导与编程细节。我们不强制禁止人工智能的使用，但过度依赖此类工具可能会导致学生在期末考试中无法适应独立解答的要求。

    动态新闻

    2026-02-27：相关课程材料已上传。

    2026-02-27：课程主页正式建立。

    课程讲义

    课程讲义通常会在上课前发布，但内容可能会根据教学进度随时更新。请同学们密切关注文件的更新时间，以确保获取的是最新版本。

    书面作业

    课程的作业邮箱为 mathlogicnju@163.com。在提交作业时，请务必将邮件主题格式设定为“学号+姓名+第XX次作业”。同学们可以提交纯电子版作业，也可以提交手写作业的高清扫描件或照片，但请务必保证提交版本的清晰度与可读性。

    补充材料

    本课程的书面作业包含大量的数学公式推导与排版。强烈推荐大家使用科技排版系统LaTeX来完成并提交电子版作业。LaTeX是由图灵奖得主Leslie Lamport设计开发的专业排版系统，在当今的学术论文撰写中发挥着不可替代的作用。您可以前往CTeX的官方网站下载其适用的中文发行版。

    在参考书目选择方面，由于主教材侧重于数理逻辑原理的数学化表达，可能会给同学们的课余阅读带来一定挑战。您可以自由选择其他参考书籍作为辅助理解的工具：

  • 李未教授编写的《数理逻辑-基本原理与形式演算》，该书不仅涵盖了经典理论，还采用了计算机软件的思维方式来解释逻辑概念，增强了可读性。

  • M. Huth等人撰写的《Logic in Computer Science》则从模型验证等实践角度，系统展示了逻辑原理与计算机科学的结合。

  • S. Hedman的《A First Course in Logic》从可计算性的视角出发，梳理了从命题逻辑到NP问题的一系列经典结论。

    关于数理逻辑证明

    本课程的许多问题都会要求您进行严格的“证明”，即给出令人信服的逻辑推演来解释某个命题为何成立。为了确保您的书面论证能够清晰传达思想并获得相应的认可，您的证明过程应当尽可能贴近专业教科书的规范。您的证明需要由完整的、语法正确的句子构成。证明中出现的所有变量，要么是题目陈述中已有的元素，要么必须在推理过程中通过明确的文字进行引入和定义。每一个陈述步骤都必须清晰地遵循先前的逻辑基础并附带原理解释，或者具有明确的论证目的，例如明确宣告进入反证法假设或归纳法步骤。同时，任何直接引用的现成结论都应当标明其通用的学术名称或标注出处。

    撰写证明的核心目的，并非仅仅向评分者展示您内心理解了题意，而是向具备相应基础但尚未思考过该问题的读者，完整地重现您的推理方案。在这个过程中，书面文字是您唯一的交流媒介。因此，讲师在课堂上的部分简写板书并不能直接等同于严谨的书面证明，因为它们脱离了当时的口头讲解后往往缺乏完整的逻辑链条。证明的评判标准在于评分者能否仅凭您的文字描述就毫无障碍地复现您的推理过程。如果因为表述跳跃导致评分者无法理解您的精妙构思，您可以在作业或考试成绩发布后，与讲师当面探讨并审查证明的合理性。