自然演绎系统也是一种逻辑演算体系,与公理系统的区别在于它的出发点只是一些变形规则而没有公理,是附有前提的推理系统。变形规则和证明过程更接近于一般的数学思维,是较直接而自然的,所以称为自然演绎系统。
所建立的系统与节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。
|