prove two 4sq lemmas in iset.mm

[jkingdon]

There are a few website changes here, but more importantly are intuitionizations of the set.mm proofs for 4sqlem11 and 4sqlem12 . This solves one of the two main outstanding issues for 4sq (proving that several sets in the proof are finite). I'll leave the other (already noted in mmil.html) for later.

There is also bringing over a few recent renames from set.mm to iset.mm.

[wlammen]

I cannot tell whether the 'intuitionizing' of 4sqlem12 needs all the workarounds presented here, but the result is ok.

[jkingdon]

I cannot tell whether the 'intuitionizing' of 4sqlem12 needs all the workarounds presented here, but the result is ok.

I've been using intuitionizing as a general word but glad to explain in more detail if people would find that helpful rather than clutter. In the case of 4sqlem12:

• change n0 to fin0 (necessary to change something here - the other choice would be to change 4sqlem11 to provide inhabited rather than nonempty as its conclusion). I'm not sure we exactly have an impossibility proof for n0 but we have https://us.metamath.org/ileuni/exmidn0m.html which is close.
• the set.mm proof uses ovex to show that ( ( n ^ 2 ) mod P ) is a set. We need to rearrange a bit so that we can use zsqcl and similar closure theorems. As for why we think we cannot prove ovex in iset.mm, I'm not sure I can go further than noting that https://us.metamath.org/mpeuni/iotaex.html uses excluded middle to combine the https://us.metamath.org/mpeuni/iotanul2.html case and the https://us.metamath.org/mpeuni/iotaval2.html case. But mmil.html (in the "Metamath Proof Explorer cross reference" section) goes into some detail about the alternatives that we do have in iset.mm.
• as a consequence of the previous change, there is some rearrangment of the logic to make sure that ph is available more places
• most theorems involving mod in set.mm are in terms of real numbers. In iset.mm we only have versions for rational numbers. The explanation is the second paragraph of https://us.metamath.org/ileuni/df-fl.html . In the case of 4sqlem12 it is using these theorems on integers so it isn't a problem, but we need to change steps like "an integer is a real number" to "an integer is a rational number".
• any theorems involving division need to change "not equal to zero" to "apart form zero" (in this case https://us.metamath.org/mpeuni/divcan1d.html to https://us.metamath.org/ileuni/divcanap1d.html ). In the case of this proof, we are dealing with a denominator which is known to be greater than zero (which implies both not equal to zero and apart from zero), so there is just a small change needed. iset.mm does have an impossibility proof which shows that we need to distinguish not equal and apart - https://us.metamath.org/ileuni/neapmkv.html
• many steps are unchanged from the set.mm proof; the above is just the ones which are different

[icecream17]

Yeah I think if df-iota was

if ( { y } = { x | ph } , y , (/) )

then iotaex (vex, 0ex, ifexd) would be provable

[jkingdon]

Yeah I think if df-iota was

if ( { y } = { x | ph } , y , (/) )

then iotaex (vex, 0ex, ifexd) would be provable

Interesting. Many theorems involving if require the condition (here { y } = { x | ph } ) to be decidable. But https://us.metamath.org/ileuni/ifexd.html has no such requirement.

I'm not sure I quite understand the proposal. If it is

df-iota $a |- ( iota x ph ) = if ( { y } = { x | ph } , y , (/) ) $.

it seems to be missing something to bind y. And I'm always a little reluctant to get too excited about such a thing until it is worked out in more detail. But if there is something which did work, it would be huge.

[wlammen]

Thanks for your explanations.

I understand that this is is a step in a longer process. While any intermediate state In my eyes should be consistent, it need not be the final result. Waiting for everything to be perfect is a good condition for getting nothing done.

[digama0]

You can prove iotaex under the condition that { x | ph } is a set, which is surely sufficient for practical applications? If A := { x | ph } is a set, then for any y such that { y } = { x | ph }, y e. A, therefore { y | { x | ph } = { y } } C_ A and ( iota x ph ) C_ U. A.

[digama0]

For the case of making this helpful for ovex, one approach that occurs to me is to modify the definition of Fun F to say that not only is the relation functional, but also all its images are pointwise sets. Of course if you have F : A --> B then you usually have that property a forteriori assuming B is a set, and this definition is classically equivalent to the one in set.mm. Are there any proved functional relations in iset.mm that don't satisfy this property?

[jkingdon]

Thanks for your explanations.

I understand that this is is a step in a longer process. While any intermediate state In my eyes should be consistent, it need not be the final result. Waiting for everything to be perfect is a good condition for getting nothing done.

Sure. Most of the intuitionizations I mentioned have impossibility proofs, so there isn't any (known or planned) improvement possible.

But hopefully it goes without saying that if we do find a way to improve on longstanding situations like ovex, that would be for a future pull request, rather than changing anything here. I'll go ahead and merge this one.

[jkingdon]

For the case of making this helpful for ovex, one approach that occurs to me is to modify the definition of Fun F to say that not only is the relation functional, but also all its images are pointwise sets. Of course if you have F : A --> B then you usually have that property a forteriori assuming B is a set, and this definition is classically equivalent to the one in set.mm. Are there any proved functional relations in iset.mm that don't satisfy this property?

So you are trying to loosen the ran F e. _V condition in https://us.metamath.org/ileuni/relrnfvex.html ?

In set.mm fvex and ovex don't have any hypothesis on F anyway, so if the goal is fvex or ovex exactly as in set.mm I'm not sure how this gets us closer.

As for F : A --> B where B is a set, this is covered by https://us.metamath.org/ileuni/relrnfvex.html already.

[jkingdon]

You can prove iotaex under the condition that { x | ph } is a set, which is surely sufficient for practical applications?

Submitted as a pull request at #4854 which also has a response to the question above.