In addition to the two very nice formal answers, let me give an informal proof that $\neg\neg\neg A \Rightarrow \neg A$.
Recall that, by definition, $\neg B$ is an abbreviation for $B \Rightarrow \bot$.
Assume $\neg\neg\neg A$. We are to show $\neg A$, that is, $A \Rightarrow \bot$.
So assume $A$, we are to show $\bot$.
Since $A$, we have $\neg\neg A$. But we also have $\neg(\neg\neg A)$. Hence $\bot$.
This proof uses the lemma that $A \Rightarrow \neg\neg A$. This lemma can also be proven informally:
Assume $A$. We are to show $\neg\neg A$, that is, $(\neg A) \Rightarrow \bot$.
So assume $\neg A$. We are to show $\bot$.
Since $\neg A$ (which means $A \Rightarrow \bot$) and since $A$, we have $\bot$.
By the way, at no point did we use the principle of explosion (ex falso quodlibet). Hence our proofs are even valid in minimal logic, where $\bot$ doesn't have any special rules attached to it.
You notice that for any propositional formula in the logical language $(\wedge, \vee, \rightarrow, \sim)$ (where $\sim$ denotes the usual negation), we have $\vdash_{IPC} \varphi$ precisely if $\vdash_{S4} \varphi'$.
By analogy, you consider a logical system $p$, defined in such a way that for any propositional formula $\varphi$ in the extended logical language $(\wedge, \vee, \rightarrow, \sim, \neg)$, we have $\vdash_p \varphi$ precisely if $\vdash_{S4} \varphi'$.
You claim that the system $p$ constitutes "a naive extension of" intuitionistic logic. As we shall see, this claim fails, and no reasonable algebraic structure or system can correspond to $p$. In particular, it's not possible to extend the variety of Heyting algebras into a semantics for $p$.
I. Why is your system not an extension of intuitionistic propositional logic $IPC$? Given any propositional formulas $\varphi, \psi$ of intuitionistic logic, we always have $\vdash_{IPC} (\varphi \rightarrow \:\sim\!\psi) \rightarrow (\psi \rightarrow \:\sim\!\varphi)$. However, we don't have $\vdash_p (\varphi \rightarrow\:\sim\!\psi) \rightarrow (\psi \rightarrow \:\sim\!\varphi)$.
Set $\varphi$ to the atomic formula $A$, and $\psi$ to the formula $\neg A$. Applying the $'$-translation to the resulting $p$-formula $ (A \rightarrow \:\sim\!\neg A) \rightarrow (\neg A \rightarrow \:\sim\! A)$
gives us the $S4$-formula
$$\Box (\Box (\Box A \rightarrow \Box (\sim \sim\! \Box \Box A)) \rightarrow \Box (\sim\! \Box \Box A \rightarrow \Box \!\sim\! \Box A))$$
which one cannot actually prove in $S4$! It fails because generally $\sim\!\Box x$ does not imply $\Box \!\sim\! \Box x$.
This means that, unlike intuitionistic logic, the system $p$ does not enjoy closure under substitution: from $\vdash_p \varphi$ you cannot conclude $\vdash_p \varphi[A := \psi]$.
The lack of closure under substitution makes the system $p$ extremely ill-behaved: in particular, it rules out the existence of any sort of sound/complete algebraic semantics for $p$.
II. What happens if we try to fix the bad behavior by taking the "closure" $q$ of system $p$ under variable substitution? We can do this, but we get something really boring: classical propositional logic. I will show this using a model-theoretic argument, but with a little effort one can turn the argument below into a direct $q$-proof of excluded middle for ordinary negation.
As you noted, your system has $\vdash_p A \vee \neg A$, so the closed system has $\vdash_q \varphi \vee \neg \varphi$ for all $\varphi$.
Moreover, I claim that $\vdash_p \sim\!\neg P \rightarrow P$ also holds, since the $'$-translation gives
$$(\sim\!\neg P)' = \Box \sim (\neg P)' = \Box\sim \sim \Box P' = \Box\!\sim \sim\!\Box \Box P$$
and consequently
$$(\sim\!\neg P \rightarrow P)' = \Box ((\sim\!\neg P)' \rightarrow P') = \Box (\Box\!\sim \sim\!\Box \Box P \rightarrow \Box P) $$
as well. Now, one can establish $\vdash_{S4} \Box (\Box\!\sim \sim\!\Box \Box P \rightarrow \Box P)$ e.g. by using the necessitation rule, then applying double-negation elimination to get rid of $\sim\sim$, and using the fact that $\Box = \Box\Box$ in S4. A nigh-identical argument gives $\vdash_p P \rightarrow \sim\!\neg P$ as well. It follows that $\vdash_q \varphi \leftrightarrow \sim\!\neg \varphi$ for all $q$-formulas $\varphi$.
Consequently, a model of $q$ would have to be a Heyting algebra $H$ equipped with a unary operator $\neg$ satisfying both $x \vee \neg x = \top$ and $\neg x \rightarrow \bot = x$ for all $x \in H$. I now show that all such Heyting algebras are Boolean algebras.
It suffices to show that $\neg x = x \rightarrow \bot$, since at that point $x \vee \neg x = \top$ will imply excluded middle.
First we show that $\neg x \leq x \rightarrow \bot$ by proving $\neg x \rightarrow (x \rightarrow \bot) = \top$. We can prove this as follows: $\neg x \rightarrow (x \rightarrow \bot) = x \rightarrow (\neg x \rightarrow \bot) = x \rightarrow x = \top$.
For the other direction $y \rightarrow \bot \leq \neg y$, notice that we already know $\neg x \leq x \rightarrow \bot$, so we can set $x = \neg y$ to conclude $\neg\neg y \leq \neg y \rightarrow \bot = y$. But if $\neg \neg y \leq y$, then by negating the inequality $y \rightarrow \bot \leq \neg\neg y \rightarrow \bot = \neg y$. Both inequalities hold, so we get that $y \rightarrow \bot = \neg y$ as claimed. Therefore, all models of $q$ are Boolean algebras.
III. How did I know in advance that your system was going to be ill-behaved? Well, generally, Heyting algebras describe how the open subsets of a topological space behave under the finitary operations of intersection, union, and "interior of the complement". The algebras corresponding to modal logic $S4$, so-called interior algebras, describe how all subsets of a topological space behave under the finitary operations of intersection, union, complement, and interior.
An open subset of a topological space is precisely a subset that coincides with its own interior. This is what makes Gödel's translation work: we simply treat the variables of intuitionistic logic as variables ranging over open sets inside the algebra of all sets.
Your attempted translation of the new operation $\neg$ breaks with this nice correspondence: it insists on translating $A$ as the complement ($\sim$) of an open set ($\Box$). But unfortunately, the complement of an open set is very rarely open! It would have required a remarkable coincidence to get something that respects substitution out of this.
After making this observation, all I had to do was look for a bad substitution instance. Once I had the substitution instance in hand, it quickly led me to the proof of Part II as well.
Best Answer
The statement "$p$ and $\neg p$ are both false" is formally expressed as $$\neg p \land \neg \neg p,$$ which is false by the law of non-contradiction, which states that for any $q$ the proposition $q \land \neg q$ is false (take $q = \neg p$).
More importantly, these consideration do not "demistyfy Gödel", as they refer to proposition with free propositional variables in them. Gödel constructed a sentence, i.e., a logical formula without free parameters, which is neither provable nor falsifiable (in a given formal system).
To put it another way, it is very easy to find a formula which is neither provable nor falsifiable, if we allow free variables, for example $$x < 42$$ where $x$ ranges over the natural numbers (say, in Peano arithmetic) is not provable, but neither is $$\neg (x < 42).$$