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/a7c6c20a-e8e4-4e96-8046-b3f0a43c11a7%40panix.com.
