I meet a question about the existence/non-existence of a dischargeable hypothesis. The question is as follows: in intuitionistic logic, if for every proposition $X$, it cannot be the case that $X$ implies $A$ and $X$ is true, does it as a whole implies $\neg A$?
$$(\forall X\neg((X\rightarrow A)\wedge X))\xrightarrow{?}\neg A$$
And what if we add a further condition that $X\not\leftrightarrow A$?
I. First, let's deal with the case when we are allowed to substitute $A$ for $X$. Then the desired implication holds. The proof is as follows.
Take a proposition $A$ and assume that $\neg ((X \rightarrow A) \wedge X$ holds for all propositions $X$. Assume for a contradiction that $A$ holds.
Clearly $A \rightarrow A$ holds, and by our second assumption $A$ holds as well, so $(A \rightarrow A) \wedge A$ holds. But by our first assumption we also have that $\neg ((A \rightarrow A) \wedge A)$, a contradiction.
Thus, we conclude that if $\neg ((X \rightarrow A) \wedge X)$ holds for all propositions $X$, then $\neg A$ holds.
II. It's not clear what the restriction $X \neq A$ means here. If it just means that we're not allowed to substitute the specific formula $A$, then that's not really a strong restriction: we could substitute the syntactically different, but practically equivalent formula $A \wedge A$ instead.
But there's another way to interpret $X \neq A$, as the restriction that we must prove $\neg (X \leftrightarrow A)$ for each $X$ that we choose to substitute. Effectively, this just changes our first assumption to $\forall X. \neg(X \leftrightarrow A) \rightarrow \neg((X \rightarrow A) \wedge A)$. In this case, the implication need not hold (indeed, it does not hold for $A \equiv \top$).
This is because $\neg(X \leftrightarrow A) \rightarrow \neg((X \rightarrow A) \wedge A)$ is a theorem of the intuitionistic second-order calculus for every proposition $X$. Here's a proof:
Let $X$ be arbitrary, and assume $\neg (X \leftrightarrow A)$ and $(X \rightarrow A) \wedge X$. We want to reach a contradiction. To do that, we shall prove $X \leftrightarrow A$. We already have $X \rightarrow A$ by the first conjunct of the second assumption, and since we have $X$ by the second conjunct as well, we can just use $X \rightarrow (A \rightarrow X)$ to conclude $A \rightarrow X$ as well. Thus, $X \leftrightarrow A$, contradicting our first assumption.