命题逻辑是指以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。相对于谓词逻辑，它是量化的并且它的原子公式是谓词函数；和模态逻辑，它可以是非真值泛函的。演算是用来证明有效的公式（就是说它的定理）和论证（argument）的逻辑系统。它是公理或公理模式的集合（它可以为空或是可数无限集合），和推导有效的推理的推理规则。形式文法（或语法）递归定义语言的表达式和合式公式（well-formed formula经常缩写为wff）。此外给出定义真值和求值（或释义）的语义。它允许人们确定哪个wff是有效的（也就是定理）。

在命题演算中语言由命题变量（或者叫占位符（placeholder））和句子/判决算子（或者叫连结词）。wff是任何原子公式或在句子操作符之上建造的公式。在下文中我们描述一种标准命题演算。很多不同的公式系统存在，它们都或多或少等价但在下列方面不同：

⑴它们的语言（就是说哪些操作符和变量是语言的一部分）；

⑵它们有哪些（如果有的话）公理；

⑶采用了哪些推理规则。

语言的构成：

字母表的大写字母，表示命题变量。它们是原子公式。惯例上，使用拉丁字母（A,B,C）或希腊字母（χ，φ，ψ），但是不能混合使用。

表示连结词（connective)（或逻辑算子）的符号：¬；、∧、∨、→、?。（我们可以使用更少的算子（和相应的符号），因为一些算子是简写形式—例如，P→Q等价于¬P∨Q）。

左右圆括号：（，）。

合式公式（wff）的集合右如下规则递归的定义：

基础：字母表的字母（通常是大写的，如A、B、φ、χ等）是wff。

归纳条款I:如果φ是wff，则¬φ是wff。

归纳条款Ⅱ如果φ和ψ是wff，则（φ∧ψ）、（φ∨ψ）、（φ→ψ）和（φψ）是wff。

闭包条款：其他东西都不是wff。

重复的应用这三个公式允许生成复杂的wff。例如：

通过规则1，A是wff。

通过规则2，¬A是wff。

通过规则1，B是wff。

通过规则3，（¬A∨B)是wff。

为了简单化，我们使用自然演绎系统，它没有公理；或者等价的说，它有空的公理集合。

使用我们的演算的推导将用编号后的行的列表，在每行之上有一个单一的wff和一个理由（justification）的形式展示出来。任何前提（premise）都在上部，并带有"p"作为它们的断定。结论将在最后一行。推导将被看作完备的，条件是所有行都是通过正确的应用一个规则而从前面的行得出的。

公理集合是空集。

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

双重否定除去

从wff¬¬φ，我们可以推出φ。

合取介入

从任何wffφ和任何wffψ，我们可以推出（φ∧ψ）。

合取除去

从任何wff（φ∧ψ），我们可以推出φ和ψ。

析取介入

从任何wffφ，我们可以推出（φ∨ψ）和（ψ∨φ），这里的ψ是任何wff。

析取除去

从（φ∨ψ）、（φ→χ）和（ψ→χ）形式的wff，我们可以推出χ。

双条件介入

从（φ→ψ）和（ψ→φ）形式的wff，我们可以推出（φψ）。

双条件除去

从wff（φψ），我们可以推出（φ→ψ）和（ψ→φ）。

肯定前件

从φ和（φ→ψ）形式的wff，我们可以推出ψ。

条件证明

如果在假定假设φ的时候可以推导出ψ，我们可以推出（φ→ψ）。

反证证明

如果在假定假设φ的时候可以推导出ψ和¬ψ，我们可以推出¬φ。

规则的可靠性和完备性

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

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

我们通过如下规则定义这种真值A在什么时候满足特定wff:

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

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

A满足（φ∧ψ）当且仅当A满足φ与ψ二者

A满足（φ∨ψ）当且仅当A满足φ和ψ中至少一个

A满足（φ→ψ）当且仅当没有A满足φ但不满足ψ的事例

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

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

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

可靠性

如果wff集合S语法蕴涵wffφ，则S语义蕴涵φ

完备性

如果wff集合S语义蕴涵wffφ，则S语法蕴涵φ

对上述规则集合这些都成立。

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

符号约定：设"G"是涉及语句集合的变量。设"A"、"B"和"C"是涉及句子的变量。我们把"G语法蕴涵A"写成"G证明A"。我们把"G语义蕴涵A"写成"G蕴涵A"。

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

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

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

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

Ⅲ.归纳步骤：(a)假定对于任意的G和A，如果G证明A则G蕴涵A。（如果需要的话，对B、C等做同样的假定）

