命题逻辑

一般地说，演算是一个形式系统，包括一套语法表示式（合式公式）、这些表示式的一个特定子集（公理）和一套定义了特定的二元关系的形式规则，这个二元关系可解释为表示式空间上的逻辑等价关系。

若形式系统会作为一个逻辑系统，其表示式会被解释成数学陈述，且其规则，被称之为“推理规则”，则一般会是保真的。在此设置下，规则（可能也包括公理）可以被用来从给定为真的陈述的公式中推导出表示真的陈述的公式来。

公理的集合可能为空集、非空有限集、可数无限集或由公理模式所给定。形式文法递归地定义了语言的表示式和合式公式。之外，有时也可以给定一个语义，用以定义真值和赋值（或解释）。

命题运算的语言包括：（1）一套原始符号，被称之为“原子公式”、“占位符”、“命题字母”或“命题变量”；（2）一套运算符号，被称之为“逻辑运算符”。一个“合式公式”是任一原子公式，或任一以运算符号依文法规则由原子公式创建起的公式。

在下文中我们描述一种标准命题演算。很多不同的公式系统存在，它们都或多或少等价但在下列方面不同：（1）它们的语言（就是说哪些原始符号和运算符号是语言的一部分）；（2）它们有哪些（如果有的话）公理；（3）采用了哪些推理规则。

命题演算是一个形式系统，它的公式按如下方式构造：

是由名为“命题符号”或“命题变量”之元素所组成的有限集合。语法上来说，它们是形式语言最基本的元素，亦被称之为“原子公式”或“终端元素”。在接着的例子中，内的元素一般写作字母p, q, r之类的形式。

是名为“算子符号”或“逻辑运算符”之元素所组成的有限集合。集合被划分成如下等不相交的子集：

。

在此一划分中，是指元数为的算子符号所构成的集合。

在更熟知的命题演算中，一般被划分如下：

。

一种常用的做法是把常数逻辑值当作一种零元算子，即：

。

有些作者用~来替代¬，也有的用&或来取替。逻辑值所构成的集合也有许多不同的符号表示，如{假,真}、{F,T}、{0,1}和{,}，这些都常见于各个论著之中。

依据所使用的精确形式文法或文法形式化，可能需要以左括号"（"和右括号"）"作语法上的辅助，用来完成公式的构造。

的语言，亦称之为“公式”或“合式公式”的集合，可由如下规则被归纳或递归地定义：

1. 基本元素：内的任何元素都是的公式。

   步骤（a）：如果p是公式，则¬p也会是公式。

   步骤（b）：如果p和q是公式，则( )、( )、()和()也都会是公式。

   封闭性：其他都不会是的公式。

透过重复应用这三个规则，可以建构出复杂的公式来。例如：

1. 依规则1，p是公式。

   依规则2，¬p是公式。

   依规则1，q是公式。

   依规则3，(¬p ∨ q)是公式。

是“转换规则”（当作为逻辑应用时则称之为“推理规则”）之所构成的有限集合。

是“起始点”（当得到逻辑解释时则称之为“公理”）所构成的有限集合。

设，这里的定义如下：

是个含有足够多元素以应付讨论所需的有限集合，如：

。

在合取、析取和蕴涵（∧、∨和→）这三个运算符之中，可以将其中一个拿来当做基本的，而另两个则以其和否定（¬）来定义。实际上，所有的逻辑运算符都可以用自足算子的方式来定义。而双条件（↔）当然可由合取和蕰涵来定义，亦即a ↔ b可被定义为(a → b)∧(b → a)。

采用否定和蕰涵做为命题演算的两个基本运算，相当于把omega集划分如下：

。

。

有一个公理系统是扬·武卡谢维奇所发现的，而这系统可以如下地公式化为此语言中的命题演算。各个公理都是由下列的公理模式作代换所得。

其推理规则为肯定前件（即可由p和(p → q)导出q）。而a ∨ b和a ∧ b则是分别被定义为¬a → b和¬(a → ¬b)。

设，这里的定义如下：

是个含有足够多元素以应付讨论所需的有限集合，如：

。

划分为如下：

。

。

在此命题演算的例子中，转换规则被解释为所谓的“自然演绎系统”下之推理规则。这里表述的特定系统没有起始点，这意味着它对逻辑应用的解释是从空公理集合中推导出其定理的。

起始点的集合是空的，亦即。

转换规则的集合描述如下：

