自然演绎系统也是一种逻辑演算体系,与公理系统的区别在于它的出发点只是一些变形规则而没有公理,是附有前提的推理系统。变形规则和证明过程更接近于一般的数学思维,是较直接而自然的,所以称为自然演绎系统。
  所建立的系统与节3.2的公理系统是等价的,即自然演绎系统可导出公理系统的所有定理,自然演绎系统的所有定理也可由重言式来描述,从而可由公理系统导出。
  下面建立一个自然演绎系统。


一、初始符号

  除公理系统3.2的符号外引入
  = {A1, …, An} = A1, …, An
  表示有限个命题公式的集合。
  ├A
  表示,A间有形式推理关系,为形式前提, A为形式结论, 或说使用推理规则可由得A。

二、形成规则

  同公理系统3.2

三、变形规则

  1. A1, …, An├Ai (i = 1, …, n)肯定前提律。
  推理过程中前提总是被肯定的,前提中任何命题都可作为结论。
  2. 如果├A, A├B 则├B, 传递律。
  3. 如果,A├B且, A├B 则├A 反证律
  在前提下, 再假设A是假的, 若可推出矛盾命题时, 使可由前提推出A。
  4. A→B, A├B 蕴涵词消去律(分离规则)
  5. 如果, A├B则├A→B 蕴涵词引入律
  在前提下, 又知A为真, 可得B。那么在原前提下可推得, 如果A那么B。