Agda命题逻辑(1) 希尔伯特系统

交流Q群: 893531731
目录: Everything.html
本文源码: Hilbert.lagda.md
高亮渲染: Hilbert.html
如果你在知乎看到本文: 知乎对Agda语法高亮的支持非常有限, 建议跳转到以上网站阅读

0 前言

本文以 Agda 为元语言, 建立希尔伯特风格的命题逻辑系统.
我们默认读者熟悉 Agda 及其标准库.
除去代码部分, 本文尽可能以传统数理逻辑入门书的风格撰写.

{-# OPTIONS --without-K --safe #-}

module Hilbert where

标准库依赖

open import Data.Bool using (Bool; true; false; not)
open import Data.Bool.Properties renaming (not-injective to not-inj)
open import Data.Nat using (ℕ)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; ∃-syntax)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

符号优先级

本文所采用的符号及其优先级列举如下. 它们的具体定义会在正文讲解.

infix 20 ~_
infixr 15 _⊃_
infixl 15 _+_
infix 10 _|≟_ _⊨ₘ_
  _⊨ᵥ_ _⊭ᵥ_ ⊨ᵥ_ ⊭ᵥ_
  _⊨_  _⊭_  ⊨_  ⊭_
  _⊢_  _⊬_  ⊢_  ⊬_

1 公式

在命题逻辑中, 我们认为命题的最基本的构成要素是一些不可再分的原子命题, 我们需要一些符号来表示它们.

〔定义1.1〕 设 Variable 为非空集合, Variable 的元素叫做命题变元 (propositional variable).

很难再进一步解释何为命题变元, 只需认为它们是一些可以相互区分_ 对应于我们的构造主义元逻辑中的 decidable equality

的符号就足够了. 形式地, 简单起见, 不妨以自然数集为 Variable.

Variable = ℕ

逻辑运算符 (propositional connective) 用于连接已有的命题得到新的命题. 命题逻辑一般使用「非, 且, 或, 如果…那么…」这四种, 分别记作 ¬, ∧, ∨, →. 然而, 这四种并不是相互独立的. 例如, 在一般数学中,「A且B」与「非A或非B」同义, 「如果A那么B」与「非A, 或B」同义_ 若有违和感, 都是自然语言的锅. 数学中的「如果…那么…」仅取分情况讨论之义, 而自然语言中并不是只有这一种用法.

, 因此只需要「非, 或」这两种就足够了. 类似地, 用「非, 如果…那么…」这两种也可以表示「且」和「或」. 简单起见我们只使用「非, 如果…那么…」这两种. 由于与元语言符号冲突, 我们采用复古符号 ~ 和 ⊃.

〔定义1.2〕 命题变元以及用逻辑运算符将它们按一定规则连接在一起得到的式子叫做公式 (formula), 也叫逻辑表达式. 具体地

如果 n 是命题变元, 那么 var n 是公式.
如果 φ 是公式, 那么 ~ φ 也是公式.
如果 φ 和 ψ 是公式, 那么 φ ⊃ ψ 也是公式.
只有符合以上规则的才是公式.

data Formula : Set where
  var : Variable → Formula
  ~_ : Formula → Formula
  _⊃_ : Formula → Formula → Formula

【注意1.3】 非形式地, 可以认为单独的命题变元就是公式. 形式地, 需要 var 将 Variable 类型转换成 Formula 类型.

【注意1.4】 有些书会说括号也是公式的一部分, 只是在无歧义的情况下可以省略. 本文实际上也是如此. 例如 ~ φ 是 (~ φ) 的省略. 这是元语言规则的一部分. 我们有文章开头处声明的符号优先级来决定 _~_ 和 _⊃_ 交互时如何省略括号. 例如, 由于 _~_ 的优先级比 _⊃_ 高, ~ A ⊃ B 与 (~ A) ⊃ B 同义, 而与 ~ (A ⊃ B) 不同. 后文其他符号的交互也类似. 此外, 按元语言的惯例, 我们约定 _⊃_ 是右结合. 例如, φ ⊃ ψ ⊃ φ 表示 φ ⊃ (ψ ⊃ φ).

