How to prove (¬¬x→¬¬y) ⊢ (x→y)?

Question

How to prove (¬¬X→¬¬Y) ⊢ (X→Y) ?

What I've done:

1. [~X] ¬¬X→¬¬Y implication exclusion

2. [Y] ¬Y AND introduction

3. ¬Y AND Y

4. [~~X] DNE

5. X implication inclusion using the assumption of line 2

6. Y→X

Answer 1

You've got a lot of things right, but much is in the wrong place.

Foremost: Justifications belong on the line of the statement they are being used to derive (it also helps to reference the lines being used for that derivation).

Also, place assumptions on their own lines. Some form of indentation to show where assumptions are raised and discharged is helpful too.

Finally there's the order of your derivations.

Your actual target is to derive $X\to Y$ (not $Y\to X$). So the first assumption needs to be $X$, with the aim of $Y$, so that you may then use "Implication Inclusion" (more commonly known as "Conditional Introduction") to get what you want to get.

Working backwards from there, you know that "Double Negation Elimination" is used to do what it says. However, since you are actually aiming for $Y$ you will first need to obtain $\neg\neg Y$.

You know to use "Implication Exclusion" (more commonly known as "Conditional Elimination") but aren't matching the form. Since you have $\neg\neg X\to\neg\neg Y$ as the premise, you may use it with $\neg\neg X$ to derive $\neg\neg Y$ by this rule. And since that is what you seek to do, you will first need to obtain $\neg\neg X$.

You know that you can do this by assuming a negation and deriving a contradiction. That negation is $\neg X$, and it contradicts the $X$ you have previously assumed.

Just put it back together.

Answer 2

So that would become:

1. [~Y] ¬¬X→¬¬Y implication exclusion

2. [X] ¬X AND introduction

3. ¬X AND X

4. [~~Y] DNE

5. Y implication inclusion using the assumption of line 2

6. X→Y