Does intuitionist second-order logic prove the negations of some classical theorems? On p.2(!) of his book The Boundary Stones of Thought, Ian Rumfitt asserts

Intuitionistic second-order logic affirms the negations of some classical theorems.

That surprised me. I'm probably just ignorant but are there well-known examples?
 A: This would surprise me too. Suppose we call $\phi$ a classical theorem iff there is a deduction $\vdash_c \phi$ in classical logic. If there now were an intuitionistic deduction $\vdash_i \neg \phi$, we would also have $\vdash_c \neg \phi$ since any intuitionistic deduction is a perfectly fine classical deduction. But then we could show $\vdash_c \bot$.
What is maybe meant by the author is that we can consistently assume and add some statements to intuitionistic theories which are incompatible with classical logic.
So intuitionistic logic cannot by itself show e.g. $\vdash_i \neg \mathsf{LEM}$ but it's possible to have a consistent(!) theory $\mathcal{T}$ with $\mathcal{T} \vdash_i \neg \mathsf{LEM}$.
Only if we were then to switch back to classical logic would we run into the immediate problem of $\mathcal{T} \vdash_c \bot$, making $\mathcal{T}$ inconsistent over classical logic.
Some examples of such theories or axioms we can add are:

*

*Assuming that all functions $\mathbb{R} \to \mathbb{R}$ are continuous. All the examples of non-continuous functions you might know or will find, need $\mathsf{LEM}$ or something equivalent in their definition.
The usage of $\mathsf{LEM}$ usually occurs when trying to show that a relation is total (which is part of what it needs to satisfy in order to be a function).

*Church's thesis; expressing that all functions $\mathbb{N} \to \mathbb{N}$ are computable. Similarly to above, $\mathsf{LEM}$ allows the construction of non-computable functions.

*Assuming the principle of microaffineness one can show $\Delta :=\{ x \mid x^2 = 0\} \neq \{0\}$ and can interpret $\Delta$ as the set of infinitesimals around $0$. This allows a different approach to differentiation; laying the foundation for synthetic differential geometry, which is a consistent intuitionistic theory as shown by the existence of models. Again using classical logic we would have $\Delta = \{0\}$ and therefore a contradiction.

In a nutshell: removing $\mathsf{LEM}$ provides more freedom.
This is in the sense that there are axioms we can assume which would have lead to a contradiction beforehand, but no longer do, since that contradiction proof crucially relied on $\mathsf{LEM}$.
