admin管理员组

文章数量:1531742

-

谢邀。

以我在数理逻辑系统的感觉是,如果是专注于传统的模型论和 Hilbert Style 系统的话,那么

并不常见,反而是数学证明中更加常见。证明论里面写 sequent 的时候有些人喜欢用

,而另一些人喜欢用

在经典命题逻辑中,有三个有推出含义的符号容易混淆:语义后承(semantic consequence),符号是

(\models)。语义后承在一般情况下是连接一个命题集合和一个命题。如果,在任何一种语义赋值

下,只要命题集合

中的每一个命题都为真,那么

就一定为真,那么,我们就说

的语义后承,记作

句法后承(syntactic consequence),符号是

(\vdash)。句法后承的用法和语义后承类似,也是连接一个命题集合和一个命题,如

,表示的是

可以通过句法证明的方式从命题集

中得出。以 Hilbert style 的证明为例,这即是说,存在一个命题序列,使得每个前提要么是公理,要么是

中的命题,而这个命题序列的最后一项是

实质蕴含(material implication / material conditional),符号是

(\to 或者 \rightarrow,当然在强调和不同蕴涵词对比的时候,我们可能会用箭头表示特殊的蕴涵,而用马蹄符号

表示实质蕴涵,这个取决于作者) 。实质蕴含是一个命题逻辑中的二元算子,连接的是两个命题。在句法系统中,由 Hilbert 的前两条公理完全刻画,由第三条公理刻画它和否定的关系。[1] 在语义系统中, 我们说

当且仅当

或者

。[2]

除此之外没有别的常用的,并且经过形式定义的符号。至于数学中的

,其实就是单纯表示推出,这种推出是没有严格定义的,一般情况下在简单的数学系统中,由于系统的强完全性和强可靠性[3],句法后承和语义后承等价,那么这时推出就同时都是两种推出。但是,据我看到 wiki 中的说法,

只表示逻辑后承,但是没有具体区分是语义后承还是句法后承,所以对于完全性和可靠性不成立的系统,这个符号就是模糊的。

在证明论中,这个符号有些时候被当作 sequent calculus 的分割符。而在语言学讨论中,有些时候这个符号被用作预设(supposition)算子。这两点都某种意义上都体现出双箭头在传统经典逻辑中没有确定的含义,所以才会被后来的人拿来用。

当然,前面的语义后承和句法后承也不是数理逻辑系统中的符号,这是元语言符号。并且,在句法系统中不谈论真假,在语义系统中不谈论证明。

此外,在不同的符号系统中,逻辑学家可能会采用

来替代

(实质蕴涵),用

替代

(或者),用

替代

(且),用

替代

(非,否定)。

相关讨论见:逻辑学蕴涵命题中的「→」和数学中的「⇒」有什么区别和共同点?​www.zhihu

[1]

Hilbert 的公理系统可以写作三个公理模式加一个规则:

为什么说是公理模式呢?因为这里的

都是元语言中用来代表合式公式的符号。换而言之,这个系统中有无穷多条公理。

至于推理规则,就只有一个 MP 规则:

,中间的

表示证明系统中的推出,并且,这里的

也都是元语言中代表合式公式的符号。

这种情况下,如果我们要证明

(从空集出发能够推出,即表示在系统内可证),那么我们要写出如下命题序列:(公理 1)

(公理 2)

(1、2,MP 规则)

(公理 1)

(4、3,MP 规则)

[2] 但是在语义系统中,如果我们要说明

(即,是空命题集的语义后承,或者说,是永真的),那么我们只需要说明,根据实质蕴含算子的语义规则,对于任何满足了空空命题集的模型

(也即,对于任何模型),都有

,而根据定义,这等价于

或者

——这是一个总是能达到的条件。因此,我们会说这个公式是空集的语义后承。

一般来说,命题逻辑中的语义规则可以简单地给出: (对于原子命题 p)当且仅当

(

由模型给出的,是从所有原子命题的集合到真假的函数,一般来说命题逻辑的模型只需要确定这个函数就足够了);

。这个操作看上去是循环,但是考虑到

总是比

更加简单,所以我们在确定公式真假的时候,总是先确定我们的模型中

能不能被满足,如果能,那么

,如果不能,那么

[3] 强完全性:对于任意的公式集合

,对于任意的公式

,如果

,那么

。强可靠性:

对于任意的公式集合

,对于任意的公式

,如果

,那么

。而弱完全性是,方式为真的公式都是可证的;弱可靠性是,凡是可证的公式都是为真的(事实上我们会这样认为,如果一个公理系统只有弱完全性,那么它还是好的系统,但是如果一个语义系统被弄成只有弱可靠性,那肯定是哪里出了问题)。 在有完全性和可靠性的基础上,没有必要在实际运用中区分两种推出。

-

本文标签: 数理逻辑这两个有什么区别符号