The definition ~df-fr in set.mm corresponds exactly to the definition in
Wikipedia (https://en.wikipedia.org/wiki/Well-founded_relation), and here
the terms *well-founded* or *wellfounded* or *foundational *are used
synonymously, with the side note "Some authors include an extra condition
Are we talking about the same edition of the book? In my (very old) paper
copies, definitions 6.21 and 6.24 are on page 27...
Nevertheless, if the numbering of the definitions is still the same,
definition 6.21 defines a "foundational relation" (`R Fr A`) , whereas
definition 6.24 1) defines a
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 anyway, I think it'd be an epsilon improvement
to mention where the mnemonic comes from in the comment.
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>
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
