二重否定除去
double-negation elimination
$ \lnot\lnot P\to P