Inconsistency in old versions of ax-cc

[Matthew House]

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 as written was inconsistent with the rest of the ZFC axioms. As first introduced 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 or ax-inf2. This was quietly rectified in a 2016 commit 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

[Jim Kingdon]

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 .

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/c0cd4d1c-9d87-4ad1-840c-630351b95a88n%40googlegroups.com.

[Matthew House]

At least for weak forms of Choice, I've found df-acn 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").

[Mario Carneiro]

(that's acncc fyi)

To view this discussion visit https://groups.google.com/d/msgid/metamath/2b78d2ad-3cab-4cb6-91a3-e44616019681n%40googlegroups.com.

[Jim Kingdon]

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).

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJStgChQG6uGuKEwgZOTiFOgmNLt4hmscynF-ucWqkbKk3Q%40mail.gmail.com.