Can, or should, we ignore uncountable models of set theory? This question is based off of a post I saw on the Physics StackExchange:
https://physics.stackexchange.com/questions/20370/does-the-banach-tarski-paradox-contradict-our-understanding-of-nature
While the question refers to physics, it also refers to mathematics. From the third answer on the page:

Even within pure mathematics, the mechanism of logical deduction is always a finite computation. If you are given a well defined collection of axioms, or axiom schemas all of whose axioms can be listed by a computer program (this includes every reasonable mathematical theory), you can write a computer program to deduce all the consequences of these axioms. Godel's completeness theorem states that every deduction will be reached by the rules of first order logic, and that when there is an undecidable statement, one which cannot be proved or disproved by the axioms, there is always a model of the axioms where the statement is true, and a model where the statement is false.
This means that when you are given a set theory, which talks about infinite non-denumerable collections, you can understand that the theory is really talking about its countable models, and this gives a countable computational interpretation to every theorem. You can then ignore the jibber-jabber about the theory talking about some enormous sets, and consider the theory as talking about its countable models.

(You might also need some of the context from the post, it's fairly long)
Now, while a countable model of (say) ZFC is possible, what I'm wondering about is does the "computational" nature of logic render the idea of "enormous" sets as just "jibber-jabber" that you don't need? Or perhaps, maybe a better way of asking the question is: how come that many (I believe) mathematicians would imagine there to really be such a vast, uncountable set when they think of, say, the Reals, as opposed to it "really" being countable inside a countable model of ZFC? What's the strongest justification that can be given for this view and also for the view (if possible) mentioned in the quoted message?
I suppose this also ties into a similar question I have been wondering about: namely, that is, given the very fact that there is not one single model of ZFC, how can we trust that familiar objects like the Reals are "what we think they are"? Namely, am I right in believing there exist models of ZFC where the model of the natural numbers is (when viewed from "outside") a "non-standard model of arithmetic", and therefore the naturals and the Reals contain nonstandard numbers: numbers that from "outside" look to be "infinitely big" and "infinitely small"? If so, then how do we reconcile this with the fact our intuition about the reals says no such things should exist -- though of course since we cannot "see" them from inside the model, it doesn't affect the math done within ZFC?
 A: The theorems of ZFC can, indeed, be regarded as telling us what happens in countable models of ZFC. But they also tell us (some of) what happens in the universe of all sets, and that is the primary purpose for which the ZFC axioms were invented. The fact that the axioms also have countable models is the price (or one of the prices) we pay for using first-order axioms. (The benefit that compensates for this cost is that first-order logic admits a complete system of logical axioms and rules of inference.)  If someone wants to ignore the universe of all sets and to ignore uncountable models, limiting their attention to countable models, that's OK, but I don't see that much is gained thereby unless either (1) you adopt a philosophical position which, for some reason, regards countably infinite sets as OK whiule rejecting uncountable sets or (2) you enjoy saying "jibber-jabber".  Personally, I find it not only more interesting but also easier to think about real numbers than to think, for all countable models simultaneously, about the real numbers of those models. 
Near the end of the text that you quoted, there is something I don't understand, about giving "a countable computational interpretation to every theorem." Even if one thinks of just one countable model of ZFC, the interpretation in that model of a typical theorem will involve numerous nested quantifications over that countable domain.  Calling such an interpretation "computational" seems quite a stretch. If one thinks not of just one countable model but of all countable models together, things look even less computational to me.  Indeed, the only computational thing I see in any of this is that there is a computational, syntactic process that generates (by formal deduction) all the theorems of ZFC.  But that process doesn't depend in any way on what semantical interpretation (countable models, or arbitrary models, or even the whole universe) we use for ZFC, or even whether we use a semantical interpretation at all.
Finally, to answer another part of your question: Yes, the countable models of ZFC will include some whose natural numbers, seen from the outside, are nonstandard.  This, like the very existence of countable models, is a consequence of the use of first-order logic in formulating ZFC. 
A: The issue here is that often we don't work with models of $\sf ZFC$. We work with the entire universe, and with its inner models. This means that our "model" has no cardinality to begin with.
The real numbers of the universe do make an uncountable set, and it can be a very large uncountable set, or a very small uncountable set. We can't decide from just the assumptions of $\sf ZFC$ being true in our universe. Moreover, sometimes we will have inner models which only know about a few real numbers and sometimes we will have inner models which know about a lot of real numbers.
Model theory tells us that if there is a countable model of $\sf ZFC$ then there is an uncountable model of $\sf ZFC$. This is much like any other first-order theory. This includes the real numbers (as a real-closed field) and the natural numbers. It is true, however, that there is no "canonical" second-order model of $\sf ZFC$.
To your quoted text, it comes from a person which sneered at the inaccessible cardinal requirement in Solovay's work (which was later proved to be essential); and openly states that he believes the continuum cannot be a set but a proper class. I don't think that this sort of person has a lot of saying in what is $\sf ZFC$ and modern set theory related to it. Note that he also points out that if the axiom of choice for sets of size $\Bbb R$ fails, then Banach-Tarski fails, which is another mistake. We can have the continuum well-ordered, say of size $\aleph_2$, but generally the axiom of choice for families of size $\aleph_2$ fails. In that case, the Banach-Tarski paradox would still hold.

No. Set theory is not just about computable and computations of proofs. One does uses uncountable sets, because when working internally to some model, you are not allowed to use the enumerations that exist outside (at least not for arguments within the model, as we often do).
If one wishes to base mathematics on set theory, then one works internally to models of $\sf ZFC$ or any other chosen set theory. By working internally uncountable sets are uncountable. Period.
Recently there has been some movement towards a philosophical point of view of the multiverse, in particular by Joel D. Hamkins. One of the multiverse axioms is that every model of set theory is countable in some other model of set theory. But the multiverse is not essential for developing modern mathematics within set theory, or classical mathematics without $\sf ZFC$ (without any other extensions).
Let me just finish that the distinction of "internal" and "external" to a model are notions which baffle professional mathematicians, and sometimes even set theorists. Don't be thrown off by your confusion, we all get confused sometimes.