【注意1.5】 即使公式表示了命题, 将公式与命题联系起来的还是人, 公式只是单纯的符号串. 可以认为, 命题是哲学对象而非数学对象, 符号串才是数学对象. 公式与命题的区分是数理逻辑特有的思考方式, 也是作为数学的数理逻辑的出发点.

【注意1.6】 形如1.2的定义也叫归纳定义. 如果要证明所有公式都具有某个性质 P, 按公式的归纳定义只需证明以下3条:

对任意 n, var n 满足 P.
如果 φ 满足 P, 那么 ~ φ 满足 P.
如果 φ 和 ψ 满足 P, 那么 φ ⊃ ψ 满足 P.

这种形式的证明叫做关于公式复杂度的归纳法.

后面为了行文的方便可能会将以下概念混同, 我们在此统一澄清它们的区分.

哲学	数理逻辑	形式化
原子命题	命题变元	`Variable`
逻辑运算	¬, →	`~_`, `_⊃_`
命题	公式	`Formula`

2 真值

由上一节我们知道, 公式是形式地表示命题的符号串. 而命题是可以确定真假的数学主张, 我们还需要建立公式与真假的联系. 由于命题是原子命题与逻辑运算符的组合, 且逻辑运算符的语义是明确的, 只要确定了原子命题的真假就可以确定所有命题的真假. 又, 原子命题由命题变元表示, 命题由公式表示. 于是只要确定了命题变元的真假就可以确定所有公式的真假. 我们认为命题变元可以用如下方式规定它们的真假.

〔定义2.1〕 (1) 可以相互区分的两个符号 true 和 false 叫做真值. 其中 true 表示真, false 表示假.
(2) 从命题变元全体的集合 Variable 到真值的集合 Bool 的函数叫做真值指派 (truth assignment), 也叫赋值 (valuation) 或指派 (assignment). 真值指派全体的集合叫做 Assignment.

Assignment = Variable → Bool

给定真值指派 v, 按逻辑运算符的语义, 从简单公式到复杂公式的真值就顺次确定了. 例如将命题变元 0 指派为真, 那么公式 ~ (var 0) 就应该估值为假. 具体地

〔定义2.2〕 给定真值指派 v, 公式 φ 的真值 v |≟ φ 归纳定义如下:

v |≟ (var n) 的值与 v n 相同.
v |≟ ~ φ 的值与 v |≟ φ 相反.
如果 v |≟ φ 为 true 且 v |≟ ψ 为 false, 那么 v |≟ φ ⊃ ψ 为 false. 除此之外 v |≟ φ ⊃ ψ 都为 true.

_|≟_ : Assignment → Formula → Bool
v |≟ (var n) = v n
v |≟ ~ φ = not (v |≟ φ)
v |≟ φ ⊃ ψ with v |≟ φ | v |≟ ψ
...           | true   | false  = false
...           | _      | _      = true

〔定义2.3〕 给定真值指派 v 和公式 φ. 当 v |≟ φ 为 true 时我们说 φ 在 v 下为真, 记作 v ⊨ᵥ φ. 当 v |≟ φ 为 false 时我们说 φ 在 v 下为假, 记作 v ⊭ᵥ φ.

_⊨ᵥ_ : Assignment → Formula → Set
v ⊨ᵥ φ = v |≟ φ ≡ true

_⊭ᵥ_ : Assignment → Formula → Set
v ⊭ᵥ φ = v |≟ φ ≡ false

由定义, 以下引理显然成立.

[引理2.4] v ⊨ᵥ ~ φ 等价于 v ⊭ᵥ φ.

v⊨~φ⇒v⊭φ : ∀ v φ → v ⊨ᵥ ~ φ → v ⊭ᵥ φ
v⊨~φ⇒v⊭φ v φ v⊨~φ = not-inj v⊨~φ

v⊭φ⇒v⊨~φ : ∀ v φ → v ⊭ᵥ φ → v ⊨ᵥ ~ φ
v⊭φ⇒v⊨~φ v φ v⊭φ rewrite v⊭φ = refl

[引理2.5] v ⊨ᵥ φ 和 v ⊭ᵥ φ 中有且只有一个成立.