此命题演算有十个推理规则。这些规则允许我们从给定的一组假定为真的公式中推导出其他为真的公式。前九个只是简单地指我们可以从其他合式公式推论出特定的合式公式。但是最后一个规则使用了假言（hypothetical）推理，这意味着在规则的前提中，我们可以临时的假定一个（未证明的）假设作为推导出的公式集合的一部分，来查看我们是否能推导出一个特定的其他公式。因为前九个规则不是这样而通常被描述为“非假言”规则，而最后一个则被称为“假言”规则。

反证证明（否定介入）：从φ → ¬ ψ和φ → ψ中可推出¬ φ。双重否定除去：从¬ ¬ φ中可推出φ。合取介入：从φ和ψ中可推出(φ ∧ ψ)。合取除去：从(φ ∧ ψ)中可推出φ和ψ。析取介入：从φ中可推出(φ ∨ ψ)和(ψ ∨ φ)。析取除去：从(φ ∨ ψ)、(φ → χ)和(ψ → χ)可推出χ。双条件介入：从(φ → ψ)和(ψ → φ)中可推出(φ ↔ ψ)。双条件除去：从(φ ↔ ψ)中可推出(φ → ψ)和(ψ → φ)。肯定前件（条件除去）：从φ和(φ → ψ)中可推出ψ。条件证明（条件介入）：若假定φ为真可证明出ψ，可推出(φ → ψ)。

以下推导将用编号后的行的列表来表示，在每行之上有一个单一的公式和一个理由（justification）。论证的各个前提会在列表的首行给出。结论将在最后一行。一个推导称为完备的，若所有行都是通过正确的应用一个规则而从前面的行得出的。

下面是（语法上的）证明的一个例子：
要证明：
证明：

编号	公式	理由
1	A	前提
2	A∨A	析取介入自（1）
3	(A∨A)∧A	合取介入自（1）和（2）
4	A	合取除去自（3）
5	A A	总结（1）到（4）
6	A→A	条件证明自（5）

可解释为“假定A，推导出A”。为“不假定任何东西，推导出A蕴涵A”，或者“A蕴涵A是重言式”，或者“A蕴涵A是永真的”。

以上规则的关键特性是它们是可靠的和完备的。非形式的说，这意味着规则都是正确的并且不再需要其他规则。这些要求可以如下这样正式的提出。

我们定义真值指派为把命题变量映射到真或假的函数。非形式的，这种真值指派可以被理解为对事件的可能状态（或可能世界）的描述，在这里特定的陈述是真而其他为假。公式的语义因而可以被形式化，通过定义哪些"事件状态"是设置为真的。

我们通过如下规则定义这种真值指派A在什么时候满足特定公式：

A满足命题变量P 当且仅当A(P) = 真

A满足¬ φ当且仅当A不满足φ

A满足(φ ∧ ψ)当且仅当A满足φ与ψ二者

A满足(φ ∨ ψ)当且仅当A满足φ和ψ中至少一个

A满足(φ → ψ)当且仅当并非A满足φ但不满足ψ的情况

A满足(φ ↔ ψ)当且仅当A满足φ与ψ二者，或则不满足它们中的任何一个

通过这个定义，我们现在可以形式化公式φ被特定公式集合S蕴涵的意义。非形式的，就是在使给定公式集合S成立的所有可能情况下公式φ也成立。这引申出下面的形式化定义：我们说公式集合S 语义蕴涵特定的公式φ，条件是满足在S中的公式的所有真值指派也满足φ。

最后我们定义语法蕴涵，φ被S语法蕴涵，当且仅当我们可以在有限步骤内使用我们提出的上述推理规则推导出它。这允许我们精确的公式化推理规则的可靠性和完备性的意思：

可靠性：如果公式集合S语法蕴涵公式φ，则S语义蕴涵φ完备性：如果公式集合S语义蕴涵公式φ，则S语法蕴涵φ

上述的两个例子都满足可靠性和完备性。

（对于多数逻辑系统，这是相对地“简单的”证明方向）

符号约定：设G是语句集合的变量。设A、B和C是命题变量。我们把“G语法蕴涵A”写成“G证明A”，还有把“G语义蕴涵A”写成“G蕴涵A”。

我们要展示：(∀A)(∀G)(如果G证明A，则G蕴涵A)

我们注意到“G证明A”有一个归纳定义，这给予我们直接的办法来证实“如果G证明A，则……”形式的断言。所以我们的证明是用归纳法进行的。

I.基础。展示：如果A是G的成员则G蕴涵A

II.基础。展示：如果A是公理，则G蕴涵A

III.归纳步骤（对证明的长度n作归纳）

