Skip to content

Theory Modification: Stronger Version of Replacement Schema

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/replacement-stronger into main

The replacement schema has been changed to use the stronger version. This is supported by Jech's Set Theory, page 166,

replacement-jech

Our older version purported that there existed a set Y that contained these elements (but not precisely these). The stronger version is provable from the weaker one with a single application of the Comprehension schema, but is closer to Jech's version of the axioms, and is also generally the version that would be used in practice.

Old:

forall(x, (in(x, a)) ==> existsOne(y, sPsi(a, x, y))) ==>
      exists(b, forall(x, in(x, a) ==> exists(y, in(y, b) /\ sPsi(a, x, y))))

New:

forall(a, in(a, x) ==> existsOne(b, sPsi(x, a, b))) ==>
      exists(y, forall(b, in(b, y) <=> exists(a, in(a, x) /\ sPsi(x, a, b))))

Our version differs from Jech in that we ask that \phi be functional only on the set we are applying replacement to, and consequently guarantee the existence of its image, and not for an arbitrary set. I believe this is more usable within our system. The two forms are equivalent (this PR guarantees no proof).

Funnily (no, it was my fault) our documentation already corresponds to the new version, since the author (definitely still me) wrote it with Jech as the reference more than the formula in code. I have checked the rest of the axioms in light of this, and we don't seem to have another one like this, partly because everything else corresponds to Jech exactly.

The replacement schema has not seen any use till now (but should in #156), so it is fine to change it right now.

Merge request reports