v⊨φ⊎v⊭φ : ∀ v φ → v ⊨ᵥ φ ⊎ v ⊭ᵥ φ
v⊨φ⊎v⊭φ v φ with v |≟ φ
...            | true  = inj₁ refl
...            | false = inj₂ refl

v⊨φ⇒v⊭φ⇒⊥ : ∀ v φ → v ⊨ᵥ φ → v ⊭ᵥ φ → ⊥
v⊨φ⇒v⊭φ⇒⊥ v φ v⊨φ v⊭φ rewrite v⊨φ with v⊭φ
... | ()

〔定义2.6〕 给定 φ, 对任意 v 都有 v ⊨ᵥ φ 时, 我们就说 φ 是恒真式 (tautological formula), 也叫重言式, 记作 ⊨ᵥ φ. 存在 v 使得 v ⊭ᵥ φ 时, 我们说 φ 不是恒真式, 记作 ⊭ᵥ φ.

⊨ᵥ_ : Formula → Set
⊨ᵥ φ = ∀ v → v ⊨ᵥ φ

⊭ᵥ_ : Formula → Set
⊭ᵥ φ = ∃[ v ] v ⊭ᵥ φ

【注意2.7】 ⊨ᵥ φ 与 ⊨ᵥ ~ φ 并非必有一个成立. 例如当 φ 为命题变元 var n 时, 可以构造 v₁ 使得 v₁ n 为真, v₂ 使得 v₂ n 为假. 此时既没有 ⊨ᵥ (var n) 也没有 ⊨ᵥ ~ (var n). 此外, ⊨ᵥ φ 与 ⊨ᵥ ~ φ 不能同时成立.

由恒真式表示的命题叫做恒真命题. 恒真命题是不依赖于原子命题真假的, 仅依靠命题本身的形式就可判断为真的命题.

[引理2.8] 以下三条公式是恒真式.

φ ⊃ ψ ⊃ φ
(φ ⊃ ψ ⊃ ρ) ⊃ (φ ⊃ ψ) ⊃ (φ ⊃ ρ)
(~ φ ⊃ ~ ψ) ⊃ ψ ⊃ φ

证明: 可以通过真值表来确定一个公式是不是恒真式. 例如, 对公式 φ ⊃ (ψ ⊃ φ) 有

φ	ψ	ψ ⊃ φ	φ ⊃ (ψ ⊃ φ)
true	true	true	true
true	false	true	true
false	true	false	true
false	false	true	true

Agda 的证明与真值表有类似的形式. 另外两条公式的证明也是类似的. ∎

Tauto1 : ∀ φ ψ → ⊨ᵥ φ ⊃ ψ ⊃ φ
Tauto1 φ ψ v with v |≟ φ | v |≟ ψ
...             | true   | true  = refl
...             | true   | false = refl
...             | false  | true  = refl
...             | false  | false = refl

Tauto2 : ∀ φ ψ ρ → ⊨ᵥ (φ ⊃ ψ ⊃ ρ) ⊃ (φ ⊃ ψ) ⊃ (φ ⊃ ρ)
Tauto2 φ ψ ρ v with v |≟ φ | v |≟ ψ | v |≟ ρ
...               | true   | true   | true  = refl
...               | true   | true   | false = refl
...               | true   | false  | true  = refl
...               | true   | false  | false = refl
...               | false  | true   | true  = refl
...               | false  | true   | false = refl
...               | false  | false  | true  = refl
...               | false  | false  | false = refl

Tauto3 : ∀ φ ψ → ⊨ᵥ (~ φ ⊃ ~ ψ) ⊃ ψ ⊃ φ
Tauto3 φ ψ v with v |≟ φ | v |≟ ψ
...             | true   | true  = refl
...             | true   | false = refl
...             | false  | true  = refl
...             | false  | false = refl

【注意2.9】 对任意公式, 都有确定性 (deterministic) 步骤可以写出其真值表. 但是, 对含 n 个命题变元的公式需要写 2ⁿ 行. 当 n 很大时需要花费很长的时间才能判断其真值. 真值的计算是确定性的但低效的.

3 理论

