At least for weak forms of Choice, I've found df-acn <https://us.metamath.org/mpeuni/df-acn.html> to be pretty helpful. Countable Choice would correspond to an antecedent of AC_ _om = _V ("you can get a choice function for a countable collection of arbitrary-sized sets").
On Friday, November 21, 2025 at 10:54:45 PM UTC-5 [email protected] wrote: > Oooh, nice historical note. > > Also makes me muse a bit about exploring axioms via $a (as in ax-cc ) or > via including them as explicit hypotheses/antecedents, as in notations like > CHOICE (set.mm and iset.mm) or CCHOICE (iset.mm). The definition checker > would complain if DV conditions were missing from > https://us.metamath.org/ileuni/df-cc.html . > On 11/21/25 18:53, Matthew House wrote: > > I'm mainly just putting this up in case someone else notices this, since I > couldn't find anything else about it. I've recently been trawling through > old versions of set.mm, and I noticed that from 2013 to 2016, ax-cc > <https://us.metamath.org/mpeuni/ax-cc.html> as written was inconsistent > with the rest of the ZFC axioms. As first introduced > <https://github.com/metamath/set.mm/commit/03160ffca94aec05c482f455f6140102d44cc48b> > > to set.mm, it was written: > > ${ > $( The axiom of countable choice (CC). It is clearly a special case of > ~ ac5 , but is weak enough that it can be proven using DC (see > ~ axcc ). It is, however, strictly stronger than ZF and cannot be > proven in ZF. $) > ax-cc $a |- ( x ~~ om -> > E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) $. > $} > > Notice that this has no DV conditions, and thus it includes the statement |- > ( x ~~ om -> E. z A. z e. x ( z =/= (/) -> ( z ` z ) e. z ) ), to which > there are obvious counterexamples if we assume ax-inf > <https://us.metamath.org/mpeuni/ax-inf.html> or ax-inf2 > <https://us.metamath.org/mpeuni/ax-inf2.html>. This was quietly rectified > in a 2016 commit > <https://github.com/metamath/set.mm/commit/cfb23de8be111e40084f4921a3718263dba63077> > > by NM, which added the missing DV condition: > > ${ > + $d f n x z y $. > $( The axiom of countable choice (CC), also known as the axiom of > denumerable choice. It is clearly a special case of ~ ac5 , but > is weak > enough that it can be proven using DC (see ~ axcc ). It is, > however, > strictly stronger than ZF and cannot be proven in ZF. It states > that any > countable collection of non-empty sets must have a choice function. > (Contributed by Mario Carneiro, 9-Feb-2013.) $) > ax-cc $a |- ( x ~~ om -> > E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) $. > $} > > This appears to be the only historical inconsistency in set.mm that was > not directly marked as such. > > Matthew House > > -- > 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 visit > https://groups.google.com/d/msgid/metamath/c0cd4d1c-9d87-4ad1-840c-630351b95a88n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/c0cd4d1c-9d87-4ad1-840c-630351b95a88n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- 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 visit https://groups.google.com/d/msgid/metamath/2b78d2ad-3cab-4cb6-91a3-e44616019681n%40googlegroups.com.
