美文网首页知识抽取与证明理论
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