Sectioning of the propositional calculus part of set.mm

[benjub]

After @wlammen's huge work of refactoring the somewhat messy section on conjunction and disjunction (thanks!), I propose to modify the TOC from

      ​​*1.2  Propositional calculus
            1.2.1  Recursively define primitive wffs for propositional calculus   wn 3
            ​*1.2.2  The axioms of propositional calculus   ax-mp 5
            ​*1.2.3  Logical implication   mp2 9
            ​*1.2.4  Logical negation   con4 113
            ​*1.2.5  Logical equivalence   wb 196
            ​*1.2.6  Logical conjunction and disjunction   wa 382
                  *1.2.6.1  Logical conjunction   wa 382
                  ​*1.2.6.2  Logical disjunction   wo 826
                  1.2.6.3  Assorted results not assigned yet   animorl 918
            ​*1.2.7  Miscellaneous theorems of propositional calculus   pm5.62 995
            ​*1.2.8  The conditional operator for propositions   wif 1049
            [...]

to

      ​​*1.2  Propositional calculus
            1.2.1  Recursively define primitive wffs for propositional calculus   wn 3
            ​*1.2.2  The axioms of propositional calculus   ax-mp 5
            ​*1.2.3  Implication   mp2 9
            ​*1.2.4  Negation   con4 113
            ​*1.2.5  Equivalence   wb 196
            ​*1.2.6  Conjunction   wa 382
            *1.2.7  Disjunction   wo 826
            *1.2.8  Mixed connectives   animorl 918
            ​*1.2.9  The conditional operator for propositions   wif 1049
            [...]

and then we can adjust the various section comments. With the current axiomatization, I guess we cannot do much better organized without going out of our way. What do you think ?

Actually, I would even begin with 1.2.1 Implication (beginning with wi, ax-1, ax-2) and 1.2.2 Negation (beginning with wn, ax-3), etc. I once suggested it to Norm who was not opposed in principle, but I didn't get to propose anything in time. Opinions ?

[wlammen]

Mixed connectives Actually mixed connectives appear as early as df-bi, Is this the correct title?

[benjub]

Actually mixed connectives appear as early as df-bi, Is this the correct title?

Yes, we have mixed connectives earlier, and in the "mixed connectives" section, there are AND-only and OR-only theorems as well (always considering IMP as a given). That's what I was trying to say in "cannot do much better without...". I think we should keep short titles, so I came up with "mixed connectives", but there may be better wordings...

[david-a-wheeler]

I think "Equivalence" should continue to be called "Logical equivalence" - there are other kinds of equivalence.

[avekens]

I think "Equivalence" should continue to be called "Logical equivalence" - there are other kinds of equivalence.

The same holds for "negation" (of a number) or maybe also "implication" (informal meaning ). So why not keep the "Logical" everywhere?

[benjub]

I think "Equivalence" should continue to be called "Logical equivalence" - there are other kinds of equivalence.

The same holds for "negation" (of a number) or maybe also "implication" (informal meaning ). So why not keep the "Logical" everywhere?

All of these are subsections of a section titled "Propositional calculus", so keeping "logical" seems redundant.

[david-a-wheeler]

All of these are subsections of a section titled "Propositional calculus", so keeping "logical" seems redundant.

That's true when you're reading just the table-of-contents.

However, each of these sections are long, and people often use hypertext links to jump to specific sections. In short, a reader of a section might not realize they're in the "Propositional calculus" section. I think the second-level headers (at least) should be clearer on their own, to help readers who just jumped into it. I'm sure there's a trade-off - no one wants 50 word headers - but adding the word "Logical" still results in a pretty short title. I'd be happy with leaving "Logical" in all those second-level headers, it'd be consistent and would help hint to people what they're looking at.

[benjub]

I can't imagine a real life scenario where this could confuse someone, but ok.

[avekens]

I agree with Benoît's proposal. I would prefer to keep "Logical", but I do not insist on it.

[david-a-wheeler]

Just to be clear, I agree with Benoît's proposed reorganization - I'm just quibbling about section names.

I would just like to see the word "Logical" be retained for at least equivalence, and I think there's a decent argument for keeping the word "Logical" in all the cases where it's currently in the heading title. It's true that "Logical" is implied by the larger section it's in, but people jumping into the section via hyperlinks may not see the broader context at first.

[benjub]

That's fine, I'll add "logical". I'll probably do that this weekend. Maybe others (@jkingdon, @digama0) may have their say.