| Description: Axiom ax-11o 1202 ("o" for "old") was the
original version of ax-11 1180,
before it was discovered (in Jan. 2007) that the shorter ax-11 1180 could
replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16
of the preprint). As theorem ax11o 1201 shows, ax-11o 1202 can be derived
from ax-11 1180 and the other axioms; conversely, theorem ax11 1203
shows that
ax-11 1180 can be derived from ax-11o 1202 and the others. An open problem is
whether ax-11o 1202 can be derived from ax-11 1180 and the others when ax-16 1194
and ax-17 1190 are omitted. See ax-11 1180, ax11o 1201, and ax11 1203
for
additional remarks. If we wish to identify where this axiom is needed
in the absence of ax-16 1194 and ax-17 1190, we can use it in place of all
references to theorem ax11o 1201 in the theorems that
follow. |
Home