由上一节我们知道, 一旦确定了真值指派 v, 所有真命题的集合也随之确定. 但在数理逻辑的实践中, 我们一般是反过来, 先确定一些命题, 然后找到某些 v 使得这些命题为真.

〔定义3.1〕 公式的集合, 即 Formula 的子集叫做理论 (theory). 理论的元素叫做非逻辑公理 (nonlogical axiom). 特别地, 空集 ∅ 也是理论.

Theory = Formula → Set

∅ : Theory
∅ _ = ⊥

给定理论 T. T 的非逻辑公理有时就简称为公理 (axiom). 理论又叫形式理论 (formal theory) 或公理系统 (axiom system). 给定公式 φ 和 ψ, 由它们组成的理论记作 ｛ φ , ψ ｝.

｛_,_｝ : Formula → Formula → Theory
｛ φ , ψ ｝ ξ = ξ ≡ φ ⊎ ξ ≡ ψ

用 φ 扩张理论 T 得到的理论记作 T + φ.

_+_ : Theory → Formula → Theory
(T + φ) ξ = T ξ ⊎ ξ ≡ φ

〔定义3.2〕 给定真值指派 v 和理论 T. 当任意 φ ∈ T 都有 v ⊨ᵥ φ 时, 我们就说这个 v 是 T 的模型, 记作 v ⊨ₘ T.

_⊨ₘ_ : Assignment → Theory → Set
v ⊨ₘ T = ∀ φ → T φ → v ⊨ᵥ φ

【注意3.3】 如本节开头所说, 理论将间接地确定可能的模型 (虽然不一定唯一确定, 甚至可能不存在模型). 像这样由非逻辑公理的集合来确定模型的做法叫做公理化定义 (axiomatic definition). 承认公理化定义为一种定义是继承了希尔伯特形式主义思想的现代数学的一大特征.

【注意3.4】 Theory 可以认为是对朴素意义的理论的一种过度的一般化. 随意给定的一个 T : Theory 大概率是没有模型的. 过去提出的各种某某理论也大多淹没在历史之中. 而且寻找新的理论并不是命题逻辑 (乃至谓词逻辑) 的目的, 而只是其中一个应用, 何况有时是滥用.

〔定义3.5〕 给定理论 T 和公式 φ. 对 T 的任意模型 v 都有 v ⊨ᵥ φ 时, 我们就说 φ 是 T 的逻辑蕴涵 (logical consequence), 也叫语义蕴涵 (semantic consequence), 记作 T ⊨ φ. 存在 T 的模型 v 使得 v ⊭ᵥ φ 时, 我们就说 φ 不是 T 的逻辑蕴涵, 记作 T ⊭ φ.

_⊨_ : Theory → Formula → Set
T ⊨ φ = ∀ v → v ⊨ₘ T → v ⊨ᵥ φ

_⊭_ : Theory → Formula → Set
T ⊭ φ = ∃[ v ] v ⊨ₘ T × v ⊭ᵥ φ

∅ ⊨ φ 简记作 ⊨ φ, ∅ ⊭ φ 简记作 ⊭ φ.

⊨_ : Formula → Set
⊨ φ = ∅ ⊨ φ

⊭_ : Formula → Set
⊭ φ = ∅ ⊭ φ

由定义立即有以下事实.

[事实3.6] 对任意 φ, ⊨ᵥ φ 当且仅当 ⊨ φ.

⊨ᵥ⇒⊨ : ∀ φ → ⊨ᵥ φ → ⊨ φ
⊨ᵥ⇒⊨ φ ⊨ᵥφ v _ = ⊨ᵥφ v

⊨⇒⊨ᵥ : ∀ φ → ⊨ φ → ⊨ᵥ φ
⊨⇒⊨ᵥ φ ⊨φ v = ⊨φ v λ _ ()

⟨例3.7⟩ 给定命题变元 A 和 B. B 是理论 ｛ A , A ⊃ B ｝ 的逻辑蕴涵.

