zoukankan      html  css  js  c++  java
  • 语义后承(semantic consequence),句法后承(syntactic consequence),实质蕴含(material implication / material conditional)

    作者:罗心澄
    链接:https://www.zhihu.com/question/21191299/answer/17469774
    来源:知乎
    著作权归作者所有。商业转载请联系作者获得授权,非商业转载请注明出处。

    在数理逻辑系统中没有使用过Rightarrow,仅在数学证明中使用过。这个符号不是一个标准命题形式语言中的符号。而是一个日常语言中的符号,它的意义是模糊的。

    在命题逻辑中,有三个有推出含义的符号容易混淆:
    • 语义后承(semantic consequence),符号是models(models)。语义后承在一般情况下是连接一个命题集合和一个命题。如果,在任何一种语义赋值下,只要命题集合Sigma中的每一个命题都为真,那么phi就一定为真,那么,我们就说phiSigma的语义后承,记作Sigmamodels phi
    • 句法后承(syntactic consequence),符号是vdash(vdash)。句法后承的用法和语义后承类似,也是连接一个命题集合和一个命题,如Sigma vdashphi,表示的是phi可以通过句法证明的方式从命题集Sigma中得出。即,存在一个证明,使得每个前提要么是公理,要么是Sigma中的命题,而证明的结论是phi。具体来说,一个证明是一个命题序列,其中每个命题要么是公理,要么是前提,要么是由前面的命题通过证明规则得到的。其中最后一个称为结论。
    • 实质蕴含(material implication / material conditional),符号是
ightarrow( ightarrow) 。实质蕴含是一个命题逻辑中的二元算子,连接的是两个命题。在句法系统中,由 Hilbert 的前两条公理完全刻画,由第三条公理刻画它和否定的关系。[1] 在语义系统中, 我们说Sigmamodels p
ightarrow q当且仅当Sigmamodels q或者Sigmamodels
eg p。就是说,如果一个实质蕴含条件句成立,就是说,前件(上面的 p)为真的情况下,后件(上面的 q)不可能为假。[2]

    除此之外没有别的常用的,并且经过形式定义的符号。至于Rightarrow,其实就是单纯表示推出,这种推出是没有严格定义的,一般情况下在简单的数学系统中,由于系统的强完全性和强可靠性[3],句法后承和语义后承等价,那么这时推出就同时都是两种推出。但是,据我看到 wiki 中的说法, Rightarrow只表示逻辑后承,但是没有具体区分是语义后承还是句法后承,所以对于完全性和可靠性不成立的系统,这个符号就是模糊的。

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

    当然,在不同的符号系统中,逻辑学家可能会采用supset来替代
ightarrow(实质蕴涵),用cup替代vee(或者),用cap替代wedge(且),用sim替代
eg(非,否定)。但是我不太清楚到底哪些人是用Rightarrow来表示什么。

    [1] Hilbert 的公理系统可以写作三个公理模式加一个规则:
    (mathcal{A}
ightarrow(mathcal{B}
ightarrowmathcal{A}))
    ((mathcal{A}
ightarrow(mathcal{B}
ightarrow mathcal{C}))
ightarrow((mathcal{A}
ightarrow mathcal{B})
ightarrow(mathcal{A}
ightarrowmathcal{C})))
    (((
egmathcal{A})
ightarrow(
egmathcal{B}))
ightarrow(mathcal{B}
ightarrowmathcal{A}))
    为什么说是公理模式呢?因为这里的mathcal{A}mathcal{B}mathcal{C}都是元语言中用来代表合式公式的符号。换而言之,这个系统中有无穷多条公理。
    至于推理规则,就只有一个 MP 规则:phi,phi
ightarrowpsivdashpsi,中间的vdash表示证明系统中的推出,并且,这里的phipsi也都是元语言中代表合式公式的符号。

    这种情况下,如果我们要证明emptysetvdash p
ightarrow p(从空集出发能够推出,即表示在系统内可证),那么我们要写出如下命题序列:
    1. p
ightarrow((p
ightarrow p)
ightarrow p)(公理 1)
    2. ( p
ightarrow( (p
ightarrow p)
ightarrow p ))
ightarrow
((p
ightarrow (p 
ightarrow p))
ightarrow(p
ightarrow p))(公理 2)
    3. 
