Spellcheck

[tirix]

This corrects several spelling mistakes in the comments of set.mm.

Seeing how many mistakes I make in my own PRs, I have made a few modifications to metamath-knife to add a spell checker for theorem comments and section headers (PR to come).

These changes are the result of findings after running it on set.mm.

The dictionary I used is missing several technical mathematical words (and a few non-words, like setvar, wff or mmj2), maybe a new $j command could be used to extend it.

We also tend to use a lot of latin terms (like modus ponens), I would recommend to italicize them so that they are skipped in the spell checking (this does not apply to words like e.g. definiens, which is a valid english word)

[tirix]

See metamath-knife#186 for the changes in metamath-knife, and more about the method used.

[avekens]

Great, I also was astonished how many typos (even by me!) were in set.mm.

[tirix]

Great, I also was astonished how many typos (even by me!) were in set.mm.

This is probably not exhaustive, it was the result of a quick first pass.
The dictionary I checked against is not exhaustive, so I had a lot of false positive with complex math terms (e.g pseudograph), but there were also e.g. foreign words, and commented out proofs, which also lead to errors I had to prune out.

[jkingdon]

We also tend to use a lot of latin terms (like modus ponens), I would recommend to italicize them so that they are skipped in the spell checking

I guess italics make sense but are these really common or is it more of a handful of occasions?

Sorry to go down a tangent but this prompted me to look at our use of tertium non datur, which is mentioned once but elsewhere we say "excluded middle" (or "law of the excluded middle"), following general usage these days. Actually, going even further down the tangent, tertium non datur isn't a very good name at least in iset.mm because of https://us.metamath.org/ileuni/pwtrufal.html and in fact the section of [Bauer] cited there discusses the point even translating tertium non datur into English as "law of excluded third".