# Is it legitimate to assert a propositional function?

About one and a half years ago, I had a dispute with someone over whether it is legitimate to assert a propositional function, as in $$\vdash x = x$$. They said an assertion containing free variables is nonsense since a propositional function is not a proposition. They also argued that the theorem equid from the Metamath Proof Explorer, which states that $$\vdash x = x$$ where $$x$$ is a set variable, is false since we can show that $$\emptyset \nvDash x = x$$.

However, it seems legitimate to assert a propositional function in Principia Mathematica by Alfred North Whitehead and Bertrand Russell:

When we assert something containing a real variable, we cannot strictly be said to be asserting a proposition, for we only obtain a definite proposition by assigning a value to the variable, and then our assertion only applies to one definite case, so that it has not at all the same force as before. When what we assert contains a real variable, we are asserting a wholly undetermined one of all the propositions that result from giving various values to the variable. It will be convenient to speak of such assertions as asserting a propositional function. (Whitehead and Russell 1910, 19)

Note that by "real variables," they meant free variables. (Linsky 2022, sect. 6)

I'm curious about whether many mathematicians accept this convention nowadays. I also want to know if it is true that $$\emptyset \vDash x = x$$; I'm not familiar with model theory.

Edit: The assertion $$\vdash x = x$$ is theorem $$*13·15$$ from PM and theorem 29 (a) from Kleene's textbook on mathematical logic. (Whitehead and Russell 1910, 178; Kleene 2002, 155) Enderton lists the wff $$x = x$$ as one of the logical axioms of first-order logic in his book. It is a generalization of itself. (Enderton 2001, 112) Asserting $$x = x$$ is not peculiar to the set.mm Metamath database.

Note that the axioms $$*10·1$$ and $$*10·11$$ are the closest that PM comes to rules of universal instantiation and universal generalization, respectively. (Whitehead and Russell 1910, 144; Linsky 2022, sect. 6)

References

• 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. https://plato.stanford.edu/archives/fall2022/entries/pm-notation.
• Whitehead, Alfred North, and Bertrand Russell. 1910. Principia Mathematica, Vol. I. Cambridge: Cambridge University Press. https://archive.org/details/principiamathema01anwh/mode/2up.
• One thing to point out: I am not familiar with Metamath, but I am pretty sure what Metamath is based on is completely different from the formal system presented in Principia Mathematica. Commented Jul 30, 2023 at 8:16
• Also, what do you mean by a propositional function? In impredicative type theories, it may mean terms of types of the form $A\to\mathsf{Prop}$. In first-order theories like $\mathsf{ZFC}$, propositions are not objects but things living outside the theory, so talking about propositional functions may not make sense. Commented Jul 30, 2023 at 8:17
• Also, $\emptyset\models x=x$ is meaningless because there is no element of $\emptyset$. $M\models \phi(x)$ makes sense only when $x$ is in the domain of $M$, but $\emptyset$ is empty... Then how to 'pick' an element $x$ from $\emptyset$ and talk about the validity of formulas with parameter $x$ over $\emptyset$? It is like talking about the baldness of a French King: There is no French King nowadays, then does it make sense to talk about his baldness? Commented Jul 30, 2023 at 8:19
• @HanulJeon For the record, the set.mm Metamath database is based on $\mathsf{ZFC}$. Commented Jul 30, 2023 at 8:36
• In most case, when we assert $\vdash x=x$ we are impicitlly assuming it as universally quantified. See quotation from PM above. Commented Jul 30, 2023 at 8:49

The formulation of FOL that set.mm uses implicitly assumes that the domain of discourse is not empty. That is, the empty set is explicitly excluded from the definition of a "model". This is a fairly common assumption in presentations of logic, and it implies theorems like $$(\forall x,\varphi(x))\to (\exists x,\varphi(x))$$.
The further complication which may or may not be contributing to confusion here is that in the axiom system of set.mm it is legal to assert an open formula (i.e. one with free variables, such as $$\vdash x=x$$); the interpretation of this assertion is that the universal closure of the formula is valid. Indeed, theorems ax-gen and spi let you freely add or remove $$\forall x$$ binders on the outside of a formula, so $$\vdash \varphi(x)$$ and $$\vdash \forall x,\varphi(x)$$ are equivalent.
According to my understanding, the propositional calculus does not admit variables, so "$$x=x$$" is not a propositional statement. It is part of the predicate calculus and is not a sentence (i.e., it has free variables) hence does not have a truth value.
In fact $$\emptyset \vDash x=x$$ in the predicate calculus. This is assuming universal quantification is implicit in $$\vDash$$, in which case the statement $$x \in \emptyset$$ is false, thus $$x=x$$ is true trivially for $$x \in \emptyset$$.
If you're talking about the propositional calculus, it would be something like $$\vdash p=p$$ where p is a proposition, which is one of the equality axioms. (There is a similar axiom for the predicate calculus.)