You guys are basically arguing over Moore's here-is-one-hand problem. https://en.wikipedia.org/wiki/Here_is_one_hand https://en.wikipedia.org/wiki/Here_is_one_

You guys are basically arguing over Moore's here-is-one-hand problem. https://en.wikipedia.org/wiki/Here_is_one_hand https://en.wikipedia.org/wiki/Here_is_one_hand pavelrub's point is that you sometimes have less reason to believe the axioms of your formalization than their derived consequences. We have better reason to believe the intuitive idea that 2+2=4 than we do any putative axioms of arithmetic. If we derived that 2+2=5 from some particular axioms of arithmetic, we would conclude those axioms were wrong (or rather, were not the proper system for formalizing 2-plus-2-ness) rather than conclude that 2+2=5.