((p
ightarrow (p 
ightarrow p))
ightarrow(p
ightarrow p))(1、2,MP 规则)
    4. 
p
ightarrow (p 
ightarrow p)(公理 1)
    5. p 
ightarrow p(4、3,MP 规则)

    [2] 但是在语义系统中,如果我们要说明emptysetmodels p
ightarrow p(即,是空集的语义后承,或者说,是永真的)。那么我们只需要说明,由于在 p 为真和 p 为假的情况下,根据实质蕴含算子的语义规则,Sigmamodels p
ightarrow q当且仅当Sigmamodels q或者Sigmamodels
eg p,我们都能得到p
ightarrow p为真。因此,我们会说这个公式是空集的语义后承。

    [3] 强完全性:对于任意的公式集合Sigma,对于任意的公式phi,如果Sigmamodels phi,那么Sigma vdashphi 。强可靠性: 对于任意的公式集合Sigma,对于任意的公式phi,如果Sigma vdashphi,那么Sigmamodels phi。而弱完全性是,方式为真的公式都是可证的;弱可靠性是,凡是可证的公式都是为真的。 在有完全性和可靠性的基础上,没有必要在实际运用中区分两种推出。
    -
     
    作者:王晓宇
    链接:https://www.zhihu.com/question/21191299/answer/30108436
    来源:知乎
    著作权归作者所有。商业转载请联系作者获得授权,非商业转载请注明出处。

    “语义后承”的后面是可以接一个命题集合的。只要后面集合中一个命题被满足就行。

    下面我说下“=>”的意义。在数理逻辑中,它定义了Sequence这个概念,比如Gamma Rightarrow Delta 就是一个Sequence,其中前后都是有限命题集合。不过它表示一个推理过程,这个过程可能是真,可能是假,要验证一个Sequence的真伪就要用Sequence Calculus进行推导,直到推出的每一个原子命题都为真。具体的推到规则在 中的第一章(命题逻辑)和第四章(谓词逻辑),当然谓词逻辑的推导过程要复杂一些。

    另外需要注意的是,这是一个语义上的推倒,只不过在谓词逻辑和命题逻辑中,语义和语法是等价的(在我发的课件中Satz 4.6中描述的完整性)。相应的,要验证一个Sequence Calculus的正确性,只能通过找对应的Interpretation。

    还有一个需要强调的是在谓词逻辑上因为forallexists可能存在多中推倒可能,所以只要有一个推导出的全是原子Sequence,那么这个Sequence就是正确的。

    最后总结一下,models是语义上的满足(一定正确的),vdash是语法上的满足(正确的),Rightarrow 只是一个推导过程,正确性需要验证。
     

    有两个世界,一个是语义世界,一个是语形世界。

    前者是语义世界的推倒,后者是语形世界的推导。

    举例:将语义世界理解为我们所生活的现实世界,语形世界则可以是一门描述这个现实世界的语言,例如英语,它是一个由字母和语法规则构成的形式系统,两者在个体上的对应体现为现实的苹果和单词“Apple”。


    一些重要的定理正是证明这两个世界的对应性,例如,按照英语的字母和语法规则推出单词Dog,则现实世界能够推出有一个实物与其对应,这应该是完全性(记不清楚了)。


    作者:杨建
    链接:https://www.zhihu.com/question/21191299/answer/29954947
    来源:知乎
    著作权归作者所有。商业转载请联系作者获得授权,非商业转载请注明出处。
  • 相关阅读:
    ansible for devops 读书笔记第二章Ad-Hoc Commands
    ansible for devops读书笔记第一章
    python3 获取天气
    简单cpu web flask mysql
    mysql mysqldump只导出表结构或只导出数据的实现方法
    nginx 限制solr
    [Selenium] 如何使 InternetExplorerDriver 每次启动的端口不会随机变化
    [Selenium] 如何绕过 IE 的安全模式
    [Selenium] close alert window
    [Selenium] waitUntilAllAjaxRequestCompletes
  • 原文地址:https://www.cnblogs.com/sddai/p/6762027.html
Copyright © 2011-2022 走看看