（b)对于针对A的推论的规则的，导出一个新的句子B的每个可能的应用，展示G蕴涵B。

（N.B.对于上述演算基础步骤Ⅱ可以省略，它是自然演绎系统而没有公理。基本上，它涉及展示每个公理都是（语义上）逻辑真理。）

基础步骤证实了对于任何G来自G的最简单的可证明的语句都被G所蕴涵。（这是简单的，因为集合蕴涵它的任何一个成员是语义事实，这是平凡的（trivial））。归纳步骤将有系统的覆盖所有的进一步的可证明的句子--通过考虑我们能够使用推理规则达成逻辑结论的每种情况--并展示如果一个新句子是可证明的，它也是在逻辑上被蕴涵的。（例如，我们可能有一个告诉我们从"A"可以推导出"A或B"。在Ⅲ.(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。（假定）

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

（a）在这个语言的所有句子上加置一个"次序"。（比如，字母表次序），并把它们编号为E1,E2,...

（b）归纳的定义集合（G0,G1...）的一个序列（series)Gn为如下(i)G0=G。（ii)如果{Gk,E(k+1）}证明A，则G(k+1）=Gk。（iii)如果{Gk,E(k+1）}不证明A，则G(k+1）={Gk,E(k+1）}

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

（d)可以容易的展示(i)G*包含（是其超集）G（通过(b.i））；（ii)G*不证明A（因为如果它证明A则某些句子被增加到某个Gn上而导致它证明了A;但是这被定义所排除）；和(iii)G*是（关于A)"最大化的集合":如果任何更多的句子不管怎样的被增加到G*，它就会证明A。（因为如果有可能增加任何更多的句子，再次根据定义，在构造Gn期间被遇到的时候它们就应当已经被增加进去了。）

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

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

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

Ⅵ.如果有在其上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叫做"排中律"（拉丁语tertiumnondatur:"排除第三者")并反映了命题公式的语义求值：公式可以有的真值要么是真要么是假。至少在经典逻辑中，没有第三个真值。直觉逻辑不接受公理NOT-3。

推理规则

推理规则是肯定前件：

\u003c数学\u003e\phi,\\phi\rightarrow\chi\vdash\chi\u003c/math\u003e.

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

IFF-1:\u003cmath\u003e\phi\leftrightarrow\chi\vdash\chi\rightarrow\phi\u003c/math\u003e

IFF-2:\u003cmath\u003e\phi\rightarrow\chi,\\chi\rightarrow\phi\vdash\phi\leftrightarrow\chi\u003c/math\u003e

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

如果相继式

\u003c数学\u003e\phi_1,\\phi_2,\...,\\phi_n,\\chi\vdash\psi\u003c/math\u003e

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

\u003cmath\u003e\phi_1,\\phi_2,\...,\\phi_n\vdash\chi\rightarrow\psi\u003c/math\u003e；。

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

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

DT的逆定理也是有效的：

如果相继式

\u003c数学\u003e\phi_1,\\phi_2,\...,\\phi_n\vdash\chi\rightarrow\psi\u003c/math\u003e

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

\u003cmath\u003e\phi_1,\\phi_2,\...,\\phi_n,\\chi\vdash\psi\u003c/math\u003e

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

如果

\u003cmath\u003e\phi_1,\...,\\phi_n\vdash\chi\rightarrow\psi\u003c/math\u003e

则

1:\u003c数学\u003e\phi_1,\...,\\phi_n,\\chi\vdash\chi\rightarrow\psi\u003c/math\u003e

2:\u003cmath\u003e\phi_1,\...,\\phi_n,\\chi\vdash\chi\u003c/math\u003e

并且可以演绎自⑴和⑵

3:\u003cmath\u003e\phi_1,\...,\\phi_n,\\chi\vdash\psi\u003c/math\u003e

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

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

\u003c数学\u003e\vdash\phi\wedge\chi\rightarrow\phi\u003c/math\u003e

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

\u003cmath\u003e\phi\wedge\chi\vdash\phi\u003c/math\u003e

这是合取除去，是（在本文中）第一个版本的命题演算中使用的十个推理规则中的一个。

证明的例子

下面是（语法上）证明的一个例子，只涉及到公理THEN-1和THEN-2:

要证明：A→A（蕴涵的自反性）。

证明：

⒈(A→((A→A)→A))→((A→(A→A))→(A→A))

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

⒉A→((A→A)→A)

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

⒊(A→(A→A))→(A→A)

得自⑴和⑵通过肯定前件。

⒋A→(A→A)

公理THEN-1通过φ=A，χ=A

⒌A→A

得自⑶和⑷通过肯定前件。