My guess was "(well-)founded relation" as well, but Takeuti and Zaring are
saying "foundational relation" in description of the 6.21 definition for Fr. If
the Fr syntax is riffing off T&K anyway, I think it'd be an epsilon improvement
to mention where the mnemonic comes from in the comment. Something like the
below?
Define the well-founded (a.k.a. foundational) relation predicate...
Mario Carneiro <[email protected]> wrote:
> 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 <
> [email protected]> 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 [email protected].
> > 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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/3DPYLIRK0IUR9.2R4PQFMFJN5VC%40wilsonb.com.
