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
that R is set-like <https://en.wikipedia.org/wiki/Set-like_relation>, i.e.,
that the elements less than any given element form a set.".
Alexander van der Vekens schrieb am Montag, 6. Mai 2024 um 18:19:11 UTC+2:
> 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 "well founded relation" (`R Wfr A`). The
> difference between both is that the second adds an "is a set" property (on
> each R-initial segment of A): ``R Wfr A <-> ( R Fr A /\ A. x e. A ( A i^i
> ( `'R " { x } ) ) e. _V )`.
>
> In set.mm, ~dffr3 is an alternate definition of ~df-fr which corresponds
> exactly to definition 6.21 in Takeuti/Zaring (as indicated in the comment).
> Furthermore, we have a set-like predicate `R Se A` in set.mm (see ~df-se
> - there isn't such a predicate in Takeuti/Zaring!?), which exactly
> represents the "is a set" property mentioned above.
>
> So if we want to define a well founded relation as in def. 6.24 1) in
> Takeuti/Zaring, then this would be
>
> `df-wfr $a |- ( R Wfr A <-> ( R Fr A /\ R Se A ) ) $.`
>
> We use this definition implicitly, for example in ~tz6.26, where the `R
> Wfwe A` in Takeuti/Zaring is represented by `( R We A /\ R Se A )`.
>
> Under the assumption that the definitions in my copy (maybe "first
> edition") and the edition used in set.mm ("second edition") are the same,
> we actually have to replace "well-founded" by "foundational" in many
> places, at least it should be mentioned in the comment of ~df-fr that there
> is a deviation in terminology, as proposed by B. Wilson.
>
> It would be great if my observations can be approved by somebody who has
> access to the edition of Takeuti/Zaring which is referenced in set.mm.
>
> [email protected] schrieb am Donnerstag, 2. Mai 2024 um 08:13:47 UTC+2:
>
>> 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/88c06ea9-5c45-4a5d-b2ad-728e7a98b2e2n%40googlegroups.com.
