Proof Theory 番外篇

A-> B  (meta language)                                              A⊢ B  (formal language)

A implies B                                                                A entails B

先说下imply 和entail的区别

A implies B 的意思是，A为真的时候我们认为B也为真

所以在truth table中

存在

A      B            A->B

0        1              1

A entails B 的意思是，当A为真的时候，B必为真

不存在

A      B              A ⊢ B

0      1                  1

⊢  Turnstile symbol  （derivability）

⊢ A

在wikipedia的解释是  I know A is truth

我稍加补充

（axiom set）⊢ A

从公理集中我们可以entail A

A ⊢ B

我们可以从A中证明B

⊢ Syntactic consequence    ⊨ Semantic consequence

A ⊢ B    from premise set A to conclusion B thru certain proof system

A ⊨ B  B is true in all premises in the set

If A⊢B then A⊨B (soundness)

If A⊨B then A⊢B(completeness)

object language & meta language （待续）