Rename excluded-middle

[MatthewDaggitt]

I think the current name of excluded-middle in Relation.Nullary.Negation is a bit disingenous. I think ¬¬-excluded-middle would be better.

[jamesmckinna]

Two remarks:

• I (personally) find it strange that DoubleNegation belongs in this module, and not in Negation.Core with Stable and friends; (but I guess there is a reason?)
• If you really want a new name, my cat-among-the-pigeons suggestion would be (law-of-)non-contradiction

[MatthewDaggitt]

I (personally) find it strange that DoubleNegation belongs in this module, and not in Negation.Core with Stable and friends; (but I guess there is a reason?)

No reason, and indeed it is about to change imminently in #1855 to what you suggest.

If you really want a new name, my cat-among-the-pigeons suggestion would be (law-of-)non-contradiction

Sure, I would be happy with that. It's not that I'm pro a particular change, it's more that I'm anti the current name 😄

[jamesmckinna]

On second thoughts about the second...
... except to say that both names seem bad; the first as Matthew points out, is not what we (or Brouwer) should properly call 'excluded middle' but I don't much care for the alternative. Hmm.

[jamesmckinna]

@MatthewDaggitt everything moving to fast for me to keep up, even with my own thoughts. Interesting to see/interested in #1855 , will try to catch-up before commenting further. And both Wikipedia and SEP tell me that I am mistaken above.
In the terminology post-Brouwer, things which were only '¬¬-true' were/are often called 'weak', so maybe weak-excluded-middle is (more) palatable?

[jamesmckinna]

The more radical alternative, for those familiar with Grothendieck topologies/j-operators, might be to call this j-excluded-middle but then we'd need a theory of such js, and instance inference to make sure this particular definition picked up the actual instance j = ¬¬... ;-) and so for this instance, we loop back around to @MatthewDaggitt 's initial proposal... 🤦 My bad!

[jamesmckinna]

So... PR #1855 and #1869 didn't in the end seem to resolve this one? FWIW, I'm now definitely 👍 to ¬¬-excluded-middle.

[MatthewDaggitt]

No those PRs didn't resolve this issue.

[Saransh-cpp]

A bit confused here - does this issue require renaming the actual excluded-middle to ¬¬-excluded-middle in Relation.Nullary.Decidable.Core, or just renaming excluded-middle while importing it in Relation.Nullary.Negation?

[JacquesCarette]

I wonder if we can steal some terminology from Coq? ClassicalFacts might be a reasonable place to start digging. Just in case people's opinions have again drifted.