module _ (m n : Variable) where
  private A = var m
  private B = var n

  ｛A,A⊃B｝⊨B : ｛ A , A ⊃ B ｝ ⊨ B
  ｛A,A⊃B｝⊨B v v⊨ with v m   | v n  | v⊨ A (inj₁ refl) | v⊨ (A ⊃ B) (inj₂ refl)
  ...                | _     | true | _                | _ = refl
  ...                | false | _    | ()               | _

【注意3.8】 跟 ⊨ᵥ φ 与 ⊨ᵥ ~ φ 一样, T ⊨ φ 与 T ⊨ ~ φ 也并非必有一个成立. 然而, 如果 T 没有模型, 那么对任意 φ 都有 T ⊨ φ. 此时有 T ⊨ φ 和 T ⊨ ~ φ 同时成立.

_ : ∀ T → (∀ v → ¬ v ⊨ₘ T) → ∀ φ → T ⊨ φ
_ = λ T ¬v⊨T φ v v⊨T → ⊥-elim (¬v⊨T v v⊨T)

[引理3.9] 给定真值指派 v, 理论 T 和公式 φ, 以下 (1) 和 (2) 等价.

v 是 T + φ 的模型.
v 是 T 的模型且 φ 在 v 下为真.

+-elimˡ : ∀ {v T} φ → v ⊨ₘ T + φ → v ⊨ₘ T
+-elimˡ φ v⊨ ψ ψ∈T = v⊨ ψ (inj₁ ψ∈T)

+-elimʳ : ∀ {v T} φ → v ⊨ₘ T + φ → v ⊨ᵥ φ
+-elimʳ φ v⊨ = v⊨ φ (inj₂ refl)

+-intro : ∀ {v T} φ → v ⊨ₘ T → v ⊨ᵥ φ → v ⊨ₘ T + φ
+-intro φ v⊨T v⊨φ ψ (inj₁ ψ∈T)  = v⊨T ψ ψ∈T
+-intro φ v⊨T v⊨φ ψ (inj₂ refl) = v⊨φ

[引理3.10] 对任意公式 φ, 以下 (1) 和 (2) 等价.

T + ~ φ 有模型.
φ 不是 T 的逻辑蕴涵.

证明: 由引理3.9显然成立. ∎

v⊨T+~φ⇒T⊭φ : ∀ v T φ → v ⊨ₘ T + ~ φ → T ⊭ φ
v⊨T+~φ⇒T⊭φ v T φ v⊨ = v , v⊨T , v⊭φ where
  v⊨T = +-elimˡ (~ φ) v⊨
  v⊭φ = v⊨~φ⇒v⊭φ v φ (+-elimʳ (~ φ) v⊨)

T⊭φ⇒v⊨T+~φ : ∀ T φ → T ⊭ φ → ∃[ v ] v ⊨ₘ T + ~ φ
T⊭φ⇒v⊨T+~φ T φ (v , v⊨T , v⊭φ) = v , +-intro (~ φ) v⊨T v⊨~φ where
  v⊨~φ = v⊭φ⇒v⊨~φ v φ v⊭φ

4 证明

我们讲了命题逻辑的公式, 真值, 理论等基本概念, 这节我们来讲何为证明. 由前几节我们知道, 一旦确定了公式的定义以及真值指派下的公式真值的计算方式, 恒真式全体的集合也就随之确定. 再次运用原子论或者说还原主义的思想, 我们认为恒真式也可以分为基本的和派生的两部分. 其中基本的恒真式叫做逻辑公理 (logical axiom).

另一方面, 给定公式的有限序列 R = φ₁, φ₂, …, φₙ, φ. 对任意真值指派 v 都有 v ⊨ᵥ φ₁, v ⊨ᵥ φ₂, …, v ⊨ᵥ φₙ 蕴涵 v ⊨ᵥ φ 时, 我们就说 R 是从前提 φ₁, φ₂, …, φₙ 到结论 φ 的演绎推理 (deductive inference). 原则上, 数学证明所采用的推理必须是演绎推理, 而只要是演绎推理, 那么采用何种推理都无关紧要. 这里, 再次运用原子论的思想, 我们认为有一些基本的演绎推理, 叫做推理规则 (inference rule).

