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

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!

• (1) implies (2) is not even valid in classical logic: if $A$ is true and $B$ is false, (1) evaluates to true but (2) evaluates to false. Jan 1, 2021 at 8:31

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.