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:
https://www.owlofminerva.net/files/formulae.pdf#page=76
https://www.owlofminerva.net/files/formulae.pdf#page=38
https://www.owlofminerva.net/files/formulae.pdf#page=825
____________________________________________________
Ken Kubota
https://doi.org/10.4444/100
> Am 30.07.2023 um 07:25 schrieb 'Bulhwi Cha' via Metamath
> <[email protected]>:
>
> 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]
> <mailto:[email protected]>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/f9774e9d-84ef-4f68-98ff-e663b3b8aa61n%40googlegroups.com
>
> <https://groups.google.com/d/msgid/metamath/f9774e9d-84ef-4f68-98ff-e663b3b8aa61n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/0CBEB112-6962-446F-8C1C-38C08F44A60F%40kenkubota.de.
