(that's acncc <https://us.metamath.org/mpeuni/acncc.html> fyi)
On Sat, Nov 22, 2025 at 5:09 AM Matthew House <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/2b78d2ad-3cab-4cb6-91a3-e44616019681n%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/CAFXXJStgChQG6uGuKEwgZOTiFOgmNLt4hmscynF-ucWqkbKk3Q%40mail.gmail.com.
