I asked the following question on mathematics stack exchange: https://math.stackexchange.com/questions/4744694/is-it-legitimate-to-assert-a-propositional-function
> About a year ago, I had a dispute with someone over whether it is legitimate to assert a propositional function, as in ⊢ 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[0] in the Metamath Proof Explorer[1], which states that ⊢ x = x where x is a set variable, is false since we can show that ∅ ⊨ x = x. > > However, it seems legitimate to assert a propositional function in Principia Mathematica: > > > 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) > > I'm curious about whether many mathematicians accept this convention. I also want to know if it is true that ∅ ⊨ x = x; I'm not familiar with model theory. > > **Reference** > > Whitehead, Alfred North, and Bertrand Russell. 1910. *Principia Mathematica, Vol. I*. Cambridge: Cambridge University Press. https://archive.org/details/principiamathema01anwh/page/18/mode/2up. > > [0]: https://us.metamath.org/mpeuni/equid.html > [1]: https://us.metamath.org/mpeuni/mmset.html -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f9774e9d-84ef-4f68-98ff-e663b3b8aa61n%40googlegroups.com.
