离散数学课程-逻辑专题答疑-问题收集

[hengxin]

下周（2021-03-25）课上，计划安排一次关于逻辑专题的答疑。

本讨论区用于收集大家的疑问，可以是不理解的概念、例子等。若有疑问，请在下面回复。

请尽量具体地描述你的问题。

请尽量在周一（包含）之前回复，便于我之后备课。

在提出自己的问题之前，请浏览一下已有的问题。如果问题类似，可为问题投票或回复该问题，避免重复提问。

如果你认为你的问题不在课堂答疑范围内，也可以开一个新的讨论区。

[Labelray]

应该如何理解这句话？”被释放“在形式化证明中又该如何体现？具体应该如何书写相关证明？

[Labelray]

顺便 是只有用implies的形式才能discharge吗

[hengxin]

是的。在我们介绍的推理系统中，只有在证明 A \to B 这种结论时，需要引入 assumption [A]，因此也只在这里会“释放” assumption [A]。当引入了某个假设 [A]，然后基于该假设进行推理，得出了 B，我们就可以得出结论 A \to B，并称 [A] 被释放了。在该推理中，B 是基于引入的假设 [A] 得到的，而 A \to B 则不依赖于假设 [A]，所以我们称 [A] 被释放了。下周课上，我会通过例子再作解释。

[kaiwenKevinn]

请问之前的作业有标准答案吗，有得分反馈或者讲解吗？

[hengxin]

有得分反馈。助教批改完后会发给大家。标准答案，需要点时间。后面会安排习题课。

[Martin7-1]

老师请问 答题的时候有严格的书写格式之类的吗，或者是只要能够用严谨的逻辑说清楚解答就可以？

[hengxin]

使用标准的格式书写证明，也是我们作证明训练的一部分。从格式方面来说，写证明，就好比写代码，不仅要正确，还要符合格式标准，方便自己也方便他人阅读。我们会在后面的课堂上强调这一点。

[Arthur-Sun]

请问老师这个符号的意思是 一个命题——对任意x都满足公式α，还是一个条件——当任意的x都满足公式α 啊

[hengxin]

不是条件，是一个公式：首先，\alpha 是一个公式，根据公式的递归定义，\forall x. \alpha 也是公式。