逻辑公理和推理规则合起来称为命题逻辑系统 \mathfrak{S}. 给定系统 \mathfrak{S} 和理论 T, 系统中的「证明」和「定理」定义如下.

〔定义4.1〕 对公式的有限序列 R = φ₁, φ₂, …, φₙ 中每一个公式 φᵢ 都有以下 (1) ~ (3) 的任意一个成立时, 我们就说 R 是在理论 T 中对 φₙ 的证明 (proof).

φᵢ 是 \mathfrak{S} 的逻辑公理.
φᵢ ∈ T
存在 \mathfrak{S} 的推理规则, 其前提都在 R 中且其结论是 φᵢ.

此时我们说 φₙ 是 T 的定理 (theorem), 也说 φₙ 在 T 中可证 (provable), 记作 T ⊢ φₙ. 特别地, ∅ ⊢ φ 时我们说 φ 是 \mathfrak{S} 的定理, 简记作 ⊢ φ.

到目前为止, 我们并没有说逻辑公理和推理规则具体有哪些. 实际上, 数理逻辑的历史上提出了许多方案, 构成了多种命题逻辑系统. 代表性的有希尔伯特流, 根岑的自然演绎 NK 和 LK, Fitch流等等. 这些系统对于证明的定义都有一些微妙的区别, 且各有一些优缺点. 大体来说, 如果希望逻辑公理尽可能得少, 那么就不得不采用较多的推理规则, 此类系统的极致是自然演绎. 反过来, 如果希望推理规则尽可能得少, 那么就不得不采用较多的逻辑公理, 此类系统的极致就是希尔伯特流.

不管哪种系统, 系统中可证的公式的集合, 也即系统中定理的集合, 与恒真式的集合都是相吻合的. 可证性, 也即证明的存在性和非存在性与逻辑系统的选取无关. 本文接下来介绍的系统属于希尔伯特流的一种, (仅在本文中) 记作 \mathfrak{S}_0. 具体地

〔定义4.2〕 \mathfrak{S}_0 有且只有以下3条逻辑公理:

Ax1 : φ ⊃ ψ ⊃ φ
Ax2 : (φ ⊃ ψ ⊃ ρ) ⊃ (φ ⊃ ψ) ⊃ (φ ⊃ ρ)
Ax3 : (~ φ ⊃ ~ ψ) ⊃ ψ ⊃ φ

\mathfrak{S}_0 有且只有以下称为肯定前件 (Modus ponens) 的推理规则 MP: \dfrac{φ\;\;φ ⊃ ψ}{ψ} \\

结合定义4.1和4.2, \mathfrak{S}_0 中的可证关系 _⊢_ 的形式化如下. 如定义4.1所说, T ⊢ φ 表示在 \mathfrak{S}_0 中理论 T 可证命题 φ. 由于 φ ⊃ (ψ ⊃ φ) 是逻辑公理, \mathfrak{S}_0 中的任意理论 T 都应该能证 φ ⊃ (ψ ⊃ φ). 这正是 _⊢_ 的构造子 Ax1 所描述的内容. Ax2 与 Ax3 亦同. Ax 是说 T 可证 T 中的元素, 也即非逻辑公理, 这也是理所应当的. 最后一行 MP 是说如果 T 能证 φ 且 T 能证 φ ⊃ ψ 那么 T 能证 ψ, 这对应定义4.2的推理规则.

data _⊢_ (T : Theory) : Formula → Set where
  Ax1 : ∀ φ ψ   → T ⊢ φ ⊃ ψ ⊃ φ
  Ax2 : ∀ φ ψ ρ → T ⊢ (φ ⊃ ψ ⊃ ρ) ⊃ (φ ⊃ ψ) ⊃ (φ ⊃ ρ)
  Ax3 : ∀ φ ψ   → T ⊢ (~ φ ⊃ ~ ψ) ⊃ ψ ⊃ φ
  Ax  : ∀ φ     → T φ → T ⊢ φ
  MP  : ∀ {φ ψ} → T ⊢ φ → T ⊢ φ ⊃ ψ → T ⊢ ψ

φ 不是 T 的定理时记作 T ⊬ φ.

_⊬_ : Theory → Formula → Set
T ⊬ φ = ¬ T ⊢ φ

