Fix axioms

[david-a-wheeler]

Chu-Wee Lim identified some issues in the book regarding the axioms, which Norm confirmed. Below are the comments from Chu-Wee Lim, with Norm Megill's replies. We need to fix these and/or note them in the errata.

From: Chu-Wee Lim ...
Subject: Metamath S2 Axioms: Book and Website (ham password: xyz.z.y)
Date: February 28, 2021 at 8:45:44 PM EST

Hi .

There's a discrepancy between the axioms of Tarski's S2 in the book and on the website.

Book (http://us.metamath.org/downloads/metamath.pdf, section 3.3):

ax-4 (Quantified Implication) $a ⊢ ( ∀ x ( ∀ x ϕ →ψ ) →( ∀ x ϕ → ∀ x ψ ) ) (comment: first ∀ x is superfluous)
ax-6 (Existence) $a ⊢ ( ∀ x ( x = y → ∀ x ϕ ) → ϕ )
ax-12 (Substitution) $a ⊢ ( ¬ ∀ x x = y → ( x = y → ( ϕ → ∀ x ( x = y → ϕ ) ) ) )
ax-13 (Quantified Equality) $a ⊢ ( ¬ ∀ z z = x → ( ¬ ∀ z z = y → ( x = y → ∀ z x = y ) ) )

We made a major revision to the propositional calculus axiom system in 2018, and unfortunately the book was not completely updated. The website version is correct in all cases. We will make a note of this so that they will be corrected for the next version of the book. (David, could you add a note to the errata list about this, specifically that the 4 axioms above are stated incorrectly?)

The incorrect axioms you mention above were in fact axioms of the older system that didn't get updated in the book. The changes that were made to the axiom system are described here:

http://us.metamath.org/mpeuni/mmset.html#oldaxioms

which has proofs of the old axioms from the new and vice versa. You will see that the incorrect axioms above are listed in the "obsolete" section of the table.

ax-un (Union) $a ⊢ ∃ x ∀ y ( ∃ x ( y ∈ x ∧ x ∈ z ) → y ∈ x ) (comment: variable x is repeated)
ax-pow (Power Set) $a ⊢ ∃ x ∀ y ( ∀ x ( x ∈ y → x ∈ z ) → y ∈ x ) (comment: variable x is repeated)

These 2 axioms are logically equivalent to the ones on the website, but are also older versions that unfortunately didn't get updated in the book. Again, the "official" axioms are the ones on the website.

The history of the above versions of ax-un and ax-pow is that a long time ago, I thought it would be interesting to state the axioms using the fewest number of different variables. In each case, the inner x is bound by a quantifier, so it is essentially "protected" from the outer x.

People complained that this was confusing (and I agree), so in the set.mm database (and the website derived from it) I later changed them to use different variable names.

(David, could you also add these 2 to the errata? Thanks.)

BTW the older axioms with the double binding are still in the database, proved as theorems if you are interested:

http://us.metamath.org/mpeuni/zfun.html
http://us.metamath.org/mpeuni/zfpow.html

Website (http://us.metamath.org/mpeuni/mmset.html#scaxioms):

ax-4 (Quantified Implication) ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
ax-6 (Existence) ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
ax-12 (Substitution) ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
ax-13 (Quantified Equality) ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))

ax-un (Union) ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
ax-pow (Power Set) ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)