[ add ] obvious lemma about self-contradiction to Relation.Nullary.Negation.Core

[jamesmckinna]

Self-explanatory, but I'm open to:

• alternative suggestions for the name of this lemma
• suggestions that we don't even need this ;-)

[gallais]

It's cute!

[Taneb]

I'd be happier with this if this had a shorter (but equally clear) name...

[jamesmckinna]

I'd be happier with this if this had a shorter (but equally clear) name...

An alternative, not necessarily better, in the spirit of #2688 might be

[A⇒¬A]⇒¬A

But I agree, shorter would be better!

Another, given that this is the 'essence' of diagonalisation arguments (you can't have a fixed point of negation; the proof structure is the contra position of the diagonal map), we could call it diagonal or diagonalisation?

UPDATED: any further thoughts on names/naming @Taneb ?

[JacquesCarette]

¬fix¬ ? contra-diag ?

[jamesmckinna]

Thanks @JacquesCarette ... not sure about either of the suggestions, though I have a slight preference for contra-diag, but honestly, I think the contra is superfluous (though semantically meaningful, both the type and the fact that this is in the Negation module...) and diag feels to me as though it leans too much towards short-for-the-sake-of-it... given that this module contains many 'long-form' names, seemingly without problems... which is why I'd suggested diagonalisation, with diagonal as my concession towards abbreviation... but perhaps contra-diagonal should then emerge as the worst-of-breed/design-by-committee compromise ;-)

[Taneb]

I've been scouring Wikipedia pages about logic trying to find a good name... it's almost negation introduction, but not quite - that's (A -> B) -> (A -> ¬ B) -> ¬ B, if you pass id as the first argument you get this. Of the suggestions so far, I like contra-diagonal the best

[jamesmckinna]

I've been scouring Wikipedia pages about logic trying to find a good name... it's almost negation introduction, but not quite - that's (A -> B) -> (A -> ¬ B) -> ¬ B, if you pass id as the first argument you get this.

Hmm... I might even take that as an argument not to add the new lemma, in favour of ¬-intro, although we tend not to have such 'Hilbert-style' principles in the library, because the A ->_ is essentially handled by parametrisation/scope, and then delegation to contradiction... NB did you mean ... -> ¬ A in the above?

Of the suggestions so far, I like contra-diagonal the best

@JacquesCarette would you be OK with this?

[JacquesCarette]

Fine with contra-diagonal (though it's barely shorter than self-contradiction...)

[jamesmckinna]

Fine with contra-diagonal (though it's barely shorter than self-contradiction...)

Well, as I wrote: design-by-committee ;-) Incoming commit... then merge?