[momentoftop]

Yes, as I said: systems such as Russell's encoded "1", "2" and "+" in such a way that the theorem "1 + 1 = 2" is non-trivial to prove. This doesn't say anything about the difficulty of proving that 1 + 1 = 2, but merely the difficulty of proving it in a particular logical encoding. Poincare ridiculed the Principia on this point almost immediately.

And had Russell failed to prove that 1 + 1 = 2 in his system, it would not have cast one jot of doubt on the fact that 1 + 1 = 2. It would only have pointed to the inadequacy of the Principia.