命题逻辑

在逻辑和数学里，命题演算（或称句子演算）是一个形式系统，有着可以由以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。一般地说，演算是一个形式系统，包括一套语法表示式（合式公式）、这些表示式的一个特定子集（公理）和一套定义了特定的二元关系的形式规则，这个二元关系可解释为表示式空间上的逻辑等价关系。若形式系统会作为一个逻辑系统，其表示式会被解释成数学陈述，且其规则，被称之为“推理规则”，则一般会是保真的。在此设置下，规则（可能也包括公理）可以被用来从给定为真的陈述的公式中推导出表示真的陈述的公式来。公理的集合可能为空集、非空有限集、可数无限集或由公理模式所给定。形式文法递归地定义了语言的表示式和合式公式。之外，有时也可以给定一个语义，用以定义真值和赋值（或解释）。命题运算的语言包括：（1）一套原始符号，被称之为“原子公式”、“占位符”、“命题字母”或“命题变量”；（2）一套运算符号，被称之为“逻辑运算符”。一个“合式公式”是任一原子公式，或任一以运算符号依文法规则由原子公式创建起的公式。在下文中我们描述一种标准命题演算。很多不同的公式系统存在，它们都或多或少等价但在下列方面不同：（1）它们的语言（就是说哪些原始符号和运算符号是语言的一部分）；（2）它们有哪些（如果有的话）公理；（3）采用了哪些推理规则。命题演算是一个形式系统 L = L   ( A ,   Ω ,   Z ,   I ) {displaystyle {mathcal {L}}={mathcal {L}} (mathrm {A} , Omega , mathrm {Z} , mathrm {I} )} ，它的公式按如下方式构造：L {displaystyle {mathcal {L}}} 的语言，亦称之为“公式”或“合式公式”的集合，可由如下规则被归纳或递归地定义：透过重复应用这三个规则，可以建构出复杂的公式来。例如：设 L 1 = L   ( A ,   Ω ,   Z ,   I ) {displaystyle {mathcal {L}}_{1}={mathcal {L}} (mathrm {A} , Omega , mathrm {Z} , mathrm {I} )} ，这里的 A ,   Ω ,   Z ,   I {displaystyle mathrm {A} , Omega , mathrm {Z} , mathrm {I} } 定义如下：在合取、析取和蕴涵（∧、∨和→）这三个运算符之中，可以将其中一个拿来当做基本的，而另两个则以其和否定（¬）来定义。实际上，所有的逻辑运算符都可以用自足算子的方式来定义。而双条件（↔）当然可由合取和蕰涵来定义，亦即a ↔ b可被定义为(a → b)∧(b → a)。采用否定和蕰涵做为命题演算的两个基本运算，相当于把omega集 Ω = Ω 1 ∪ Ω 2 {displaystyle Omega =Omega _{1}cup Omega _{2}} 划分如下：有一个公理系统是扬·武卡谢维奇所发现的，而这系统可以如下地公式化为此语言中的命题演算。各个公理都是由下列的公理模式作代换所得。其推理规则为肯定前件（即可由p和(p → q)导出q）。而a ∨ b和a ∧ b则是分别被定义为¬a → b和¬(a → ¬b)。设 L 2 = L   ( A ,   Ω ,   Z ,   I ) {displaystyle {mathcal {L}}_{2}={mathcal {L}} (mathrm {A} , Omega , mathrm {Z} , mathrm {I} )} ，这里的 A ,   Ω ,   Z ,   I {displaystyle mathrm {A} , Omega , mathrm {Z} , mathrm {I} } 定义如下：在此命题演算的例子中，转换规则被解释为所谓的“自然演绎系统”下之推理规则。这里表述的特定系统没有起始点，这意味着它对逻辑应用的解释是从空公理集合中推导出其定理的。此命题演算有十个推理规则。这些规则允许我们从给定的一组假定为真的公式中推导出其他为真的公式。前九个只是简单地指我们可以从其他合式公式推论出特定的合式公式。但是最后一个规则使用了假言（hypothetical）推理，这意味着在规则的前提中，我们可以临时的假定一个（未证明的）假设作为推导出的公式集合的一部分，来查看我们是否能推导出一个特定的其他公式。因为前九个规则不是这样而通常被描述为“非假言”规则，而最后一个则被称为“假言”规则。以下推导将用编号后的行的列表来表示，在每行之上有一个单一的公式和一个理由（justification）。论证的各个前提会在列表的首行给出。结论将在最后一行。一个推导称为完备的，若所有行都是通过正确的应用一个规则而从前面的行得出的。下面是（语法上的）证明的一个例子： 要证明： A → A {displaystyle Arightarrow A} 证明：A ⊢ A {displaystyle Avdash A} 可解释为“假定A，推导出A”。 ⊢ A → A {displaystyle vdash Arightarrow A} 为“不假定任何东西，推导出A蕴涵A”，或者“A蕴涵A是重言式”，或者“A蕴涵A是永真的”。以上规则的关键特性是它们是可靠的和完备的。非形式的说，这意味着规则都是正确的并且不再需要其他规则。这些要求可以如下这样正式的提出。我们定义真值指派为把命题变量映射到真或假的函数。非形式的，这种真值指派可以被理解为对事件的可能状态（或可能世界）的描述，在这里特定的陈述是真而其他为假。公式的语义因而可以被形式化，通过定义哪些"事件状态"是设置为真的。我们通过如下规则定义这种真值指派A在什么时候满足特定公式：通过这个定义，我们现在可以形式化公式φ被特定公式集合S蕴涵的意义。非形式的，就是在使给定公式集合S成立的所有可能情况下公式φ也成立。这引申出下面的形式化定义：我们说公式集合S 语义蕴涵特定的公式φ，条件是满足在S中的公式的所有真值指派也满足φ。最后我们定义语法蕴涵，φ被S语法蕴涵，当且仅当我们可以在有限步骤内使用我们提出的上述推理规则推导出它。这允许我们精确的公式化推理规则的可靠性和完备性的意思：上述的两个例子都满足可靠性和完备性。（对于多数逻辑系统，这是相对“简单”的证明方向）符号约定：设G是命题集合。设φ、ψ和χ是命题。我们把“G语法蕴涵φ”写成“G证明φ”，还有把“G语义蕴涵φ”写成“G蕴涵φ”。我们要展示：(∀φ)(∀G)(如果G证明φ，则G蕴涵φ)我们注意到“G证明φ”有一个归纳定义，这给予我们直接的办法来验证“如果G证明φ，则……”形式的断言。所以我们的证明是用归纳法进行的。需要注意的是，对于自然演绎系统，基础步骤II可以省略，因为它们根本没有公理。基本上，基础步骤II是要展示每个公理都是（语义上的）逻辑真理。基础步骤证实了对于任何G，来自G的最简单的可证明的语句都被G所蕴涵。（这是简单的，因为集合蕴涵它的任何一个成员，是个平凡的语义事实）。归纳步骤将有系统的覆盖所有的进一步的可证明的命题--通过考虑我们能够使用推理规则达成逻辑结论的每种情况--并展示如果一个新命题是可证明的，它也是在逻辑上被蕴涵的。（例如，可能有一个规则，使得从φ可以推导出“φ或ψ”。在III.（a）中我们假定如果φ是可证明的则它也是被蕴涵的。我们也知道如果φ是可证明的，则“φ或ψ”是可证明的。接着，我们必须验证“φ或ψ”也是被蕴涵的。我们求助于语义的定义和我们所做的假定来完成。我们假定了φ是可以从G证明出来的，所以它也被G所蕴涵。所以任何使G全部为真的指派，都使φ为真。此外通过“或”的语义定义，使φ为真的任何指派都使“φ或ψ”为真。所以任何使G的全部为真的指派，都使“φ或ψ”为真。所以“φ或ψ”被蕴涵了。）一般的，归纳步骤的证明会较长，但不过是对所有推论规则按例分析，去展示每个规则都能“保持”语义蕴涵。通过可证明性的定义，除了G的成员、公理、或从规则推导出的命题之外，没有别的命题是可证明的；而这些命题都是语义上被蕴涵的，所以演绎演算是可靠的。（这通常是相对地困难不少的证明方向。）我们采用同上面一样的符号约定。我们要展示：如果G蕴涵φ，则G证明φ。我们通过反证法来进行：我们转而展示如果G不证明φ，则G不蕴涵φ。下面定义的命题演算通过公理的方式定义了多数逻辑算子的语法并且它只使用一个推理规则。它也叫做标准命题演算。设φ、χ和ψ表示合式公式。（wff自身将不包含任何希腊字母，而只包含大写罗马字母、链接算子和圆括号）。公理有公理THEN-2可以被看作是“蕴涵关于蕴涵的分配律”。公理AND-1和AND-2对应于“合取除去”。在AND-1和AND-2之间的关系反映了合取算子的交换律。公理AND-3对应于“合取介入”。公理OR-1和OR-2对应于“析取介入”。在OR-1和OR-2之间的关系反映了析取算子的交换律。公理NOT-1对应于反证法。公理NOT-2说明了“从矛盾中可以推导出任何东西”。公理NOT-3叫做排中律（拉丁语tertium non datur：“排除第三者”）并反映了命题公式的语义求值：公式的真值要么是真要么是假。至少在经典逻辑中，没有第三个真值。直觉逻辑不接受公理NOT-3。推理规则是肯定前件：如果还使用双箭头的等价算子的话，则要增加如下"自然"推理规则：设一个推导被表示为相继式，各个假设在十字转门（turnstile）的左侧，而结论在十字转门的右侧。则演绎定理可以被陈述如下：这个演绎定理（DT）自身没有公式化为命题演算：它不是命题演算的定理，而是关于命题演算的一个定理。在这个意义上，它是元定理，相当于关于命题演算可靠性和完备性的定理。在另一方面，DT对于简化语法上的证明过程是如此的有用以至于它看作和用做推理规则，同肯定前件一起使用。在这个意义上，DT对应于自然条件证明推理规则，它是在本条目中提出的第二个例子的命题演算的一部分。DT的逆定理也是有效的：实际上，DT的逆定理的有效性相对于DT而言是平凡的：DT的逆命题有着强有力的蕴涵：它可以用来把公理转换成推理规则。例如，公理AND-1可以通过演绎定理的逆定理的方式被转换成推理规则这是合取除去，是前面给出的自然演绎命题演算中使用的十个推理规则中的一个。下面是（语法上）证明的一个例子，只涉及到公理THEN-1和THEN-2： 要证明：A → A（蕴涵的自反性）。 证明：前面的公理化命题演算是希尔伯特风格演绎系统的一个例子。在这种命题系统中公理是用逻辑链接词构建的项，而唯一的推理规则是肯定前件。等式逻辑在高等学校的抽象代数教学中被作为正式的标准，它是不同于希尔伯特系统的一类不同的演算。它的定理是等式而它的推理规则表达出等号的性质，也就是在容许代换的项上的相等关系。上述的经典命题演算等价于布尔代数，而直觉命题演算等价于海廷代数。等价性是通过在两个方向上转换各自系统的定理来证明的。经典命题演算或直觉命题演算的定理Φ被分别转换为布尔代数或Heyting代数的等式Φ = 1。反过来布尔代数或Heyting代数的定理x = y被分别转换为定理经典名义演算或直觉命题演算的定理(x → y)∧(y → x)，它的标准简写是x ≡ y。在布尔代数的情况下，x = y还可以被转换为(x∧y)∨(¬x∧¬y)，但在直觉命题演算的情况下中不能这么转换。在布尔代数和Heyting代数中，可以使用不等式x ≤ y代替等式。等式x = y可以被表达为一对不等式x ≤ y和y ≤ x。反过来不等式x ≤ y可被表达为等式x∧y = x或x∨y = y。不等式的重要性在于它对应于希尔伯特系统的演绎或蕴涵符号 ⊢ {displaystyle vdash } 。蕴涵被转换为代数框架下的不等式反过来代数不等式x ≤ y被转换为蕴涵在实质条件（implication）x → y和不等式或者蕴涵（entailment）x ≤ y或 x   ⊢   y {displaystyle x vdash y} 之间的区别在于，前者是内在于逻辑的，而后者是外在的。在两个项之间内在的实质条件是同类的另一个项。在两个项之间的外在的蕴涵表达了在逻辑语言之外的元真理，并被认为是元语言的一部分。即使所研究的逻辑是直觉的，蕴涵都通常经典的理解为二值的：要么左侧蕴涵（或小于等于）右侧，要么不蕴涵之。同代数逻辑之间类似但更加复杂的相互转换，对于自然演绎系统和相继式演算也是可能的。后者的转换可以被释义为二值的，但是更有洞察力的释义是作为集合，它的元素可以被理解为由范畴的态射组成的抽象证明。在这种释义下相继式演算的切规则对应于范畴的复合。命题演算大概是在所有当前使用的逻辑演算中最简单的一种。（亚里士多德的“三段论”演算，在现代逻辑中在很大程度上被替代了，它与命题逻辑相比在某些方面更简单--但在其他方面更加复杂）。它可以按很多方式来扩展。最直接的方式是开发一个更加复杂的逻辑演算，介入对所用于的句子的更精细的细节敏感的规则。在命题逻辑中的原子句子被分解成项（英语：Singular term）、变量、谓词和量词的时候，它们就生成了一阶逻辑，或者叫做一阶谓词逻辑，它保留命题逻辑的所有规则并增加了一些新规则。（例如，从“所有的狗都是动物”我们可以推出“如果Rover是狗，则Rover是动物”）。通过一阶逻辑的工具，有可能公式化一些理论，要么带有显式的公理要么通过推理规则，而把它们自身当作逻辑演算。算术是其中最周知的理论；其他的还包括集合论和分体论。模态逻辑也提供了一种推理的变体，它不能在命题演算中捕获。例如，从“必然地p”我们可以推出p。从p我们可以推出“可能地p”。多值逻辑是允许句子有除了“真”和“假”之外的值的逻辑。（例如，“都不”和“都是”是标准的“额外值”；“连续统逻辑”允许每个句子有任何的在“真”和“假”之间的表示“真实程度”的无限个值）。这些逻辑经常要求与命题逻辑非常不同的运算设备。