∅ ⊢ φ 简记作 ⊢ φ. ⊢ φ 不成立时记作 ⊬ φ.

⊢_ : Formula → Set
⊢ φ = ∅ ⊢ φ

⊬_ : Formula → Set
⊬ φ = ¬ ⊢ φ

容易验证

[引理4.3] MP 是演绎推理.

MP-deductive : ∀ v φ ψ → v ⊨ᵥ φ → v ⊨ᵥ φ ⊃ ψ → v ⊨ᵥ ψ
MP-deductive v φ ψ v⊨φ v⊨φ⊃ψ
  with v |≟ φ | v |≟ ψ | v⊨φ | v⊨φ⊃ψ
...  | _      | true   | _   | _     = refl
...  | true   | false  | _   | ()
...  | false  | false  | ()  | _

【注意4.4】 本节开头说逻辑公理是基本的恒真式, 推理规则是基本的演绎推理. 从形式上看, MP 好像是基本的, 但 Ax1 ~ Ax3 形式复杂, 很难令人相信是基本的. 此外, 从形式上也看不出为什么 Ax1 ~ Ax3 加上 MP 就是足够的. 我们需要对 \mathfrak{S}_0 的逻辑公理以及推理规则的选取方式进行辩护. 辩护又分两种:

弱辩护: \mathfrak{S}_0 的定理的集合与恒真式的集合相吻合
强辩护: 对任意理论 T 和公式 φ, T ⊨ φ 当且仅当 T ⊢ φ

弱辩护其实是强辩护中 T ≡ ∅ 的特殊情况. 我们将进行强辩护.

〔定义4.5〕 对任意理论 T 和公式 φ 都有 T ⊨ φ 蕴涵 T ⊢ φ 时, 我们就说 \mathfrak{S}_0 具有完备性 (completeness). 对任意理论 T 和公式 φ 都有 T ⊢ φ 蕴涵 T ⊨ φ 时, 我们就说 \mathfrak{S}_0 具有可靠性 (soundness). 有些书会把这里说的完备性和可靠性合称为完备性.

本篇先证可靠性, 后篇再证完备性.

[引理4.6] 如果 v 是 T 的模型, 那么 T ⊢ φ 蕴涵 v ⊨ᵥ φ.
证明: 反演 T ⊢ φ, 分五种情况.
(1) ~ (3) 逻辑公理 Ax1, Ax2, Ax3 的情况, 分别由 Tauto1, Tauto2, Tauto3 得证.
(4) 非逻辑公理 Ax 的情况, 有 T φ, 由于 v 是 T 的模型, 依定义即得 v ⊨ᵥ φ.
(5) MP 的情况, 由归纳法有 v ⊨ φ 和 v ⊨ φ ⊃ ψ, 由 MP 的演绎性即证. ∎

T⊢φ⇒v⊨φ : ∀ {v T φ} → v ⊨ₘ T → T ⊢ φ → v ⊨ᵥ φ
T⊢φ⇒v⊨φ _ (Ax1 φ ψ)    = Tauto1 φ ψ _
T⊢φ⇒v⊨φ _ (Ax2 φ ψ ρ)  = Tauto2 φ ψ ρ _
T⊢φ⇒v⊨φ _ (Ax3 φ ψ)    = Tauto3 φ ψ _
T⊢φ⇒v⊨φ v⊨T (Ax φ φ∈T) = v⊨T φ φ∈T
T⊢φ⇒v⊨φ v⊨T (MP {φ} {ψ} T⊢ψ T⊢φ⊃ψ) =
  MP-deductive _ φ ψ v⊨φ v⊨φ⊃ψ where
  v⊨φ   = T⊢φ⇒v⊨φ v⊨T T⊢ψ
  v⊨φ⊃ψ = T⊢φ⇒v⊨φ v⊨T T⊢φ⊃ψ

[推论4.7] \mathfrak{S}_0 具有可靠性.
证明: 这是引理4.6的直接推论. ∎

soundness : ∀ T φ → T ⊢ φ → T ⊨ φ
soundness T φ T⊢φ v v⊨T = T⊢φ⇒v⊨φ v⊨T T⊢φ

