search

metamath / set.mm

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

"Uses only Tarski's FOL axiom schemes." #2833

Open benjub opened 2 years ago

benjub commented 2 years ago

The sentence "Uses only Tarski's FOL axiom schemes." appears 33 times in set.mm, all of them in comments of statements anterior to ax-10. Therefore, these comments are redundant (since "Tarski's FOL axiom schemes" designates ax-mp, ax-gen, ax-1 through ax-9). A reader may also wonder what that means and why it appears for some results but not others. If needed, there is ample information on axiom subsystems on the main page mmset.html and in the relevant section comments.

Therefore, I propose to remove this phrase in individual comments, keeping the complete information on the main page and in section comments.

digama0 commented 2 years ago

Even if it's obvious from the ordering of statements in the file, it may not be obvious when reading the theorem on the web page. It would be good for it to come with a link to something for people who want to know what it means though.

david-a-wheeler commented 2 years ago

I agree with Mario. I think many people will first encounter a statement by jumping straight to it via hyperlinks, and it's important that they get some context via comments alone.

benjub commented 2 years ago

It also appears at the bottom of each statement webpage:

This theorem was proved from axioms: [...]

digama0 commented 2 years ago

Yes, but unless you are very involved with metamath you are not likely to know whether ax-7 or ax-10 is Tarski's. The naming convention is not very good for that.

benjub commented 2 years ago

I think it's possible that someone not know whether ax-10 is one of "Tarski's FOL axiom schemes". I think it's possible that someone know what "Tarski's FOL axiom schemes" means in the present context. But I think it's not possible that the same person simultaneously know the latter but not the former, since basically if you want to know what is meant by "Tarski's FOL axiom schemes", you will have to read the definition on mmset.html or a section comment, where it is defined as "ax-mp, ax-gen, ax-1 through ax-9".

But maybe not, so, ok, I'll leave it there.

digama0 commented 2 years ago

Hence why I suggested to put a link. I would expect most readers not to know what it means in the first place. It might be possible to know some logic and know about what Tarski did in general and therefore have a good guess at what "Tarski's FOL axiom schemes" are without knowing how they map to the metamath naming convention, so that would be a counterexample to your claim, but I would expect such people to be very much in the minority.

benjub commented 2 years ago

Ok, so I'm leaving this open the time to figure out where to put the links and which explanation to write.