Definition talk:Strictly Well-Founded Relation

Fixing/expanding

This definition works fine for defining a foundational relation in ZF (in classical logic). However, it does not work as the definition of a foundational relation on a class unless the axiom of foundation is accepted. Otherwise we need what Smullyan & Fitting happen to call a "well-founded relation" (just an alternative term for the same thing) and define as a relation on a class such that every subclass (not just subset) has a minimal element. With AoF, these are equivalent, because AoF implies that every set has a rank, and it's possible to build from there to the more precise definition.

It also does not work for intuitionistic logic, where a still-stronger formulation is required to be able to do induction. Specifically, the usual way to do induction classically is to start with the assumption that the theorem is false, conclude that there must be a minimal element at which it fails, and derive a contradiction. But this approach inherently requires LEM. The intuitionistic definition, therefore, is that a well-founded/foundational relation is one over which well-founded induction works. I'm no intuitionist, but I figured I should mention it anyway. --Dfeuer (talk) 15:58, 5 April 2013 (UTC)

This is to be addressed in due course as the source works in question are carefully read. --prime mover (talk) 08:13, 2 May 2021 (UTC)