（a）假定对于任意的G和A，如果G在n或更少的步数能证明A，则G蕴涵A。

（b）对于在第n+1步时，从A导出一个新的句子B的每个可能推理规则的应用，展示G蕴涵B。

注意对于自然演绎系统，基础步骤II可以省略，因为它们根本没有公理。基本上，基础步骤II是要展示每个公理都是（语义上的）逻辑真理。

基础步骤证实了对于任何G，来自G的最简单的可证明的语句都被G所蕴涵。（这是简单的，因为集合蕴涵它的任何一个成员，是个平凡的语义事实）。归纳步骤将有系统的覆盖所有的进一步的可证明的句子--通过考虑我们能够使用推理规则达成逻辑结论的每种情况--并展示如果一个新句子是可证明的，它也是在逻辑上被蕴涵的。（例如，可能有一个规则，使得从A可以推导出“A或B”。在III.（a）中我们假定如果A是可证明的则它也是被蕴涵的。我们也知道如果A是可证明的，则“A或B”是可证明的。我们必须展示接着“A或B”也是被蕴涵的。我们求助于语义定义和我们所做的假定来完成。我们假定了A从G是可证明出来的。所以它也被G所蕴涵。所以使G全部为真的任何语义求值也使A为真。此外通过“或”的语义定义，使A为真的任何求值都使“A或B”为真。所以使G的全部为真的任何求值都使“A或B”为真。所以“A或B”被蕴涵了。）一般的，归纳步骤的证明会较长，但不过是对所有推论规则按例分析，去展示每个规则都能“保持”语义蕴涵。

通过可证明性的定义，除了G的成员、公理、或从规则得出的句子之外，没有别的句子是可证明的；所以如果所有这些都是语义上被蕴涵的，则演绎演算是可靠的。

（这通常是相对地困难不少的证明方向。）

我们采用同上面一样的符号约定。

我们要展示：如果G蕴涵A，则G证明A。我们通过反证法来进行：我们转而展示如果G不证明A，则G不蕴涵A。

I. G不证明A。（假定）

II.如果G不证明A，则我们可以构造一个（有限的）"最大化的集合" G*，它是G的超集并且不证明A。

（a）把这个语言中的所有句子上加置一个“次序”。（比如，字母表次序），并把它们编号为E₁, E₂, ...

（b）归纳的定义集合(G₀, G₁, ...)的一个序列G_n为如下。

（i）G₀=G。

（ii）如果G_k ∪ {E_k+1}证明A，则G_k+1=G_k。

（iii）如果G_k ∪ {E_k+1}不证明A，则G_k+1=G_k ∪ {E_k+1}。

（c）定义G* 为所有G_n的并集。（就是说，G* 在任何G_n中的所有句子的集合）

（d）可以容易的展示

（i）G* 包含（是其超集）G（通过(b.i)）；

（ii）G* 不证明A（因为如果它证明A，则某些句子被增加到某个G_n上而导致它证明了A；但是这被定义所排除）；

（iii）G* 是（关于A）"最大化的集合"：如果任何更多的句子不管怎样的被增加到G*，它就会证明A。（因为如果有可能增加任何更多的句子，再次根据定义，在构造G_n期间被遇到的时候它们就应当已经被增加进去了。）

III.如果G* 是（关于A）的最大化集合，则它是"类真理的"。这意味着它包含句子A，只在它不包含非-A的句子的条件下；如果它包含A并且包含“如果A则B”，则它也包含B；以此类推。

IV.如果G* 是类真理的，则有这个语言的“G*-规范”求值：它使在G* 中每个句子为真而在G* 之外的所有句子为假，而仍然遵守在这个语言的语义合成的法则。

V. G*-规范求值将使我们最初的集合G中的句子全部为真，而使A为假。

VI.如果有在G其上是真而A是假的赋值，则G 不（语义上）蕴涵A。Q.E.D.

下面定义的命题演算通过公理的方式定义了多数逻辑算子的语法并且它只使用一个推理规则。它也叫做标准命题演算。

设φ、χ和ψ表示合式公式。（wff自身将不包含任何希腊字母，而只包含大写罗马字母、链接算子和圆括号）。公理有

THEN-1：φ →(χ → φ)

THEN-2：(φ → (χ → ψ)) →((φ → χ)→(φ → ψ))

AND-1：φ ∧ χ → φ

AND-2：φ ∧ χ → χ

AND-3：φ →(χ → (φ ∧ χ))

OR-1：φ → φ ∨ χ

