search

metamath / set.mm

Metamath source file for logic and set theory
Other
254 stars 88 forks source link

Add well-founded predicate to iset.mm #646

Closed jkingdon closed 4 years ago

jkingdon commented 5 years ago

Right now iset.mm does not have a well-founded predicate (Fr in set.mm). This means that some ordinal theorems may require the Axiom of Set Induction (the IZF equivalent to the Axiom of Foundation/Regularity in ZF). Being able to do some of this development without that axiom is the purpose of the well-founded predicate in set.mm (if we assume regularity/foundation in classical logic, set membership is well-founded on any class - see zfregfr in set.mm).

Presumably the "right" notion of well founded is the inductive one, that is, a property that satisfies the epsilon (or R) induction principle is always true. To state this in set theory, you can say something like this:

R Fr A <-> A. s ( A. x ( A. y ( y R x -> y e. s ) -> x e. s ) -> A C_ s )

This definition has some problems when A is a proper class. As such, ax-setind has to be stated as a schema instead:

A. x ( A. y ( y e. x -> y e. S ) -> x e. S ) -> S = _V

There are two ways to say no infinite descending sequence, using E. -. or -. A., which are not intuitionistically equivalent. Furthermore there are some trivial commutations that are not intuitionistically valid. So I think that makes the following definition possibilities:

R Fr A <-> A. s ( A. x ( A. y ( y R x -> y e. s ) -> x e. s ) -> A C_ s )
R Fr2 A <-> A. s ( s C_ A -> ( A. x e. s E. y e. s y R x -> s = (/) ) )
R Fr3 A <-> A. s ( s C_ A -> ( E. x x e. s -> E. x e. s A. y e. s -. y R x ) )

The set.mm definition is roughly Fr3 (but it uses nonempty in place of inhabited). We can probably just focus on the first definition, but ideally we'd prove it in set.mm (to show that in classical logic it is equivalent to the definition of Fr in set.mm).

(some of this description was adapted from an email by @digama0 ).

jkingdon commented 5 years ago

There's discussion of proving irreflexivity for a well-founded relation at https://github.com/metamath/set.mm/issues/647#issuecomment-441550666 . That proof should be adaptable to well-founded relations given a definition analogous to ax-setind.