PFPL 笔记 - XI Types and Propositions

笔记 11 Types and Propositions

Constructive Logic

构造性逻辑将「真」定义为「存在一个证明」

著名的 Curry-Howard 同构描述了

• Propositions as types
• Proofs as programs
• Simplification of proofs as evaluation of programs

Constructive logic 没有排中律，which means 如果我们有 $\phi$ false 并不能推出 $\neg \phi$ true

Constructive Semantics

Constructive Logic 关注两个判断： $\phi \text{ prop}$ 和 $\phi \text{ true}$

命题不止被视为一个真值，还被视为一个问题陈述

Classical Logic

constructive logic 没有排中律比较难受

书中认为 Constructive Logic 某种意义上是“人类死角”而 classical logic 是“上帝视角”