Obsolete Axiom ax-c16 mentioned!?

[avekens]

In the footnote on page 71, the (obsolete!) Axiom ax-c16 is mentioned. Since this axiom is not mentioned elsewhere in this section, this footnote is very confusing. Either the footnote must be revised, or it should be removed completely.

Additionally, there is a reference to a "comment" on page 125, where there is no explict "comment" anymore (as it was in the old book). It should be referred as "end of section 4.2.4" instead. The corresponding paragraph is also not very clear by itself (what does "the system in set.mm obtained from ax-1 through ax-c14 in set.mm, and deleting ax-c16 and ax-5" mean?). I propose to revise this paragraph, too.

Finally, looking at the example for a missing $d statement, I think it is not a good idea to use axioms or axiom-like theorems for demonstration purposes. It could be confusing and misleading ("is this a problem/matter only for axioms?"). By the way, ax-c16 is described as "axiom of logic", which is also not true anymore...