使用 Curry-Howard 对应来证明下一个命题逻辑陈述的正确方法是啥？

Posted 2023-02-19

【中文标题】使用 Curry-Howard 对应来证明下一个命题逻辑陈述的正确方法是啥？

【英文标题】：What is a correct way to prove the next propositional logic statement using Curry–Howard correspondence?使用 Curry-Howard 对应来证明下一个命题逻辑陈述的正确方法是什么？

【发布时间】：2022-01-20 14:46:45

【问题描述】：

我正在研究库里-霍华德的对应关系。

给定命题逻辑语句：(¬p -> q) -> ((¬p -> ¬q) -> p)。

我需要在 OCaml 中定义一个类型（作为命题）和一个函数（作为证明）。

我想出了下一个代码并卡住了：

type empty = | ;; 
let ex58: (('p->empty) -> 'q) -> (('p->empty) -> ('q->empty)) -> 'p = fun f g -> g(f)

错误：

This expression has type ('p -> empty) -> 'q but an expression was expected of type 'p -> empty.

【问题讨论】：

这是某本书中的练习编号 58？它是什么书？我很确定这在直觉上是无效的。

你是对的。证明涉及： p 的双重否定消除。在发布问题之前我不知道。前 5.8 intrologic.stanford.edu/chapters/chapter_05.html

【参考方案1】：

在进行此练习时，从为not 引入类型构造函数开始可能会更容易：

type empty = |
type 'a not = 'a -> empty

然后使用明确的全称量化来重写练习：

let proof_by_contradiction: type p q. (p not -> q) -> (p not -> q not) -> p =
   ...

这应该会稍微改善错误消息

错误：此表达式的类型为 p not -> q 但预期的表达式类型为 p not = p -> empty

在开始这个练习之前，尝试一下可能会很有用

let proof_by_negation:  type p q. (p -> q) -> (p -> q not) -> p not =
  ...

首先。

【讨论】：

您的建议很棒；但我不确定 OP 提到的初始分配是否可以建设性地证明……不使用 fun _ -> assert false ;-)

最初的赋值肯定是一个技巧赋值，我希望它是在构造逻辑中没有双重否定消除的解释之后。

@octachron 我已经实现了：let proof_by_negation: type p q. (p -> q) -> (p -> q not) -> p not = fun f g x -> g(x)(f(x))。最初的分配期望消除p 的双重否定，因此它不能建设性地证明吗？您能否建议来源以阅读有关 OCaml 中普遍和存在量化的更多信息？如何定义和证明一阶定理。

对于通用量化，ocaml.org/manual/polymorphism.html#s%3Apolymorphic-recursion。对于存在量化，GADTs 章节将是最接近的：ocaml.org/manual/gadts-tutorial.html。

不，OCaml 不支持值级别的依赖类型。原因之一是对依赖类型的推断根本无法确定。在类型系统能够表达多少与自动推断类型的可能性之间存在设计折衷。

【参考方案2】：

我很确定这不是建设性可证明的。

首先，请注意

¬¬p -> (¬p -> a)

适用于完全任意的p 和a（从¬¬p 和¬p，您首先获得虚假证据，然后通过同样的方式获得任何a）。

特别是对于任何q，

    ¬¬p -> ((¬p -> q) /\ (¬p -> ¬q))             // ("lemma")

保留（将先前的语句应用于a = q 和a = ¬q）。

现在，如果您的原始陈述((¬p -> q) /\ (¬p -> ¬q)) -> p 为真，那么您可以预组合¬¬p -> ((¬p -> q) /\ (¬p -> ¬q))，从而获得¬¬p -> p。但这是双重否定消除，众所周知，它无法建设性地证明。

这是 Scala 3 中的完整结构（与 OCaml 有点密切相关；这里使用的语言子集应该很容易翻译成 OCaml）：

type ¬[A] = A => Nothing                               // negation
type /\[A, B] = (A, B)                                 // conjunction / product
type Claim[P, Q] = (¬[P] => Q) => (¬[P] => ¬[Q]) => P  // your claim
type DoubleNegationElimination[P] = ¬[¬[P]] => P

/** Ex falso quodlibet. */
def efq[X]: Nothing => X = f => f

/** Lemma, as explained above. */
def lemma[P, Q](a: ¬[¬[P]]): (¬[P] => Q) /\ (¬[P] => ¬[Q]) =
  val left: ¬[P] => Q = notP => efq(a(notP))
  val right: ¬[P] => ¬[Q] = notP => efq(a(notP))
  (left, right)

/** This shows that if you could prove your claim for any `P`, `Q`,
  * then you would also be able to prove double negation elimination
  * for `P`.
  */
def claimImpliesDoubleNegationElimination[P, Q](
  c: Claim[P, Q]
): DoubleNegationElimination[P] =
  notNotP => 
    val (left, right) = lemma[P, Q](notNotP)
    c(left)(right)
  

/** This is an (incomplete, because impossible) proof of the double
  * negation elimination for any `P`. It is incomplete, because it
  * relies on the validity of your original claim.
  */
def doubleNegationElimination[P]: DoubleNegationElimination[P] =
  claimImpliesDoubleNegationElimination(claim[P, Unit])

/** There cannot be a constructive proof of this, because otherwise
  * we would obtain a constructive proof of `doubleNegationElimination`.
  */
def claim[P, Q]: Claim[P, Q] = ???