1

我正在研究库里-霍华德函授。

给定命题逻辑陈述：(¬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.
4

2 回答 2

3

在进行此练习时，从为 引入类型构造函数开始可能会更容易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 =
  ...

第一的。

于 2021-12-18T16:16:40.490 回答
3

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

首先，请注意

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

适用于完全任意的pand a（从¬¬pand¬p您首先获得虚假证明，然后通过 ex falso quodlibet 您获得 any a）。

特别是，对于任何q，

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

成立（将前面的语句应用于a = qand 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] = ???
于 2021-12-21T19:14:44.787 回答