Does this variant of Peirce's law hold in intuitionistic logic? $\vdash ((A \rightarrow B) \rightarrow A) \implies \vdash A$ In intuitionistic logic, Peirce's Law, $((A \rightarrow B) \rightarrow A) \rightarrow A$, does not hold.
However, I am wondering about a slight modification to this same law:
$$\vdash ((A \rightarrow B) \rightarrow A) \text{ implies } \vdash A$$
i.e., if $(A \rightarrow B) \rightarrow A$ is provable, then $A$ is also provable, for any values of $A$ and $B$.
My question is: does this meta-version of Peirce's Law hold in intuitionistic logic? I'm asking this question after trying unsuccessfully to find any counter-examples, but also not knowing how to prove the validity of such a statement.
I'm looking for either (1) a proof that it holds, or (2) a counter-example (showing, for some $A$ and $B$, an intuitionistic proof of $(A \rightarrow B) \rightarrow A$, where $A$ is not provable in intuitionistic logic).
 A: In regards to your other question, the deduction theorem holds for intuitionistic logic, so your "meta" version is equivalent to the non-meta version.
The issue is that what you're asking for is not the negation $((A\to B)\to A)\vdash A$. $((A\to B)\to A)\vdash A$ states "given a proof of $(A\to B)\to A$, then you could make a proof of $A$". To refute this, I don't need to provide a proof of $(A\to B)\to A$, I need to show that even if I had a proof of $(A\to B)\to A$ I could not use it to make a proof of $A$. You are confusing "not provable" with "refutable", i.e. "the negation is provable".  It impossible to provide a "counter-example" in the sense that you want, because every theorem of intuitionistic logic is a theorem of classical logic, so such a counter-example would also need to work in classical logic. That is to say, just because I can't provide a proof doesn't mean I can provide a refutation.
To actually prove this there are two approaches: the syntactic approach or the semantic approach. The semantic approach is good for counter-examples, the syntactic approach less so. 
The syntactic approach to this would be to show that such a derivation doesn't exist, and this would require an induction on possible derivations (possibly hidden in some other theorem). Cut-elimination and normalization theorems are useful here since you can consider only "normal form" derivations, and those are much easier to deal with. Still, such proofs are tedious.
The semantic approach, as I said, is much easier. Any model of intuitonistic propositional logic that doesn't validate Pierce's Law (i.e. that isn't also a model of classical logic) will provide a semantic counter-example showing that no proof exists. (Of course, per the previous paragraph, this relies on a soundness theorem which will involve an induction on derivations.) As a simple counter-model, let $X$ be a topological space with open subsets $\mathcal{O}(X)$. This forms a model of intuitionistic logic which will usually not also be a model of classical logic, e.g the open sets of the real line with the usual topology. In this model, propositions correspond to open subsets of $X$, e.g. unions of open intervals. $\Gamma\vdash U$ is interpreted simply as $\bigcap\Gamma\subseteq U$, in particular $\vdash U$ means $X \subseteq U$ and so $U = X$. Finally, for our purposes, $U\to V$ is interpreted as $\bigcup\{W\in\mathcal{O}(X)\mid W\cap U\subseteq V\}$, i.e. the largest open subset of $X$ whose overlap with $U$ is contained in $V$. In particular, $U\to\emptyset$, i.e. $\neg U$, is the interior of the complement of $U$. Choosing $A = U$ and $B = \emptyset$, we need to show that there is a topological space $X$ and open subset $U$ such that $\neg U \to U \nsubseteq U$. Using $\mathbb{R}$, pick $U=(0,1)\cup(1,2)$. $\neg ((0,1)\cup(1,2))$ is thus $(-\infty,0)\cup(2,\infty)$. $$\neg U \to U = ((-\infty,0)\cup(2,\infty))\to ((0,1)\cup(1,2)) = (0,2) \nsubseteq ((0,1)\cup(1,2)) = U$$
A: I've realized that a counter-example exists, so my modification to Peirce's law does not hold in intuitionistic logic.
We must find some $A$ and $B$ such that $A$ is not provable in intuitionistic logic, while $(A \to B) \to A$ is provable in intuitionistic logic.
Let $A = \neg \neg P\to P$, and let $B = \neg P$
$A$ is clearly not provable in intuitionistic logic, since it is equivalent to the double negation elimination rule, which does not hold intuitionistically.
It remains to prove: $((\neg\neg P \to P)\to\neg P) \to (\neg\neg P \to P)$


*

*Suppose $(\neg\neg P \to P)\to\neg P$  

*Since it's tautologically true that $P\to (\neg\neg P \to P)$, we can deduce that $P\to\neg P$. Therefore, $\neg P$.

*Now suppose $\neg\neg P$. But this contradicts $\neg P$. Therefore, by the principle of explosion, we can say: $\neg\neg P \to P$. 

*Therefore, $((\neg\neg P \to P)\to\neg P) \to (\neg\neg P \to P)$, Q.E.D.


Since this proof requires the principle of explosion to work, I believe my modified version of Peirce's law would still hold in minimal logic.
Edit: It doesn't hold in minimal logic either. Proof:
Let $A = ((P\to Q)\to P)\to P$, let $B = P\to Q$.
$A$, being equivalent to Peirce's Law, is clearly not provable in minimal logic.
It remains to prove: $((((P\to Q)\to P)\to P)\to (P\to Q))\to (((P\to Q)\to P)\to P)$


*

*Suppose $(((P\to Q)\to P)\to P)\to (P\to Q)$.

*Since it's tautologically true that $P\to (((P\to Q)\to P)\to P)$, we can deduce from (1) that $P\to(P\to Q)$, and hence that $P\to Q$. 

*Suppose, in addition, that $(P\to Q)\to P$. Then we can deduce $P$, by modus ponens from (2). Therefore, $((P\to Q)\to P)\to P$.

*Therefore, $((((P\to Q)\to P)\to P)\to (P\to Q))\to (((P\to Q)\to P)\to P)$, Q.E.D.

