Is the " contrapositive relation" rigorously symmetric? What is rigorously the contrapositive of : ~X --> ~ Y?

Question

Is the relation " being the contrapositive of" really symmetric?

I mean : the contrapositive of X --> Y is ~Y --> ~X.

If the relation " being the contrapositive of " is symmetric, then I can say that the contrapositive of : ~Y --> ~X is X --> Y.

But I ask myself whether, rigorously, the contrapostive of ~Y --> ~X should not rather be :

                           ~ ~ X --> ~ ~ Y. 

Certainly , ~ ~ X --> ~ ~ Y is equivalent to X --> Y. But is this equivalence a sufficient reason to say that the contraposition relation is symmetric?

Remark. The same question could be asked for the relation " being the nagation of". ~X is the negation of X , but is X the negation of ~X?

Answer 1

You are completely right, if we define the contrapositive as a syntactic transformation and don't want to do an awkward case analysis, then the contrapositive of $\neg X\to \neg Y$ is $\neg\neg Y\to \neg\neg X$.

This is equivalent to $Y\to X$ in classical logic but not, say, in intuitionistic logic where $\neg\neg X$ may differ from $X$.

Viewing $\neg X$ as $(X\to \bot)$ which is the usual definition of $\neg$ if it is not taken as a primitive, then the theorem "$(X\to Y)\to (\neg Y\to \neg X)$" requires basically no rules of logic. Of course, this is an exageration, but look :

Assume $X\to Y$, assume $\neg Y$, and assume $X$. Then by modus ponens, $Y$. Then by modus ponens [recall $\neg Y = (Y\to \bot)$] $\bot$. Thus $X\to \bot$ [discharge the $X$ assumption]. Therefore $\neg Y\to\neg X$ [discharge the $\neg Y$ assumption]. Therefore $(X\to Y)\to (\neg Y\to \neg X)$ [no assumptions].

And of course, this shows that $(\neg X\to \neg Y)\to (\neg\neg Y\to \neg\neg X)$ with also very few logic rules; whereas $(\neg X\to \neg Y)\to (Y\to X)$ requires a lot more : $\neg\neg Y\to \neg\neg X$ is the rightful contrapositive of $\neg X\to \neg Y$. (notice that if we defined $\neg_C X$ as $(X\to C)$ and the $C$-contrapositive of $X\to Y$ as $\neg_C Y\to \neg_C X$, then the theorem would still hold, whereas you wouldn't expect that $\neg_C X\to \neg_C Y$ implied $Y\to X$, would you ?)

Another point of view is to interpret (this is a very loose explanation) "$X\to Y$" as "functions from $X$ to $Y$". Then the contrapositive is nothing but functional application, whereas again, going from $\neg X\to \neg Y$ to $Y\to X$ requires more than that.

The answer for negation is the same : the negation of $\neg X$ is $\neg\neg X$, and it is equivalent to $X$ in classical logic, but even then syntactically it's different, and there are logics where the equivalence does not hold anymore.