Misc comment edits

[benjub]

(see commit messages)

[benjub]

Proposal: relabel ~a1tru to ~imtru since it is dual to ~falim and the label is more informative.

[benjub]

@avekens : what about the label change proposal (see comment above) ?

[avekens]

@avekens : what about the label change proposal (see comment above) ?

On the one hand, the label ~imtru is better than ~a1tru. On the other hand, it should be named ~trud, because it follows our rules for deduction style. The currently named theorem ~trud is not in deduction form, therefore this theorem should be renamed...

[benjub]

I propose:
a1tru --> trud
trud --> trump ("tru" followed by modus ponens)

[avekens]

I propose: a1tru --> trud

OK

trud --> trump ("tru" followed by modus ponens)

Do you really like "trump"? ;-) Nevertheless, what about ~mptru, like ~mpbi ("biimpi" followed by ax-mp)?

[avekens]

I think the label changes shoud be documented in changes-set.txt

[avekens]

The label changes themselves are OK.

[david-a-wheeler]

I'm not sure that trump is a good name. No orange hair :-). Seriously, I think that name is a little distracting. Maybe that's just me though.

If we do rename trud, can you add an issue to metamath-book and plan on changing mmnatded.raw.html at least? We specifically discuss applying trud in various places.

[avekens]

For me, everything is fine now - but we should consider David's concerns...

[benjub]

@david-a-wheeler @avekens : I'm going to add an issue to metamath-book regarding trud-->mptru and a1tru-->trud (edit: done: metamath/metamath-book#238). I just updated mnatded.raw.html (no other "raw" or "html" files contain it nor a1tru).

(We finally chose "mptru", but maybe "trump" would have brought unexpected visitors, like a few other pages of theorems with bizarre labels!)

[digama0]

I don't think we should compromising our naming conventions because of some coincidences with modern politics and/or playing cards. That said, I don't think that trump or mptru is a good name here, since it's not a modus-ponens like theorem (it isn't a cut, there is only one hypothesis). In MM0 I use a naming convention of prefix i and e for intro/elim rules for propositional connectives, and this is reasonably called "true elimination" so perhaps etru? true is also a little unfortunate re: accidentally spelling a word.

[benjub]

It's kind of a modus ponens since from the major premise T. -> ph you deduce the conclusion ph. It just happens that the minor premise is T. so does not need to be stated.

The convention following intro/elim is nice, but mixing different conventions can become a bit messy. That said, if you really think etru is preferable, then I'll make a new PR to change mptru to it.

[david-a-wheeler]

As far as naming goes, truim or maybe truimp are probably better names per conventions-label, meaning "true implies".

tru is the fragment from dr-tru, and im is the fragment from df-im (though we sometimes use imp instead; this is documented in conventions-label).

[digama0]

Well, I liked trud, it put it in the same category as all the other deduction form theorems. But the fact that it doesn't fit deduction form but rather is a tool for entering deduction form does make the wording awkward. David, I think that putting im in the name is not a great choice since practically all theorems use im in some form or another so it's not very good at distinguishing theorems. Instead, the prefixes and suffixes are used to describe certain patterns of implication usage in the theorem. A variation would be that since it goes from deduction form to inference form, to call it trudi? Sorry for bikeshedding on an already merged topic.

[david-a-wheeler]

Sometimes you have to bikeshed. This particular theorem is widely used, so we probably should try to make a "good choice". Maybe we should raise this to the mailing list for discussion? May as well maximize the bikeshedding :-).

[david-a-wheeler]

I think that putting im in the name is not a great choice since practically all theorems use im in some form or another so it's not very good at distinguishing theorems.

We usually don't, but we do use im in cases where there's almost nothing else to describe it. It wouldn't be a unique case, it's specifically documented already.

A variation would be that since it goes from deduction form to inference form, to call it trudi?

trudi is fine by me.