精益4中口头澄清

Question

以下段落出现在“精益定理证明 4”中有关量词和等式的章节的开头部分：

因此，构造演算以这种方式用 forall 表达式识别依赖箭头类型。如果 p 是任意表达式，∀ x : α, p 只不过是 (x : α) → p 的替代表示法，其思想是在 p 是命题的情况下，前者比后者更自然。通常，表达式 p 将取决于 x : α。回想一下，在普通函数空间的情况下，我们可以将 α → β 解释为 (x : α) → β 的特殊情况，其中 β 不依赖于 x。类似地，我们可以将命题之间的蕴涵 p → q 视为 ∀ x : p, q 的特例，其中表达式 q 不依赖于 x。

最后一句提到了表达式

∀ x : p, q

，其中

q

可以依赖于

x

，并将其与

p → q

进行比较，其中

p

和

q

是命题。

我的问题是这样的：有没有任何在以下保持时使用

∀ x : p, q

的真实例子？

• p

  是一个命题（所以

  x

  是

  p

  的证明）

• q

  取决于

  x

在普通数学中，当

∀ x : p, q

是集合而不是命题时，会使用表达式

p

，所以这种用法让我感到困惑。

我试图举出

∀ x : p, q

的例子，其中

p

和

q

是命题，而

q

取决于

p

的证明。我找不到任何在普通数学中见过这种情况的情况。

Answer 1

这可能不算是“真正的[数学]示例”，但

List.head?_eq_head

似乎是一个很好的例子

@List.head?_eq_head :
  ∀ {α : Type u_1} (l : List α) (h : l ≠ []),
    List.head? l = some (List.head l h)

你的

p

是我的

l ≠ []

，你的

x

是我的

h

。

这里

List.head

产生列表的第一个元素；但是如果列表为空，这个操作是不可能的，所以它必须证明它是非空的。

Answer 2

Lean 4 将 ∀ 与 Π 合并，据说是为了避免混淆新用户（代价是让老用户/数学家与以前的依赖类型理论经验混淆。）

Π x: p, q

符号在 Curry-Howard 对应关系的讨论之外很少见，但在这种情况下仍然是标准的；它也出现在维基百科关于依赖类型理论的文章中。

该符号通常不会出现在数学中的其他地方，原因很简单：通常，您使用哪个定理证明并不重要，因此不必介意为有关证明选择的元级问题使用特殊符号，我们不介意首先甚至没有真正区分证明的符号。这是该领域有些独特的问题，因此符号也同样独特。