Recently, Gino Giotto posted a PR metamath/set.mm#4995
<https://github.com/metamath/set.mm/pull/4995>, which proves ax-8 from
df-ss, and posed a question: can ax-8 similarly be proven from df-cleq?
The justification theorem is sufficient for a definition to be
conservative, so any non-conservative result must follow from instances of
the justification theorem. Here, the justification theorem cleqjust for
df-cleq would be ⊢ (∀*x*(*x* ∈ *A* ↔ *x* ∈ *B*) ↔ ∀*y*(*y* ∈ *A* ↔ *y* ∈ *B*)),
with *A*, *B* disjoint from *x*, *y*. Each class *A* and *B* can either be
a setvar or a class abstraction. The theorem follows from axextb if *A* and
*B* are both setvars, or from eleq1ab if *A* and *B* are both class
abstractions; neither of those derivations requires ax-8. Thus, we can
assume WLOG that all uses of cleqjust are of form ⊢ (∀*x*(*x* ∈ *z* ↔ *x* ∈
{*w* | *φ*}) ↔ ∀*y*(*y* ∈ *z* ↔ *y* ∈ {*w* | *φ*})), that is, ⊢ (∀*x*(*x* ∈
*z* ↔ [*x* / *w*] *φ*) ↔ ∀*y*(*y* ∈ *z* ↔ [*y* / *w*] *φ*)), with *z*, *w*,
*φ* disjoint from *x*, *y*.
Our goal is to construct an object theory where cleqjust holds but ax-8
does not. As in the usual interpretation, metavariables *x*, *y*, *z*, …
always represent object variables *v*0, *v*1, *v*2, …, and the truth value
of a wff depends on the values assigned to the object variables. Each value
is an ordered pair of natural numbers. The equality predicate *v**i* = *v*
*j* is true iff the value of *v**i* is equal to the value of *v**j* in both
components. The membership predicate *v**i* ∈ *v**j* is true iff *v**i* =
*v**j* and the second components of both values are equal to *i*; note how
this depends on the values of *v**i* and *v**j* as well as the index *i* of
its first argument.
Generally speaking, whenever we see "*v**i* ∈ *v**j*" in the object theory,
we should read it as *v**i* =*i* *v**j*, where each of the predicates =0, =1,
=2, … acts solely on the values of its arguments and not the indices. To
restate the definition, we have (*x* =*i* *y* ↔ (*x*1 = *y*1 ∧ *x*2 = *i* ∧
*y*2 = *i*)). Indeed, if we wish to access some particular predicate *x* =
*i* *y* in the object theory, we can write it as "[*x* / *v**i*] *v**i* ∈
*y*".
Now that we have defined it, we can see that this theory easily satisfies
ax-mp through ax-7, ax-10, ax-11, and ax-13, since the connectives →, ¬, ∀,
and = all have their usual semantics. All instances of ax-12 are satisfied,
since any expansion of the wff *φ* using the ∈ predicate is equivalent to
one using some particular set of =*i* predicates, all of which respect the
semantics of =. Similarly, all instances of ax-9 are satisfied, since ⊢ (*x*
= *y* → (*v**i* ∈ *x* → *v**i* ∈ *y*)) is equivalent to ⊢ (*x* = *y* → (*z*
=*i* *x* → *z* =*i* *y*)), which is true for any =*i*. Also, all instances
of ax-ext are satisfied, since ⊢ (∀*v**i*(*v**i* ∈ *x* ↔ *v**i* ∈ *y*) → *x*
= *y*) is equivalent to ⊢ (∀*z*(*z* =*i* *x* ↔ *z* =*i* *y*) → *x* = *y*),
which is true for any =*i*. But ax-8 is not satisfied, since ⊢ (*v*0 = *v*1
→ (*v*0 ∈ *z* → *v*1 ∈ *z*)) is invalidated by the assignment *v*0 = *v*1 =
*z* = ⟨0, 0⟩.
Finally, we want to show that all instances of cleqjust are satisfied. Any
instance will be of form ⊢ (∀*v**i*(*v**i* ∈ *z* ↔ *v**i* ∈ {*w* | *φ*}) ↔ ∀
*v**j*(*v**j* ∈ *z* ↔ *v**j* ∈ {*w* | *φ*})), with *z*, *w*, *φ* disjoint
from *v**i*, *v**j*. This can be rewritten as ⊢ (∀*x*(*x* =*i* *y* ↔ *φ*) ↔
∀*x*(*x* =*j* *y* ↔ *φ*)), with *y* disjoint from *x* and *φ* disjoint from
*v**i*, *v**j*. The crucial idea is that for all wffs *φ* definable in the
object language, ∀*x*(*x* =*i* *y* ↔ *φ*) never holds if *φ* is disjoint
from *v**i*. Intuitively, this is because the particular predicate =*i* is
the only one that separates *x*2 = *i* from other possible values of *x*2;
no finite combination of predicates, logical connectives, and quantifiers
can do so, unless it involves =*i*. But directly accessing =*i* in the
object theory would require writing "*v**i* ∈ *y*", which would violate the
DV condition between *φ* and *v**i*. Thus, cleqjust is always true in the
object theory, since both sides are always false due to the DV conditions.
(As a corollary, the defined predicate *z* = {*w* | *φ*} is always false.)
In this object theory, all instances of ax-mp through ax-7, ax-9 through
ax-13, ax-ext, and cleqjust hold, but ax-8 does not hold. Thus, there can
be no proof of ax-8 in set.mm from the rest of ax-mp through ax-13 together
with ax-ext and df-cleq. A more clever construction of ∈ might additionally
satisfy the ZFC axioms, but that would take some work. The underlying
discrepancy for why df-ss or df-in can be used to derive ax-8, but df-cleq
cannot, is that the DV conditions do not allow us to make one side of
cleqjust true and infer the other side.
Please let me know if there are any holes in this argument, I'm no expert
in working with wacky models, especially wacky models of Metamath's
semantics.
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/CADBQv9aHp1pAh4og2sLfPB4d9RtPq%3DDDK7taMqpDeHB5Jykmww%40mail.gmail.com.
