如何理解没有谓词的量词“ ∀(λφ.(φ x m→ φ y))”？

Question

我正在阅读有关经典高阶逻辑中模态逻辑的嵌入/自动化的内容（http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf）和哥德尔对上帝存在的证明就是这里的突出例子 https://www.isa-afp.org/entries/GoedelGod.html （如 Isabelle/HOL 编码）。

该嵌入具有个体莱布尼茨平等的嵌入：

abbreviation mLeibeq :: "μ ⇒ μ ⇒ σ" (infixr "mL=" 90) where "x mL= y ≡ ∀(λφ. (φ x m→ φ y))"

这种类型的等式已经用于第一个公理：

A1a: "[∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))]"

无需 lambda 即可将其写为：

A1a: ∀φ[P(¬φ)↔¬P(φ)]

我的问题是 - 如何理解这个表达 ∀(λφ. (φ x m→ φ y)), ，因为通常我们有 ∀x.P(x)？IE。全称量词需要参数 (x) 和谓词 (P(x)），但是这个表达式包含什么没人知道？是完整的 (λφ. (φ x m→ φ y)) 和论证 x 或谓词 P(x)？这里可以省略什么，这里使用的约定是什么？

Answer 1

这 $x$ 在 $\forall x .P(x)$ 是 不是 一个论点。它是一个 绑定变量 指示量词的范围是哪个变量。

让我们将这种情况与定积分进行比较，为了具体起见， $0$ 到 $1$. 。这是一个例子：$$\int_0^1 x^2 + 3 x \, dx$$这是数学家喜欢坚持的一种非常古老的数学表达式编写方式。一般来说（忽略不可积函数的细节）定积分本身就是一个函数：它需要一个函数 $f$ 作为参数，例如 $f(x) = x^2 + 3x$ 并返回一个数字（曲线下的面积）。所以我们可以简单地写 $我$ 对于“整合自 $0$ 到 $1$” 然后积分 $f$ 简直就是$$我(女)$$（或者，如果您想保持集成边界可见，请写 $I_0^1(f)$, ，但我不会）。论据 $f$ 不必是符号，它可以是复杂的表达式：$$I(x \映射到 x^2 + 3 x)$$注意如何“$dx$上面的“改为”$x \mapsto$”。在 $\lambda$- 微积分符号我们将其写为$$I(\lambda x .x^2 + 3 x).$$在古老的符号中，人们有时会感到不安$$\int_0^1 f$$所以他们最终总是显示 $dx$ 通过写作$$\int_0^1 f(x) \, dx$$尽管确实没有必要这样做，因为 $\int_0^1$ 是一个 高阶函数 它将实值函数映射到实数。如果你想让传统数学家感到不安你应该写$$\int_0^1 (x \映射到 x^2 + 3 x)$$在他们的白板上

如果这些都清楚了，那么应该很容易看出全称量词 $\forall$ 就像积分一样，只不过它需要一个 命题函数 （映射到真值而不是数字）并返回 真值。古老的记法$$\forall x 。(x^2 + 3 x > -3)$$就像积分一样，可以更改为$$A(f).$$这里 $A$ 是全称量词，并且 $f$ 它的参数是一个从集合到真值的函数映射。这种函数的一个例子是 $f(x) = (x^2 + 3 x > -3)$. 。同样，我们可以内联复杂的表达式来得到$$A(\lambda x .(x^2 + 3 x > -3))$$现在只需更换 $A$ 和 $\forall$ 为了美好的旧时光：$$\forall(\lambda x .(x^2 + 3 x > -3)).$$这就是计算机喜欢的方式。符号是通用的，所以我们可以写成 $\forall f$ 代替 $\forall x .f(x)$, ，并且它暴露了 $\forall$ 到底是什么：A 高阶 将命题函数映射到真值的函数。