I slightly edited my question from Mathematics Stack Exchange. Mario Carneiro already answered it.
On Sunday, July 30, 2023 at 9:29:30 PM UTC+9 Bulhwi Cha wrote: > 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/c008693a-96d0-4e55-8e48-4f1a1ed0cf2en%40googlegroups.com.
