 For atomic sentences like \(1\ne 1\) the translation \(\tau\) is clearly the identity, and the provability of \(1\ne 1\) in PA would imply its provability in HA. Thus, PA is consistent relative to HA. This result is technically of great interest and had a profound effect on the perspective concerning the relationship between finitism and intuitionism: finitist and intuitionist mathematics were considered as co-extensional; this theorem showed that intuitionist mathematics is actually stronger than finitist mathematics. Thus, if the intuitionist standpoint is taken to guarantee the soundness of HA, then it guarantees the consistency of PA. The corresponding connection between classical and intuitionist logic had been established already by Kolmogorov (1925) who not only formalized intuitionist logic but also observed the translatability of classical into intuitionist logic. His work, though, seems not to have been noticed at the time or even in 1932, when Gentzen and Gödel established their result for classical and intuitionist arithmetic.