6
$\begingroup$

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!

$\endgroup$
1
  • $\begingroup$ (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. $\endgroup$ Jan 1, 2021 at 8:31

1 Answer 1

6
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .