第二课：数学基础

1.逻辑基础

命题逻辑 + 谓词逻辑
变体：经典逻辑、构造逻辑。

2.命题逻辑 Propositional logic:

每个形式系统应当包括语法+语义

2.1 语法 The syntax

$P \bigvee P$P⋁P ：析取
$P \bigwedge P$P⋀P：合取
$P \to P$P→P：蕴含

2.2 证明系统 The proof system

数学上：Hibert系统，构造性，没有规律可言。
CS上：自然演绎系统，具有机械化步骤，即算法。

Nature deduction

• 断言 Judgment：Γ⊢????
  Γ为命题组成的列表，P是单独的逻辑命题。Example: P, Q, R ⊢????
  可以理解为Γ是一组假定为真，在这种假定的前提下，能够推出P为真。

• 推理规则
  四元组：直线，直线上面为n个断言（前提/假设），下面一个断言（结论），右侧名字（推理规则名字）。
  
  意思是，如果在Γ条件下去证明P，那么只需要证明Γ1⊢????1、Γ2⊢????2…，同理一旦知道前提条件，即可证明Γ⊢????。
  由假设到结论，由结论到假设的双向推理过程。
  如果当前提中，n=0时，即为公理(axiom)。
  （1）直接证明的结论P，已经存在前提条件中。（公理）
  
  （2）T是无条件成立（公理）
  
  TI中的I为introduction，引入。
  （3）⊥，假推出一切！
  
  ⊥E中的E为elimination，消去。
  从一组自相矛盾的条件出发，任何结论都成立。
  （4）$\bigwedge$⋀，如果可以证明P，也可以证明Q，那么可以证明$P \bigwedge P$P⋀P
  
  （5）$P \bigvee P$P⋁P
  
  （6）$P \to P$P→P
  
  （7）¬ （反证法）
  
  （8）¬¬ 双重否定律
  
  不同的是之前所有都是语法制导。

2.3 语义 Semantics

证明系统关心的是是否可证，以及不可证，而在语义学中更关心计算，得到的结果是“真”还是“假”。但并不是所有问题都是可计算的，NP以及NPC问题。

• 真值表 The truth table
  
• Interpertation
  
  在以上两个形式系统AB中，A即上文中研究的命题逻辑系统（逻辑命题，连接词，推理规则），B即真值表系统（T，F，AND，OR），语义学本质上要写一个编译器V，将A中的元素编译（数学中即映射\函数）到B中。
• 重言式 Tautology （永真式）
  即对于任意的编译器V，V§=T，使用⊨ P来表示。
  （⊢????语法上可证，⊨ P通过计算为真）
  两种观点命题成立，1.在证明系统中可证 2.在模型论中为真。
  可靠性：Γ⊢ P => Γ ⊨ P
  完备性：Γ ⊨ P => Γ⊢ P

3.构造逻辑 Constructiove logic

3.1 Motivation

排中律：⊢ P / ~P