$A\rightarrow(\neg\neg B\rightarrow B)$ in intuitionistic logic

Question

I have a basic question about intuitionistic logic. Here are two propositions in intuitionistic logic, where $B$ is not $\neg\neg$-stable (that is, it is not the case that $\neg\neg B\rightarrow B$):
$$(1). A\rightarrow(\neg\neg B\rightarrow B),\quad\quad\quad (2). A\rightarrow B.$$
By weakening rule, (2) implies (1). This is trivial. But what about the other direction? It appears to me that if we assume (1), since $B$ is not $\neg\neg$-stable, then (1) holds only if $A\rightarrow B$. Consequently, we shall infer (2) from (1)? Is that right? Thanks a lot!

Answer 1

This does not constitute a valid inference. Choose a proposition $B$ for which neither $(\neg\neg B \rightarrow B) \rightarrow B$ nor $\neg\neg B \rightarrow B$ are provable, then set $A$ to $\neg\neg B \rightarrow B$.

You then have (1) $(\neg\neg B \rightarrow B) \rightarrow \neg\neg B \rightarrow B$, but not (2) $(\neg\neg B \rightarrow B) \rightarrow B$.

edit: How do we know that a suitable $B$ exists? Just take the empty theory over a language with one nullary relation symbol $R$, and verify that $R$ already gives rise to a suitable proposition.