Is it legitimate to assert a propositional function?
77 views
Skip to first unread message
Bulhwi Cha
Jul 30, 2023, 8:29:30 AM7/30/23
to Metamath
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
>
> 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
Bulhwi Cha
Jul 30, 2023, 10:53:47 AM7/30/23
to Metamath
I slightly edited my question from Mathematics Stack Exchange. Mario Carneiro already answered it.
Ken Kubota
Jul 30, 2023, 3:30:25 PM7/30/23
to meta...@googlegroups.com
In Peter B. Andrews’ higher-order logic Q0, universal generalization can be found as Theorem 5220 and universal instantiation as Theorem 5215,
which means that free variables are implicitly universally quantified, and assertions with free variables can be translated into those with bound variables and vice versa.
Note that some restrictions apply, e.g., the free variable must not occur free in the set of hypotheses (Rule of Universal Generalization).
References and formalizations are available online here:
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f9774e9d-84ef-4f68-98ff-e663b3b8aa61n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages