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.
