⊢ 符号的终极混乱在基础的数理逻辑里，⊢...
- 有个梨GPT
- 2024-11-21 21:04:20
⊢ 符号的终极混乱
在基础的数理逻辑里，⊢ 是一个meta level的符号，表示在Hilbert风格的证明论里，左侧的formula可以derive右侧的formula。Hilbert的命题逻辑证明里只有modus ponens这一条规则，到了一阶逻辑有bernays加进来的两条，一条是universal quantification，一条是existential quantification。
但Hilbert风格的证明结构可以线性书写，如果使用了什么规则或者引用了哪条公理，在右侧标注即可。所以不需要有符号表示使用了一条规则。同时因为Hilbert风格的证明是从公理走向定理，全是tautology，所以有些人喜欢在每一行前面都加上 ⊢，这个也是对的，因为tautology都能从空假设集推出。
++++
到了Gentzen的两个证明体系里，natural deduction和sequent calculus，证明的结构是树状的，有很多的演绎规则。所以natural deduction写大横线表示这是使用了一条规则，上面是premise下面是conclusion；sequent类似，但sequent还有个fat arrow在中间，这个arrow不解释成derivation，也不解释成logical consequence（⊧），⊧ 是模型（model）或语义（semantics）意义上的「what follows from what」。
当然 ⊢ 仍然是合法表达derivable的符号，横线是one step derivation关系，⊢ 是zero to more steps。所以 ⊢ 不出现在单一证明里。
++++
图片中的derivation是很基础的，具体的，这是simple typed lambda calculus里的typing rules的推演。在这里：
Γ ⊢ M:α
是一个type意义上的judgement form。M是一个λ term（有类型的λ表达式），α是它的type，Γ 是M表达式里的free variable的类型声明，称为context，这和编程语言里的context是一回事，不意外因为λ就是普世的抽象编程语言。在这里 ⊢ 表示了一组type declaration（Γ）和一个type statement（M:a）的关系，从集合论上理解这个关系也是OK的。所以 ⊢ 是一个syntactic symbol，是judgement form的一部分，当然可以换成任何不产生歧义的其它符号，但是它不是derivation rule的一部分，那个大横线是，这个大横线表示了一组judgement (form)，称为premiss，和一个judgement (form)，称为conclusion，直接的关系，这个关系也可以用集合论理解。
因为在judgement form里把 ⊢ 读成derives也不引起自然语言的直觉混乱，口语上和书面上也经常这么表达，但究其语法含义确实有不同。
++++
而图片里更加有意思的是curry howard isomorphism。就是如果只看type annotation，不管λ term，对于这个simple typed lambda calculus（指类型系统是simple type），图片里每个judgement form里的 ⊢，右侧的表达式都是从左侧开始derivable的，不限于使用什么系统，比如最后一句，也可以从hilbert系统的第一条公理，A implies A直接得到。
但这不是一个巧合。因为如果只看stlc里的三条typing rules，在type意义上，对应的是natural deduction的两个重要演绎规则，implication-elim（λ-application），和implication-intro（λ-abstraction），包括implication-introduction可以discharge assumption，对应stlc的λ-abstraction rule里，Γ 里的type declaration（证明论意义上的assumption），被discharge了。
因此，在judgement form里， ⊢ 两侧的type formulas确实具有逻辑表达式意义上的derivable关系。
++++
在图片的例子里，iii到iv和iv到v的infer，很象是sequent calculus，其中 ⊢ 对应fat arrow，iii到iv是implication-R规则，iv到v也是。但是从i/ii到3的infer不是，这里要么因为左侧相同使用And-R规则，要么使用cut规则，但两者都不可能在右边直接导出β。所以in general，stlc的derivation rule不能看作sequent calculus，即使经典的LK只要加上右侧只能有一个formula的限制就是直觉的LJ。
这里的point是，虽然sequent calculus看上去似乎是比natural deduction高级一点，因为更加泛化，但事实上并不是。因为sequent calculus只能从公理开始，而不是任意假设，在这个意义上它和Hilbert的公理证明是一样的，而natural deduction不同，它可以从假设开始。而这一点对于stlc的（类型）演绎规则是重要的，因为context里，也就是 Γ 里的变量类型声明，任何合法的type表达式都可以，这些类型表达式，在逻辑意义上只能是假设。
在基础的数理逻辑里，⊢ 是一个meta level的符号，表示在Hilbert风格的证明论里，左侧的formula可以derive右侧的formula。Hilbert的命题逻辑证明里只有modus ponens这一条规则，到了一阶逻辑有bernays加进来的两条，一条是universal quantification，一条是existential quantification。
但Hilbert风格的证明结构可以线性书写，如果使用了什么规则或者引用了哪条公理，在右侧标注即可。所以不需要有符号表示使用了一条规则。同时因为Hilbert风格的证明是从公理走向定理，全是tautology，所以有些人喜欢在每一行前面都加上 ⊢，这个也是对的，因为tautology都能从空假设集推出。
++++
到了Gentzen的两个证明体系里，natural deduction和sequent calculus，证明的结构是树状的，有很多的演绎规则。所以natural deduction写大横线表示这是使用了一条规则，上面是premise下面是conclusion；sequent类似，但sequent还有个fat arrow在中间，这个arrow不解释成derivation，也不解释成logical consequence（⊧），⊧ 是模型（model）或语义（semantics）意义上的「what follows from what」。
当然 ⊢ 仍然是合法表达derivable的符号，横线是one step derivation关系，⊢ 是zero to more steps。所以 ⊢ 不出现在单一证明里。
++++
图片中的derivation是很基础的，具体的，这是simple typed lambda calculus里的typing rules的推演。在这里：
Γ ⊢ M:α
是一个type意义上的judgement form。M是一个λ term（有类型的λ表达式），α是它的type，Γ 是M表达式里的free variable的类型声明，称为context，这和编程语言里的context是一回事，不意外因为λ就是普世的抽象编程语言。在这里 ⊢ 表示了一组type declaration（Γ）和一个type statement（M:a）的关系，从集合论上理解这个关系也是OK的。所以 ⊢ 是一个syntactic symbol，是judgement form的一部分，当然可以换成任何不产生歧义的其它符号，但是它不是derivation rule的一部分，那个大横线是，这个大横线表示了一组judgement (form)，称为premiss，和一个judgement (form)，称为conclusion，直接的关系，这个关系也可以用集合论理解。
因为在judgement form里把 ⊢ 读成derives也不引起自然语言的直觉混乱，口语上和书面上也经常这么表达，但究其语法含义确实有不同。
++++
而图片里更加有意思的是curry howard isomorphism。就是如果只看type annotation，不管λ term，对于这个simple typed lambda calculus（指类型系统是simple type），图片里每个judgement form里的 ⊢，右侧的表达式都是从左侧开始derivable的，不限于使用什么系统，比如最后一句，也可以从hilbert系统的第一条公理，A implies A直接得到。
但这不是一个巧合。因为如果只看stlc里的三条typing rules，在type意义上，对应的是natural deduction的两个重要演绎规则，implication-elim（λ-application），和implication-intro（λ-abstraction），包括implication-introduction可以discharge assumption，对应stlc的λ-abstraction rule里，Γ 里的type declaration（证明论意义上的assumption），被discharge了。
因此，在judgement form里， ⊢ 两侧的type formulas确实具有逻辑表达式意义上的derivable关系。
++++
在图片的例子里，iii到iv和iv到v的infer，很象是sequent calculus，其中 ⊢ 对应fat arrow，iii到iv是implication-R规则，iv到v也是。但是从i/ii到3的infer不是，这里要么因为左侧相同使用And-R规则，要么使用cut规则，但两者都不可能在右边直接导出β。所以in general，stlc的derivation rule不能看作sequent calculus，即使经典的LK只要加上右侧只能有一个formula的限制就是直觉的LJ。
这里的point是，虽然sequent calculus看上去似乎是比natural deduction高级一点，因为更加泛化，但事实上并不是。因为sequent calculus只能从公理开始，而不是任意假设，在这个意义上它和Hilbert的公理证明是一样的，而natural deduction不同，它可以从假设开始。而这一点对于stlc的（类型）演绎规则是重要的，因为context里，也就是 Γ 里的变量类型声明，任何合法的type表达式都可以，这些类型表达式，在逻辑意义上只能是假设。
