I agree with the main tenets of your view - rejecting the platonic realm of mathematical truths, instead founding mathematics rigorously and finitely on formal systems - but you do not hold fast to it, for example the notion of a formal system "talking about itself" is appears deeply semantic rather than syntactic.
I will speak informally about rigorous mathematics.
to prove that □ does what we think it does, we have to appeal to second-order arithmetic
There are two ways I can communicate to you what PA is:
It is not possible to consider Godel's theorem with only a direct understanding of PA, you need an implemented one. This isn't a problem though, suppose you had a direct understand of PA and any understanding of ZFC, it's very easy to give an implemented understanding of PA because you can easily check that my implementation corresponds to your direct understanding by checking it axiom at a time.
I don't consider formal systems to talk about themselves
Inside our implemented PA we construct a predicate and then prove in ZFC that it satisfies a particular property defined in terms of PA. Specifically we construct a PA formula Bew which in ZFC is proved to satisfy a specification stating that PA |- P is equivalent to PA |- Bew("P"). (I am just making up symbols here, Godel uses a different notation, if it's not clear I can write it out much more formally but I'm sure this make sense). This dissolves the question of whether PA "talks about itself" or not without infinite regress, because one must have a direct understanding of some foundation to ever get started doing rigorous mathematics.
it is a basic principle of my philosophy that [..] formal systems [are real]
This doesn't make sense to me. I have no idea what real means here. PA was created by Peano, of course if he communicated this theory to someone else (by either of the means defined earlier) or someone independently came up with an isomorphic system they will prove the same theorems. This surprising coincidence can be very misleading (it is the cause of platonism after all!) so it is important that one realize why two people share the same theorems: because they start from the same axioms and apply the same deduction rules! Not because there is some magical spirit realm of mathematical truths which they divine from.
I agree with the main tenets of your view - rejecting the platonic realm of mathematical truths, instead founding mathematics rigorously and finitely on formal systems - but you do not hold fast to it
This is because you have misconstrued my view. My philosophy of syntacticism is not formalism, nor is it a straight rejection of Platonism. Instead it is a Platonic formalism, in which the Platonic ideals are of the form "thus-and-such is derivable from these axioms with these deduction rules", except that any attempt to talk directly and formal...
I've mentioned in comments a couple of times that I don't consider formal systems to talk about themselves, and that consequently Gödelian problems are irrelevant. So what am I actually on about?
It's generally accepted in mathematical logic that a formal system which embodies Peano Arithmetic (PA) is able to talk about itself, by means of Gödel numberings; statements and proofs within the system can be represented as positive integers, at which point "X is a valid proof in the system" becomes equivalent to an arithmetical statement about #X, the Gödel number representing X. This is then diagonalised to produce the Gödel sentence (roughly, g="There is no proof X such that the last line of X is g", and incompleteness follows. We can also do things like defining □ ("box") as the function from S to "There is a proof X in PA whose last line is S" (intuitively, □S says "S is provable in PA"). This then also lets us define the Löb sentence, and many other interesting things.
But how do we know that □S ⇔ there is a proof of S in PA? Only by applying some meta-theory. And how do we know that statements reached in the meta-theory of the form "thus-and-such is true of PA" are true of PA? Only by applying a meta-meta-theory. There is no a-priori justification for the claim that "A formal system is in principle capable of talking about other formal systems", which claim is used by the proof that PA can talk about itself. (If I remember correctly, to prove that □ does what we think it does, we have to appeal to second-order arithmetic; and how do we know second-order arithmetic applies to PA? Either by invoking third-order arithmetic to analyse second-order arithmetic, or by recourse to an informal system.)
Note also that the above is not a strange loop through the meta-level; we justify our claims about arithmeticn by appeal to arithmeticn+1, which is a separate thing; we never find ourselves back at arithmeticn.
Thus the claim that formal systems can talk about themselves involves ill-founded recursion, what is sometimes called a "skyhook". While it may be a theorem of second-order arithmetic that "the strengthened finite Ramsey theorem is unprovable in PA", one cannot conclude from second-order arithmetic alone that the "PA" in that statement refers to PA. It is however provable in third-order arithmetic that "What second-order arithmetic calls "PA" is PA", but that hasn't gained us much - it only tells us that second- and third-order arithmetic call the same thing "PA", it doesn't tell us whether this "PA" is PA. Induct on the arithmetic hierarchy to reach the obvious conclusion. (Though note that none of this prevents the Paris-Harrington Theorem from being a theorem of n-th order arithmetic ∀n≥2)
What, then, is the motivation for the above? Well, it is a basic principle of my philosophy that the only objects that are real (in a Platonic sense) are formal systems (or rather, syntaxes). That is to say, my ontology is the
setclass of formal systems. (This is not incompatible with the apparent reality of a physical universe; if this isn't obvious, I'll explain why in another post.) But if we allow these systems to have semantics, that is, we claim that there is such a thing as a "true statement", we start to have problems with completeness and consistency (namely, that we can't achieve the one and we can't prove the other, assuming PA). Tarski's undefinability theorem protects us from having to deal with systems which talk about truth in themselves (because they are necessarily inconsistent, assuming some basic properties), but if systems can talk about each other, and if systems can talk about provability within themselves (that is, if analogues to the □ function can be constructed), then nasty Gödelian things end up happening (most of which are, to a Platonist mathematician, deeply unsatisfying).So instead we restrict the ontology to syntactic systems devoid of any semantics; the statement ""Foo" is true" is meaningless. There is a fact-of-the-matter as to whether a given statement can be reached in a given formal system, but that fact-of-the-matter cannot be meaningfully talked about in any formal system. This is a remarkably bare ontology (some consider it excessively so), but is at no risk from contradiction, inconsistency or paradox. For, what is "P∧¬P" but another, syntactic, sentence? Of course, applying a system which proves "P∧¬P" to the 'real world' is likely to be problematic, but the paradox or the inconsistency lies in the application of the system, and does not inhere in the system itself.
EDIT: I am actually aiming to get somewhere with this, it's not just for its own sake (although the ontological and epistemological status of mathematics is worth caring about for its own sake). In particular I want to set up a framework that lets me talk about Eliezer's "infinite set atheism", because I think he's asking a wrong question.
Followed up by: The Apparent Reality of Physics