Email Gateway (May 20 2025 at 06:22): Email Gateway (May 20 2025 at 06:22):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hello,
the "Péter Rózsa" mentioned on lines 13/14 of
HOL/Examples/Ackermann.thy should in fact be Rósza Péter (I hear that
this gender-sensitive mistake is common).
Stepan
Email Gateway (May 20 2025 at 08:37):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Stepan,
this has nothing to do with gender, but the surname-forename order in Hungarian.
Also "Rózsa" is the correct spelling.
https://en.wikipedia.org/wiki/R%C3%B3zsa_P%C3%A9ter
On Tue, 20 May 2025 at 07:22, Stepan Holub
<cl-isabelle-users@lists.cam.ac.uk> wrote:
Hello,
the "Péter Rózsa" mentioned on lines 13/14 of
HOL/Examples/Ackermann.thy should in fact be Rósza Péter (I hear that
this gender-sensitive mistake is common).Stepan
Email Gateway (May 20 2025 at 10:28):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Gergely,
I understand your point. However, do you suggest that
"... the traditional definition, as modified by Péter Rózsa and Raphael
Robinson ..."
is the correct word order in Ackermann.thy, given the Hungarian
convention? Even your Wikipedia link gives "Rózsa Péter".
(Gender aside. It is an unimportant aspect, which I think, just
contributes to the assumption that Péter is the forename.)
Stepan
On 5/20/2025 10:36 AM, Gergely Buday (via cl-isabelle-users Mailing
List) wrote:
Stepan,
this has nothing to do with gender, but the surname-forename order in Hungarian.
Also "Rózsa" is the correct spelling.
https://en.wikipedia.org/wiki/R%C3%B3zsa_P%C3%A9ter
- Gergely
On Tue, 20 May 2025 at 07:22, Stepan Holub
<cl-isabelle-users@lists.cam.ac.uk> wrote:Hello,
the "Péter Rózsa" mentioned on lines 13/14 of
HOL/Examples/Ackermann.thy should in fact be Rósza Péter (I hear that
this gender-sensitive mistake is common).Stepan
Email Gateway (May 20 2025 at 10:54):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
I don't suggest that, it shall be written Rózsa Péter.
And yes, Péter is her forename, see the linked Wikipedia entry.
On Tue, 20 May 2025 at 11:28, Stepan Holub
<cl-isabelle-users@lists.cam.ac.uk> wrote:
Gergely,
I understand your point. However, do you suggest that
"... the traditional definition, as modified by Péter Rózsa and Raphael
Robinson ..."
is the correct word order in Ackermann.thy, given the Hungarian
convention? Even your Wikipedia link gives "Rózsa Péter".
(Gender aside. It is an unimportant aspect, which I think, just
contributes to the assumption that Péter is the forename.)Stepan
On 5/20/2025 10:36 AM, Gergely Buday (via cl-isabelle-users Mailing
List) wrote:Stepan,
this has nothing to do with gender, but the surname-forename order in Hungarian.
Also "Rózsa" is the correct spelling.
https://en.wikipedia.org/wiki/R%C3%B3zsa_P%C3%A9ter
- Gergely
On Tue, 20 May 2025 at 07:22, Stepan Holub
<cl-isabelle-users@lists.cam.ac.uk> wrote:Hello,
the "Péter Rózsa" mentioned on lines 13/14 of
HOL/Examples/Ackermann.thy should in fact be Rósza Péter (I hear that
this gender-sensitive mistake is common).Stepan
Email Gateway (May 20 2025 at 11:21):From: Pierpaolo Bernardi <olopierpa@gmail.com>
Why not write the name as PÉTER Rózsa, in contexts where confusion may arise?
This is a convention widely used.
Cheers
On Tue, May 20, 2025 at 12:54 PM Gergely Buday
<cl-isabelle-users@lists.cam.ac.uk> wrote:
I don't suggest that, it shall be written Rózsa Péter.
And yes, Péter is her forename, see the linked Wikipedia entry.
Last updated: May 30 2025 at 04:27 UTC