feat: delete Lusin sets

[felixpernegger]

Delete the two Lusin sets S147 and S148. This was discussed previously in some issue (which I cant find now) and no one was against this.

The reason for the removal is that their definition requires axioms beyond ZFC. So they "resolve" (give counterexamle) certain implications PA => PB that might not exist in pure ZFC.

I like the spaces very much and have thought quite a bit about them in the past. However the point above is critical when systematically tracking open implications.

I do think they should be in pibase, but rather in a section "spaces with additional axioms" or something, which are not included in the "Explore" tab (at least not like regular spaces)

Note that nothing is really lost; they still live in the git history.

[prabau]

I remember there was a discussion about how much we should allow beyong ZFC. I think we said we should not have theorems involving axioms beyond ZFC. But in my recollection we did not come to any conclusion about not adding spaces involving such axioms, or removing spaces like the Luzin spaces. Nobody was against it because that was not the understanding.

We need to discuss the pros and cons further about this before making a decision.
(For the moment I'll block this PR so it does not accidentally get merged.)

@StevenClontz @ccaruvana @felixpernegger @Moniker1998 @yhx-12243 and others: does one of you want to create an issue to discuss further?

[prabau]

Need further discussion first

[Moniker1998]

I don't know what other people feel about this, but I'm not bothered with those spaces existing per se. The issue I had is that there has to be a way to implement something which would regulate non-ZFC content.

[felixpernegger]

Do you need exactly CH (and not more) for Lusin sets btw? Its not clear from the description

[Moniker1998]

@felixpernegger what do you mean? The constructions are under ZFC+CH

[prabau]

@felixpernegger Personally, I don't have a problem having a space requiring axioms beyond ZFC. But I am open to discuss pros and cons is a separate issue if you want to pursue this.