search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

nf.mm cleanup #905

Open benjub opened 5 years ago

benjub commented 5 years ago

The file nf.mm needs some cleanup as noted in #901 (quoted below). I do not plan to do it, but it should not take long to someone with better text editor skills than me.

From #901: I noticed two other discrepancies in nf.mm (but not in iset.mm) compared to set.mm:

    the "sans-serif reversion" of 2016-01-02 was not done in nf.mm
    the IMG tag misses an ALT attribute and has an ALIGN=TOP attribute
    Should they be fixed ?

Yes, it would be nice to fix these. It is lower priority and can be done at your convenience if you wish to do it (in a separate PR). nf.mm has achieved its primary goal of proving the main important features of NF (derive infinity and show that Cantor's theorem and AC don't hold in general) and isn't being actively developed right now.

BTW I find Scott Fenton's development of nf.mm very impressive. AFAIK this is the only computer formalization of NF set theory in existence. Scott was unable to derive what he calls the "axiom of singleton" from Halperin's NF formalization, and whether Halperin's in incomplete as a result is an open problem. If it is incomplete, that would certainly merit publication I think.

benjub commented 5 years ago

By the way: it looks like mmnf.html could benefit from @david-a-wheeler 's ".raw.html" treatment, to make the axioms appear nicer.

benjub commented 5 years ago

@david-a-wheeler Do you think you can apply the "raw.html" thing to mmnf.html ?

david-a-wheeler commented 5 years ago

@benjub - I certainly can. It won't take me long once I get to it, I just need to find those few minutes :-).

david-a-wheeler commented 5 years ago

I did this here: https://github.com/metamath/set.mm/pull/1002

To make it easier to use and test I improved the script that generates HTML from .raw.html first.

benjub commented 5 years ago

Looks great, thanks!