I've made a pull request to add AC_ to iset.mm at
https://github.com/metamath/set.mm/pull/5119
I had forgotten about the AC_ notation; it does seem to cover full
choice and countable choice (but not dependent choice).
On 11/22/25 13:27, Mario Carneiro wrote:
(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
<http://set.mm> and iset.mm <http://iset.mm>) or CCHOICE
(iset.mm <http://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
<http://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 <http://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 <http://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
<https://groups.google.com/d/msgid/metamath/CAFXXJStgChQG6uGuKEwgZOTiFOgmNLt4hmscynF-ucWqkbKk3Q%40mail.gmail.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/4246efbf-4dfc-4a1e-96ea-09633f894041%40panix.com.
