Inconsistency ?

[tirix]

The following database has been produced by Niels Voss (probably @nielsvoss) on "Proof Assistants Stack Exchange".
I don't think many people read it regularly, so I'm reposting here.

Here is the database:

$[ set.mm $]

$c myvar $.
wmyvar $a setvar myvar $.

my1 $p |- E. myvar -. myvar = myvar $= wmyvar wmyvar exneq $.
my2 $p |- ( E. myvar -. myvar = myvar -> F. ) $=
  wmyvar wmyvar weq wn wfal wmyvar wmyvar wmyvar weq wn wn wmyvar wmyvar weq wn
  wfal wi wmyvar wmyvar weq wmyvar cv eqid notnoti wmyvar wmyvar weq wn wn
  wmyvar wmyvar weq wn wfal wi wmyvar wmyvar weq wn dfnot biimpi ax-mp exlimiv
$.
my3 $p |- F. $= wmyvar wmyvar weq wn wmyvar wex wfal my1 my2 ax-mp $.

It appears Niels manages to prove "falsehood" by declaring a "constant variable".
Isn't this some inconsistency that our tools should detect?

[digama0]

Yes, it is not allowed to create a constant in setvar in set.mm, as this makes it ineligible to be a variable sort. I thought this was part of the mmj2 definition checker, but it was never really generalized properly.

[tirix]

I thought this was part of the mmj2 definition checker

Could someone check with MMJ2? I have not tried.

I think what Niels has done here by using a constant as a setvar amounts to state that there is only one set - which obviously contradicts with at least the axiom of separation.