关于断言命题函数的合法性及模型论中∅⊨x=x是否成立的技术问询

大概一年半前，我和人争论过断言命题函数（比如⊢ x = x）是否合法。对方坚持认为包含自由变量的断言完全没有意义，因为命题函数本质上不是命题；还指出Metamath Proof Explorer里的equid定理——也就是⊢ x = x（其中x是集合变量）——是错误的，理由是我们可以证明∅ ⊭ x = x。

不过，在怀特海和罗素的《数学原理》（Principia Mathematica）里，断言命题函数似乎是被认可的：

当我们断言包含实变量的内容时，严格来说我们并不是在断言一个命题，因为只有给变量赋值后才能得到确定的命题，而此时我们的断言只适用于这一个确定的情况，和原来的断言效力完全不同。当我们断言的内容包含实变量时，我们是在断言给变量赋予不同值后得到的所有命题中的任意一个未确定的命题。我们可以方便地称这类断言为“断言一个命题函数”。（Whitehead and Russell 1910, 19）

这里要说明一下，他们所说的“实变量”其实就是指自由变量。（Linsky 2022, sect. 6）

我现在有两个疑问：

• 如今有多少数学家接受《数学原理》里的这个约定？
• ∅ ⊨ x = x到底是否成立？我对模型论不太熟悉。

编辑补充：⊢ x = x这个断言其实是《数学原理》里的*13·15定理，也是克林（Kleene）数理逻辑教材里的定理29(a)（Whitehead and Russell 1910, 178; Kleene 2002, 155）。恩德顿（Enderton）在他的书中也把x = x列为一阶逻辑的逻辑公理之一，它本身就是自身的全称概括（Enderton 2001, 112）。所以断言x = x并不是Metamath的set.mm数据库独有的做法。

另外要注意，《数学原理》里的10·1和10·11公理，分别对应着全称实例化和全称概括规则的近似形式（Whitehead and Russell 1910, 144; Linsky 2022, sect. 6）。

参考文献 #

• Enderton, Herbert B. 2001. A Mathematical Introduction to Logic. 2nd ed. Burlington: Harcourt/Academic Press.
• Kleene, Stephen Cole. 2002. Mathematical logic. New York: Dover Publications.
• Linsky, Bernard. 2022. “The Notation in Principia Mathematica.” In The Stanford Encyclopedia of Philosophy (Fall 2022 Edition), edited by Edward N. Zalta and Uri Nodelman.
• Whitehead, Alfred North, and Bertrand Russell. 1910. Principia Mathematica, Vol. I. Cambridge: Cambridge University Press.

备注：内容来源于stack exchange，提问作者Bulhwi Cha