Are these theorems really provable in PRA? In this article, Tait claims that $0 = 1 \Rightarrow \phi$ and $((\phi \Rightarrow 0 = 1) \Rightarrow0 = 1) \Rightarrow \phi$ are theorems of PRA (at least, of the formalization of PRA in this article, which employs a bit of type theory). Are there any proofs of these theorems, then?
 A: Tait's system does what he claims, but it seems to require some work to verify this.
First, notice that, for any two terms $a$ and $b$ of the same finitist type $A$, the primitive recursion construction of PRA provides a function $f:\mathbb N\to A$ such that $f(0)=a$ and $f(n')=b$ for all $n$. In particular, $f(0')=b$. So if $0=0'$ then $a=b$ (because Tait's logic includes the usual axioms and rules of identity). Thus, from $0=0'$, we can deduce all the atomic formulas (equations) of Tait's system. Then, thanks to the laws of implication that are also included in Tait's logic, we can deduce all formulas; they're implications, and thus they follow from their consequents. That is, repeatedly apply the rule "from $\phi$ deduce $\psi\to\phi$."
This gives the first claim: $0=0'\to\phi$. To get the second claim, we need another law of implication: From $(\phi\to\psi)\to\psi$ and $\psi\to\phi$, deduce $\phi$. To see that this is a valid rule of inference, just write out the truth table (or convince yourself that $(\phi\to\psi)\to\psi$ is equivalent to $\phi\lor\psi$) (or check that $((\phi\to\psi)\to\phi)\to\phi$ is a tautology). Now apply that rule with $0=0'$ as $\psi$, and use the fact that we've already proved $0=0'\to\phi$. So we get that $(\phi\to\psi)\to\psi$ implies $\phi$, as required.
(Side comment: The laws of implication mentioned in the last paragraph above are valid in classical logic but not in intuitionistic logic. That's unavoidable, because what's being proved, essentially the law of double-negation, is not intuitionistically valid.)
