美文网首页知识抽取与证明理论
Proof Theory 摘要第五辑

Proof Theory 摘要第五辑

作者: 鱼棉糖 | 来源:发表于2019-05-12 02:27 被阅读0次

    Apply rules of inference to derive conclusions

    Schema:符合我们语言语法规则(除了用原变量替代various subparts of expression的过程)的表述(expression)或者信息组合方式

    Rules of inference:一种推理的pattern,包含前提(premises),一个或多个结论(conclusion)

    下面的部分主要定义各种不同的推理pattern下几种不同的前提与结论之间的关系类型

    Linear Reasoning (线性推理)

    1) Implication Elimination

    A=>B                                 promise

    A


    B                                      conclusion

    2) Implication Creation

    A                                        promise


    B=>A                               conclusion

    3)Implication Distribution

    A=>(B=>C)                       promise


    (A=>B)=>(B=>C)               conclusion

    以上任何推理中的变量都可以替换为compound sentence

    但是Rules of inference在推理的过程中仅能适用于整个sentence,下面是一个错位的示范

    promise set {A=>B;A=>C}

    下面是一个错误的运用Implication Elimination到局部的sentence的例子

    A=>B                                   B (thru IE)

    A=>C


    B=>C                                   错误!

    整个linear reasoning的过程通常被记为 Δ ⊢R φ

    其中 Δ 是 premise 集合

    R为 推断规则集合 (set of Rules of inference) 

    φ为 conclusion集合 

    Hypothetical Reasoning (假设推理)

    在讲引入Assumption的必要性之前,必须再一次明确的一点是在这个体系内 sentence只能被作为一个整体来对待

    e.g.

    A=>B 与 A 是两个截然不同的表述,前者是说A与B存在implication关系(参考第三辑),而后者是观察到A发生

    Implication Introduction

    A=>B                          promise 1

    B=>C                          promise  2

          // sub proof 1

           /  A                        Assumption

           /   B                        Implication Elimination thru promise 1  and Assumption

           /   C                        Implication Elimination thru promise 2  and Assumption

    A=>C                             Implication Introduction  (Implication Creation thru sub proof 1 3rd line)

    这里需要注意的是Assumption并不是promise,且!在某一个sub proof中间得到的结论不能在 super proof或者 其它 sub proof中使用

    在这里论证的是 A=>C 这个表述关系的sentence,并没有论证A是否发生

    我们检查一下相应的truth table

    A   B   C                   A=>C      A=>B      B=>C

    1    1    1                     1             1              1                          satisfaction

    0    1    0                      0             1              0

    1    0    1                       1             0             1                          satisfaction

    0    0     0                       0             0             0

    这里我们需要关注的是 A=>C在truth table中为1的情况下,会不会promise set中任意子集发生冲突,并没有

    Implication Introduction  本质上是通过reasoning过程创建新的implication关系

    φ ⊢ ψ


    φ ⇒ ψ

    Fitch System

    Soundness & Completeness (Reasoning System的评价方式)

    相关文章

      网友评论

        本文标题:Proof Theory 摘要第五辑

        本文链接:https://www.haomeiwen.com/subject/pkionqtx.html