[推论4.8] T 的元素都是恒真式时, T 的任意定理 φ 也都是恒真式. 特别地, \mathfrak{S}_0 的定理都是恒真式. 反过来, 如果 φ 不是恒真式, 那么 φ 不是 \mathfrak{S}_0 的定理.

tauto-theory : ∀ T → (∀ φ → T φ → ⊨ᵥ φ) → ∀ φ → T ⊢ φ → ⊨ᵥ φ
tauto-theory T H φ T⊢φ v = T⊢φ⇒v⊨φ (λ φ φ∈T → H φ φ∈T v) T⊢φ

⊢⇒⊨ : ∀ φ → ⊢ φ → ⊨ᵥ φ
⊢⇒⊨ φ ⊢φ = tauto-theory ∅ (λ _ ()) φ ⊢φ

⊭⇒⊬ : ∀ φ → ⊭ᵥ φ → ⊬ φ
⊭⇒⊬ φ (v , v⊭φ) ⊢A with ⊢⇒⊨ φ ⊢A v
... | v⊨φ rewrite v⊭φ with v⊨φ
... | ()

\mathfrak{S}_0 由于形式相对简单, 方便证明元定理, 如上面的 soundness, 而不方便证明 \mathfrak{S}_0 的内定理, 如下面的引理.

[引理4.9] 对任意理论 T 和公式 φ 都有 ⊢ φ ⊃ φ.
证明: 如代码, 其理解留作练习. ∎

⊢φ⊃φ : ∀ {T} φ → T ⊢ φ ⊃ φ
⊢φ⊃φ φ =        MP
              --/\
       (Ax1 φ φ) (MP
               --/\
  (Ax1 φ (φ ⊃ φ)) (Ax2 φ (φ ⊃ φ) φ))

【注意4.10】 很难想象 φ ⊃ φ 这样简单自明的恒真式必须要两次 MP 和三次逻辑公理才能证明. 希尔伯特风格的系统并不追求系统内的自然证明, 而是在保证完备可靠的前提下追求元定理证明的流畅性而人为选定的.

【注意4.11】 前面说过, 真值的计算是确定性的但低效的. 与之相对, 证明的存在性的确认是非确定性的但高效的. 意思是说, 没有机械的步骤可以保证找到证明, 但一旦找到, 那么我们可以相对快速地检验证明正确与否.

【注意4.12】 任意命题变元都不是恒真式, 也不是 \mathfrak{S}_0 的定理. 这意味着对任意命题变元 A 和 B, 如果 A 是定理, 那么 B 是定理. 这是个相当令人迷惑的元定理, 它跟系统内的 A ⊃ B 一点关系都没有.

module _ (m : Variable) where
  private A = var m

  ⊭A : ⊭ᵥ A
  ⊭A = (λ _ → false) , refl

  ⊬A : ⊬ A
  ⊬A ⊢A = ⊭⇒⊬ A ⊭A ⊢A

  module _ (n : Variable) where
    private B = var n

    A⇒B : ⊢ A → ⊢ B
    A⇒B ⊢A = ⊥-elim (⊬A ⊢A)

【注意4.13】 T ⊢ φ ⊃ ψ 时有 T ⊢ φ 蕴涵 T ⊢ ψ. 反之则不一定成立. 例如 ⊢ A → ⊢ B 成立但 A ⊃ B 不是恒真式.

φ⊃ψ⇒φ⇒ψ : ∀ T φ ψ → T ⊢ φ ⊃ ψ → T ⊢ φ → T ⊢ ψ
φ⊃ψ⇒φ⇒ψ T φ ψ T⊢φ⊃ψ T⊢φ = MP T⊢φ T⊢φ⊃ψ

module _ where
  private A = var 0
  private B = var 1

  ⊭A⊃B : ⊭ᵥ A ⊃ B
  ⊭A⊃B = (λ { 0 → true ; _ → false}) , refl

  ⊬A⊃B : ⊬ A ⊃ B
  ⊬A⊃B ⊢A⊃B = ⊭⇒⊬ (A ⊃ B) ⊭A⊃B ⊢A⊃B