Comment by lmm

Everything rests on the consistency of ZFC, which we can't prove. In some sense even results like 2+2=4 are provisional, because if ZFC were inconsistent (and we can't prove that it isn't) then it might also be true that 2+2=3 and 2+2=5.

(Well, strictly we can prove that 2+2=4 in Presburger arithmetic which is provably complete and consistent. But any result that we prove by contradiction and that uses the higher axioms (e.g. Hilbert's basis theorem) is implicitly assuming the (unprovable) consistency of ZFC).

Mostly this doesn't bother working mathematicians - ZFC seems reasonable, corresponds to the models that we do have, so we just take it on trust. People who care explicitly about these issues might work in a "higher" axiom system to prove "metamathematical" facts (e.g. ZFC + weakly inaccessible large cardinal, under which we can prove that ZFC is consistent and also that this particular Turing machine doesn't halt).

((Of course the whole point of Gödel's incompleteness theorems is that there's no sharp line between mathematical and metamathematical; any unproven proposition might turn out to be an unprovable landmine. But this doesn't tend to bother people. After all, the proposition might just as easily turn out to simply be very difficult to prove, and the practical impact would be much the same))