Not a correction (because this is all philosophy) but the problem with this “hard formalism” stance:
Mathematical truth is very much about provability from axioms.
is that statements of the form “statement x follows from axiom set S” are themselves arithmetical statements that may or may not even be provable from a given standard axiom system. I would guess that you’re implicitly taking for granted that Σ1 and Π1 statements in the arithmetic hierarchy have inherent truth in order to at least establish a truth value for such statements. Most people do this implicitly; it’s equivalent to saying that every Turing machine either halts or it doesn’t (and the behavior has nothing to do with someone’s axiom system).
Not a correction (because this is all philosophy) but the problem with this “hard formalism” stance:
is that statements of the form “statement x follows from axiom set S” are themselves arithmetical statements that may or may not even be provable from a given standard axiom system. I would guess that you’re implicitly taking for granted that Σ1 and Π1 statements in the arithmetic hierarchy have inherent truth in order to at least establish a truth value for such statements. Most people do this implicitly; it’s equivalent to saying that every Turing machine either halts or it doesn’t (and the behavior has nothing to do with someone’s axiom system).