Prove moabex in iset.mm

[jkingdon]

http://us.metamath.org/mpeuni/moabex.html is a theorem in set.mm which we do not have (yet at least) in iset.mm but which seems potentially provable.

The weaker version http://us.metamath.org/mpeuni/euabex.html is easy to prove:

${
  $d y x $.  $d y ph $.
  $( The abstraction of a wff with existential uniqueness exists.
     (Contributed by NM, 25-Nov-1994.) $)
  euabex $p |- ( E! x ph -> { x | ph } e. _V ) $=
    ( vy weu cab csn wceq wex cvv wcel euabsn2 vex snexg ax-mp mpbiri
    cv eleq1 exlimiv sylbi ) ABDABEZCPZFZGZCHTIJZABCKUCUDCUCUDUBIJZUA
    IJUECLUAMNTUBIQORS $.
$}

As for how to prove moabex the following are things we can show:

1. From mo3, elsn and logic:

   |- ( E* x ph
   <-> A. x
        ( ph
         -> A. y
               ( [ y / x ] ph -> y e. { x } ) ) )

2. { x | ph } = { y | [ y / x ] ph } follows from cbvab

3. We do have some potentially helpful theorems like abss and ss2ab.

I can't really tell whether those are on the right track or not. At times it seems like moabex should just be a few easy steps away, at other times it feels like I'm running right into "there are two cases: the set has one element or it has none" or other territory which won't work.

As for why it would be useful, moabex would lead to snex and other good stuff.

[jkingdon]

Oh let me not be coy, I'm asking @digama0 if he has a proof of this theorem or a proof that it can't be done.

[digama0]

I don't think it is provable. I know it feels very plausible, but the right way to think about it is that, relative to the rank hierarchy, an assertion that a set exists is giving a constructive bound on the level V_alpha in which all of the set's members can be found. In the case of a predicate that has at most one satisfying instance, we have no such bound. If we know additionally that there is some element in the set, then this element provides the bound, but without it we have nothing. You could write something like ( E* x ph /\ E. y ( A. x ph -> x e. y ) ) -> { x | ph } e. _V, but that's trivial from the second conjunct; the mo pulls no weight.

[digama0]

Another fruitful way to think about this rank bounding business is as data manipulation. The axioms of ZFC allow you to construct rank levels from others, but you can't construct something from nothing (except the 0 rank and stuff you can bootstrap from there). A class provides no "data" about where it lives, because it is spread out over the whole universe - you only get the ability to ask yes-no(-maybe) questions about set membership in the class. An assertion that a class exists is a piece of data that gives you a bound on the rank of this set, which can be used to build other existing things like unions and powersets of this class and so on. Anything with unbounded rank cannot be proven to exist.

So snex, which starts from an arbitrary class and produces evidence that { A } exists, cannot be provable, because the bound here can't depend on A and cannot be upper bounded by anything independent of A either - there are singletons at every rank.

[david-a-wheeler]

On December 4, 2018 9:59:40 PM EST, Mario Carneiro notifications@github.com wrote:

Anything with unbounded rank cannot be proven to exist. So snex, which starts from an arbitrary class and produces evidence that { A } exists, cannot be provable, because the bound here can't depend on A and cannot be upper bounded by anything independent of A either - there are singletons at every rank.

I suggest that comments be added to iset.mm to record when a particular theorem from set cannot be proved, and briefly explain while. That will prevent people from trying unnecessary rabbit holes.

--- David A.Wheeler

[jkingdon]

Oh, back when I was doing all the at most one stuff initially (when I proved mo3 and was unable to prove mo2), I sort of suspected that theorems like the forward direction of mo2 might not be provable. And that also somewhat transferred to moabex. So I'll submit euabex as #667 and we can call it a day (which means I have a lot more proofs where I get to change snex to snexg, but hey, I've been doing that for months now so I'm used to it).

I can't really comment on the ranked hierarchy (for the most part in general, and even more so how it relates to IZF), but my intuition is more just trying to see patterns of what works. Which I can try to put into words as: in classical logic existence is about "is this set too big?" but in with intuitionistic logic, existence is about "you can't get something from nothing" (in the sense that E. x .... tends to be hard to prove and often only comes about if there is an axiom like union or pairing which explicitly provides it).

[jkingdon]

I suggest that comments be added to iset.mm to record when a particular theorem from set cannot be proved, and briefly explain while. That will prevent people from trying unnecessary rabbit holes.

In many ways the most satisfying way to do this is by actually proving that a particular theorem implies excluded middle for an arbitrary proposition, as in http://us.metamath.org/ileuni/ordtriexmid.html (we could try to do the same for the large number of variants of ordinal trichotomy in set.mm but perhaps doing this on a theorem-by-theorem level is overkill, and readers can look for clues like "ordinal trichotomy" in the description).

Formalizing the other proofs of this sort mentioned in https://github.com/metamath/set.mm/issues/629#issuecomment-436954329 strikes me as the best way to handle them. This is fairly subtle stuff and so it is the kind of place where being able to prove things is helpful.

I have been pretty liberal with comments (e.g. http://us.metamath.org/ileuni/19.35-1.html or http://us.metamath.org/ileuni/pm2.01.html ) where the literature treats the topic specifically and clearly (most theorems in this category are in logic, and certain topics like decidable equality of real numbers or inhabited versus non-empty sets). Unfortunately, that level of clarity tends to peter out the farther you get into set theory. Either the references (at least the ones I've found) just don't have much detail, or it isn't clear whether what a given reference says applies to IZF or how to correctly translate to our notation.

So if it is just based on a hunch, or even an informal proof quickly sketched out, I'm more inclined to say "we do not have a proof for X" (which I know) even if I suspect the truth might be "this would imply excluded middle" (which I merely suspect).

[digama0]

After I posted the comment above, I spent a long while seeing if I could prove excluded middle from snex, without success. I suspect you will need a meta-argument to show the unprovability.

[digama0]

I just noticed that not-not-snex is provable quite easily: ( -. { A } e. _V -> -. A e. _V ) by snexg, and ( -. A e. V -> { A } e. _V ) by snexprc, so -. { A } e. _V entails a contradiction.

[jkingdon]

I just noticed that not-not-snex is provable quite easily: ( -. { A } e. _V -> -. A e. _V ) by snexg, and ( -. A e. V -> { A } e. _V ) by snexprc, so -. { A } e. _V entails a contradiction.

I have put this in pull request form at https://github.com/metamath/set.mm/pull/2660