Frege/Hilbert系统

Frege/Hilbert系统是一个证明系统,是最古老、最简单的证明系统之一。简单来说,这个系统中的证明都是一个命题序列,命题序列中的每个命题PiP_i都是

  • 一个公理
  • 由命题序列 Pk1P_{k_1}Pk2P_{k_2}(其中k1,k2[1,i)k_1, k_2 \in [1, i)) 通过modus ponens得到的命题

这所谓的modus ponens是指,如果Pk1P_{k_1}aa,而Pk2P_{k_2}aba → b,那么可以得到bb

例如说,一个Frege系统由以下两条公理构成:

  1. abaa → b → a
  2. (ab)(abc)ac(a → b) → (a → b → c) → a → c

这里把这个系统叫做系统F.

那么,一个证明aaa → a的序列就是:

  1. aaaa → a → a (公理 1.)
  2. (aaa)(a(aa)a)aa(a → a → a) → (a → (a → a) → a) → a → a (公理 2.)
  3. (a(aa)a)aa(a → (a → a) → a) → a → a (1.,2. modus ponens)
  4. a(aa)aa → (a → a) → a (公理 1.)
  5. aaa → a (4., 3. modus ponens)

证明的正确性是显然的,但却令人有种“不知所云”的感觉。事实上如果要证明aaa → a,那么一个自然的想法是,在前面的aa正确的前提下,证明后面的aa。这就是所谓的“推演定理”(deduction theroem),用形式化的语言写出来,是这样的:

Γ ψϕΓψϕ\frac{Γ\ ψ ⊢ ϕ}{Γ ⊢ ψ → ϕ}

组合子逻辑

用“推演定理”进行证明,是Coq里的主要证明方式。不过这里我们甚至无需借助Coq这种语言,仅仅用Haskell,就可以在编程语言中相当深入地理解“推演定理”和Frege系统的关系。

在Haskell中,一个类型为aaa → a的函数应该被定义为:

id :: a -> a
id x = x
-- 或者
id = \x -> x

根据Curry-Howard同构,如果构造出了一个类型为a -> a的值,那么就相当于证明了aaa → a这个命题。

所以,“推演定理”在Haskell中实际上表现为了一个类型规则(typing rule):

Γ, (x:a)y:bΓ(λx.y):ab\frac{Γ,\ (x:a)⊢ y:b}{Γ ⊢ (λ x. y): a → b}

modus ponens在Haskell中也是一个类型规则,它是函数调用的类型规则:

Γf:abΓx:aΓ(f x):b\frac{ \begin{aligned} Γ ⊢ & f : a → b \\ Γ ⊢ & x : a \end{aligned} }{ Γ ⊢ (f\ x) : b }

这时我们再看系统F的这两条公理,显然它们都对应着一个函数,我们把公理1.对应的函数叫做k,把公理2.对应的函数叫做s:

k :: a -> b -> a
k = \x -> \y -> x

s :: (a -> b) -> (a -> b -> c) -> a -> c
s = \f1 -> \f2 -> \x ->  f2 x (f1 x)

此时推演定理和系统F的关系被破解了一半:

  • 因为sk都被用λ表达式构造出来,所以只要某个系统A承认推演定理和modus ponens,那么一切系统F可证的命题,在系统A中都可证
  • 如果系统A由推演公理和modus ponens组成,那么系统A可证的命题,系统F可证吗?

要回答这个问题,最直接的方法是寻找一个算法,这个算法可以将所有λ表达式转化为只用k函数和s函数进行定义的形式。

例如说之前的id函数,可以被定义为:

id2 :: a -> a
id2 = s k k

如果感到迷惑,可以试一下加个x在末尾:

SKKx=Kx(Kx)=x\begin{aligned} &\bold{S} \bold{K} \bold{K} x \\ = &\bold{K} x (\bold{K} x) \\ = &x \end{aligned}

这个算法是存在的吗?当然存在,为了方便起见,把id函数叫做i,算法如下:

λx.xIλx.UKU,xFV(U)λx.UxU,xFV(U)λx.UVS(λx.U)(λx.V),others\begin{aligned} λ x.x &→ \bold{I} \\ λ x.U &→ \bold{K}U , x ∉ FV(U)\\ λ x.U x &→ U, x ∉ FV(U) \\ λ x.U V &→ \bold{S} (λ x.U) (λ x.V) , \text{others} \end{aligned}

用这个算法,我在coq中改写了一个证明:

(*
	Author: Chenxi Li 
	Email:  [email protected]
*)

Definition K {p q:Type} (a:p) (b:q) := (* p -> q -> p *)
	a.

Definition S {p q s:Type} (f: p -> q -> s) (g: p -> q) (x: p) := 
	(* (p -> q -> s) -> (p -> q) -> p -> s *)
	f x (g x).

Definition I {p:Type} (a:p) := (* p -> p *)
	a.

Theorem L2: forall p q:Prop, p -> (p -> q) -> q.
Proof.
	intros p q H1 H2. apply H2. apply H1.
Qed.

Definition L2': forall p q:Prop, p -> (p -> q) -> q :=
	fun p q => 
		fun a => 
			fun H2 => H2 a.

Definition L2'': forall p q:Prop, p -> (p -> q) -> q :=
	fun p q =>
		(*  fun a => fun H2 => H2 a
		=   fun a => S (fun H2 => H2) (fun H2 => a)
		=   fun a => S I (K a)
		=   S (K (S I)) K
		*)
		S (K (S I)) K.

(*
	By S (K (S I)) K, we can write a Hilbert style proof.

S (K (S I)) K: p -> (p -> q) -> q
	S: (p -> ((p -> q) -> p) -> (p -> q) -> q) -> 
	   (p -> ((p -> q) -> p) -> p) -> 
	   (p -> (p -> q) -> q)
	(K (S I)): p -> ((p -> q) -> p) -> (p -> q) -> q
		K: (((p -> q) -> p) -> (p -> q) -> q) -> p -> 
		   (((p -> q) -> p) -> (p -> q) -> q)
		S I: ((p -> q) -> p) -> (p -> q) -> q
			S: ((p -> q) -> p -> q) -> ((p -> q) -> p) -> (p -> q) -> q
			I: (p -> q) -> p -> q
	K : p -> ((p -> q) -> p) -> p
*)