My understanding is that it stands for "founded relation", as in
well-founded but without the "well", I think because it doesn't have any
other ordering properties like being a partial order attached to it.
On Wed, May 1, 2024 at 5:21 AM 'B. Wilson' via Metamath <
metamath@googlegroups.com> wrote:
> This has been bugging me midly for a while, but I couldn't figure out what
> the
> Fr symbol in df-fr stood for:
>
> 19201 df-fr $a |- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y
> e. x A. z e. x -. z R y ) ) $.
>
> I finally bothered to look up the Takeuti and Zaring reference, which also
> uses
> "Fr" and calls R a "foundational relation". It's not super important, but
> would
> it be worth mentioning this in df-fr's comment?
>
> Cheers,
> B. Wilson
>
> --
> 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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/2F5KIFFJJY2KH.28Z6N87TP90O2%40wilsonb.com
> .
>
--
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSsXfJqj3nGxjuDEFGCMAw8Zvq6AFF0wZ53qib3d8u%3DD3A%40mail.gmail.com.
