search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

ax-strcoll and ax-sscoll in iset.mm are inconsistent #4077

Closed CatsAreFluffy closed 5 days ago

CatsAreFluffy commented 1 week ago

Assuming phi is true and a is inhabited and after simplifying, ~ax-strcoll is E. b A. y y e. b, which is equivalent to _V e. _V, which contradicts ~vprc. Comparing to axiom 7'' of https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html, after expanding ~ax-strcoll has A. x e. a E. y ( ph -> y e. b ), where the similar term in axiom 7'' is A. x e. a E. y e. b ph. Similar concerns apply to ~ax-sscoll. These axioms are in @benjub's mathbox, and they are not currently used outside their respective sections.

benjub commented 1 week ago

Thanks. I'm going to look at it this weekend.