形式系统-命题演算

命题演算（Propositional Calculus）是书中介绍的一个概念-形式系统，它旨在形式化地捕捉逻辑推理中仅依赖于“并且”（and）、“或”（or）、“非”（not）、“若…则…”（if…then…）这四个词的推理部分。它是一个没有公理，完全由推理规则驱动的系统。

只依赖于正确使用这四个词的那种推理，叫作命题推理。

系统定义

命题演算的符号表包括：

系统的“合法语句”（良构串）是通过概念-递归规则定义的：

每一个串都可以用这种方法追溯到它的基本成分——这就是原子。你可以简单地往回运用形成规则，直到你不能再往下用为止。

命题演算的核心是一套精巧的推理规则，用于从无到有地生成定理：

联结规则: 如果x和y是定理，那么<x∧y>是定理。
分隔规则: 如果<x∧y>是定理，那么x和y都是定理。
双重弯号规则: ～～可以从任何定理中删除，或添加到任何定理中（只要结果良构）。
幻想规则 (演绎定理): 如果假定x是一个定理时能推导出y来，那么<x→y>是一个定理。这是系统生成第一条定理的起点，通过进入一个“幻想”的层次来完成。
搬入规则: 在一个幻想里边，任何来自于“现实性”高一个层次的定理都可以拿进并使用。
分离规则 (Modus Ponens): 如果x和<x→y>二者都是定理，那么y是一个定理。这对应于人物-刘易斯·卡罗尔的对话中乌龟所挑战的逻辑步骤。
易位规则: <x→y>与<～y→～x>是可互换的。
德·摩根规则: <～x∧～y>与～<x∨y>是可互换的。
思维陀螺规则: <x∨y>与<～x→y>是可互换的。

这个系统的一个特别之处在于它没有公理——只有规则。……事情怎么才能开始呢？回答是有那么一条规则，它无中生有地制造定理——它不需要一个“老定理”作为输入……这个特别的规则被称为幻想规则。

命题演算的定理，在“半解释”（只解释逻辑符号，不解释原子P, Q, R等）下，都是普遍为真的语句形式，例如<P∨～P>（P或非P）。这表明该系统是一致的，它通过纯粹的符号操作，精确地捕捉了逻辑真理的某种形式。

命题演算的关键思想：它产生一些定理，当它们被半解释时，它们被看成是“普遍为真的半句子”，由此就意味着：不管我们怎样去把解释做完全，最后的结果总是一个真语句。