命题逻辑是指以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。相对于谓词逻辑，它是量化的并且它的原子公式是谓词函数；和模态逻辑，它可以是非真值泛函的。

在命题演算中语言由命题变量（或者叫占位符（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。

我们的命题演算有十个推理（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 语法蕴涵 φ

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

为了简单化，我们使用自然演绎系统，它没有公理；或者等价的说，它有空的公理集合。 使用我们的演算的推导将用编号后的行的列表，在每行之上有一个单一的 wff 和一个理由（justification）的形式展示出来。任何前提（premise

（对于多数逻辑系统

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

归纳定义，这给予我们直接的办法来证实（demonstrate归纳法进行的。

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 蕴涵 A，则 G 证明 A。我们通过反证法来进行： 我们转而展示如果 G 不证明 A，则 G 不蕴涵 A。

I. 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 中的所有句子的集合）。

composition）的法则。

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

Ⅵ. 如果有在其上 G 是真而 A 是假的求值，则 G 不（语义上）蕴涵 A。

可供选择的演算

有可能定义其他版本的命题演算，它通过公理的方式定义了多数逻辑算子的语法，并且它只使用一个推理规则。

公理

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

THEN-1: φ → （χ → φ）

THEN-2: （φ → （χ → ψ）） → （（φ → χ） → （φ → ψ））

AND-1: φ ∧ χ → φ

AND-2: φ ∧ χ → χ

AND-3: φ → （χ → （φ ∧ χ））

OR-1: φ → φ ∨ χ

OR-2: χ → φ ∨ χ

OR-3: （φ → ψ） → （（χ → ψ） → （φ ∨ χ → ψ））

NOT-1: （φ → χ） → （（φ → ¬ χ） → ¬ φ）

NOT-2: φ → （¬ φ → χ）

NOT-3: φ ∨ ¬ φ

排中律拉丁语命题公式的语义求值： 公式可以有的真值要么是真要么是假。至少在经典逻辑中，没有第三个真值。直觉逻辑不接受公理NOT-3。

推理规则

推理规则是肯定前件：

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

如果相继式

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

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

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

DT 的逆定理也是有效的：

如果相继式

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

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

如果

则

并且可以演绎自 ⑴ 和 ⑵

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

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

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

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

证明的例子

下面是（语法上）证明的一个例子，只涉及到公理 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

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