OR-2：χ → φ ∨ χ

OR-3：(φ → ψ)→((χ → ψ)→(φ ∨ χ → ψ))

NOT-1：(φ → χ)→((φ → ¬ χ)→ ¬ φ)

NOT-2：φ →(¬ φ → χ)

NOT-3：φ ∨ ¬ φ

公理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。

推理规则是肯定前件：

.

如果还使用双箭头的等价算子的话，则要增加如下"自然"推理规则：

IFF-1：

IFF-2：

设一个推导被表示为相继式，各个假设在十字转门（turnstile）的左侧，而结论在十字转门的右侧。则演绎定理可以被陈述如下：

如果相继式

已经被证明了，则也有可能证明相继式

。

这个演绎定理（DT）自身没有公式化为命题演算：它不是命题演算的定理，而是关于命题演算的一个定理。在这个意义上，它是元定理，相当于关于命题演算可靠性和完备性的定理。

在另一方面，DT对于简化语法上的证明过程是如此的有用以至于它看作和用做推理规则，同肯定前件一起使用。在这个意义上，DT对应于自然条件证明推理规则，它是在本条目中提出的第二个例子的命题演算的一部分。

DT的逆定理也是有效的：

如果相继式

已经被证明了，则也有可能证明相继式

实际上，DT的逆定理的有效性相对于DT而言是平凡的：

如果

则

1：

2：

并且可以演绎自（1）和（2）

3：

通过肯定前件的方式，Q.E.D.

DT的逆命题有着强有力的蕴涵：它可以用来把公理转换成推理规则。例如，公理AND-1

可以通过演绎定理的逆定理的方式被转换成推理规则

这是合取除去，是前面给出的自然演绎命题演算中使用的十个推理规则中的一个。

下面是（语法上）证明的一个例子，只涉及到公理THEN-1和THEN-2：
要证明：A → A（蕴涵的自反性）。
证明：

1.(A → ((B → A)→ A)) →((A → (B → A)) →(A → A))

公理THEN-2通过φ = A, χ = B → A, ψ = A

2. A →((B → A)→ A)

公理THEN-1通过φ = A, χ = B → A

3.(A → (B → A)) →(A → A)

得自（1）和（2）通过肯定前件。

4. A →(B → A)

公理THEN-1通过φ = A, χ = B

5. A → A

得自（3）和（4）通过肯定前件。

如果公式是重言式，则它有展示对每个赋值的这个公式生成的值都是真的一个真值表。考虑这样一个求值。通过在子公式长度上的数学归纳法，展示从在子公式中的每个命题变量（适合这个求值）的真或假推出子公式的真或假。接着使用“(P为真→S)→((P为假→ S)→S)”一次两行的合并真值表的行到一起。持续重复这个过程直到对命题变量的所有依赖都除去了。结果是我们证明了这个重言式。因为所有重言式都是可证明的，逻辑是完备的。

前面的公理化命题演算是希尔伯特风格演绎系统的一个例子。在这种命题系统中公理是用逻辑链接词构建的项，而唯一的推理规则是肯定前件。等式逻辑在高等学校的抽象代数教学中被作为正式的标准，它是不同于希尔伯特系统的一类不同的演算。它的定理是等式而它的推理规则表达出等号的性质，也就是在容许代换的项上的相等关系。

上述的经典命题演算等价于布尔代数，而直觉命题演算等价于海廷代数。等价性是通过在两个方向上转换各自系统的定理来证明的。经典命题演算或直觉命题演算的定理Φ被分别转换为布尔代数或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。不等式的重要性在于它对应于希尔伯特系统的演绎或蕴涵符号。蕴涵

被转换为代数框架下的不等式

反过来代数不等式x ≤ y被转换为蕴涵

在实质条件（implication）x → y和不等式或者蕴涵（entailment）x ≤ y或之间的区别在于，前者是内在于逻辑的，而后者是外在的。在两个项之间内在的实质条件是同类的另一个项。在两个项之间的外在的蕴涵表达了在逻辑语言之外的元真理，并被认为是元语言的一部分。即使所研究的逻辑是直觉的，蕴涵都通常经典的理解为二值的：要么左侧蕴涵（或小于等于）右侧，要么不蕴涵之。

同代数逻辑之间类似但更加复杂的相互转换，对于自然演绎系统和相继式演算也是可能的。后者的转换可以被释义为二值的，但是更有洞察力的释义是作为集合，它的元素可以被理解为由范畴的态射组成的抽象证明。在这种释义下相继式演算的切规则对应于范畴的复合。