I'd separate the question whether mathematical statements are (often) existential from the question of the status of set theory. (Sure, we can construct faithful proxies inside set theory for most of the structures that mathematicians are interested in. But it is a moot question whether this makes set theory foundational in any good sense at all.)

Now, many mathematical statements are pretty uncontroversially not existential, but have the form "if anything is A it is B". So the theorem that anything which is a finite division ring is commutative doesn't tell us that there are such things as finite division rings, but only what they must be like if they do exist.

But of course many other common or garden mathematical theorems certainly do look existential. "There are an infinite number of prime numbers" looks existential -- and it is naturally read as implying that there are prime numbers (lots of them!). "There are four regular star polyhedra" looks existential -- and it is naturally read as implying that there are regular star polyhedra. And so it goes.

Perhaps appearances are deceptive, however. Perhaps these superficially existential statements are really non-committal "if ... then ..." statements in disguise. So really what we are saying, for example, is something along the following lines: if any collectionof things has the natural-number structure, then it contains an infinite number of things filling the prime-number role -- leaving it open whether there is anything that satisfies the antecedent of the conditional. Alternatively, maybe "there are an infinite number of prime numbers" is a statement made inside an essentially fictional mode of discourse (the arithmetical fiction), and no more really implies that there are numbers than "Sherlock Holmes lived at 222B Baker Street" implies that there really was such-and-such a man living along Baker Street.

Now, "if ... then ..."-ism and fictionalism are problematic as stories about the status of mathematics. I'm not recommending either position! But they are enough to illustrate the point that it isn't, perhaps, so obvious after all that prima facie existential mathematical statements have to be construed as really being kosher existential statements.

Stewart Shapiro's Thinking about Mathematics gives a terrific introduction to some of the issues hereabouts.

Just a footnote to Marc Lange's response (which seems spot on to me). It is worth adding that in serious analytical philosophy there is actually a good deal more agreement on arguments than there might appear to be at first sight, and there is a good deal of pretty secure knowledge.

For what often emerges from the to and fro of debate is essentially something of the form "If you accept A, B and C, then you'd better accept D too". Then one party might endorse A, B and C and conclude that D; and another party might think D is unacceptable, and conclude that one of A, B, or C must be wrong. And another party again (me, often!) might not know how to respond. [A trite example. If you accept act utilitarianism plus some other things, it seems that you should sanction the sheriff hanging an innocent man if that is the way to stop a riot in which more innocent people are killed. Some bite the bullett, some think so much the worse for utilitarianism.]

Now, there may indeed be a loud disagreement between the first two parties. But a lot of hard thinking may have gone into working out what they agree on, namely that "If you accept A, B and C, then you'd better accept D too". [For example, initially people might have thought, wrongly, that accepting A and B alone forced conclusion D, and it took some subtle argument to show that C was playing a role too. Working out what act utilitarianism really does sanction is like this.] And finding that sort of connection can represent a solid achievement of which we can be tolerably certain, even while there remains vigorous disagreement about what to do with the discovery.

Does there need to be a single, particular contribution that philosophical research makes and other disciplines fail ito make? Of course, science and math clarify concepts and contribute to making empirical predictions. Philosophical research does all of that, too, from time to time. I don't think there needs to be an interesting answer to "What does philosophy do?" that distinguishes philosophy from science and math. All are in pursuit of truth. Philosophers, scientists, and mathematicians are trained somewhat differently, often have somewhat different tools in their toolkits, and come out of somewhat (though overlapping) traditions and so will generally be familiar with different argumentative moves. But these may be differences in degree, not in kind.

The kinds of reasons that are given for favoring one scientific theory over its rivals are a good deal more subtle than "observation is king." To begin with, a theory need not be justly rejected merely because it conflicts with a given observation; sometimes, the observation is appropriately doubted, and sometimes, a given theory is rationally retained despite its failure to fit our observations because blame for the mismatch is placed on other theories ("auxiliary hypotheses") that were used to bring the theory to bear on those observations. (The Copernican model of the solar system, for instance, was retained despite 300 years of failure to observe the stellar parallax it apparently predicts.) By the same token, a theory that fits our observations very well may nevertheless be justly and emphatically rejected on the grounds that it is ad hoc, fails to fit nicely with our other theories, lacks unity or fruitfulness or explanatory power, etc.

Once these familiar features of scientific practice are recognized, then I think the choice among theories in philosophy seems not so dissimilar to the choice among competing scientific theories. Admittedly, much of philosophy is a priori, unlike science. However, the virtues of elegance, parsimony, unity, coherence, explanatory power, and so forth play significant roles in both scientific and philosophical theory-choice.

Finally, philosophy has long been and is increasingly brought into contact with empirical results. A philosophical analysis of causal relations, for instance, that fails to do justice to modern physics has a severe deficiency. Of course, philosophers will disagree about the extent to which modern physics (or even classical physics) discovers causal relations, as well as disagreeing about what physics has revealed about them. Nevertheless, philosophical theorizing hardly takes place in isolation from empirical results. Recent literature in the philosophy of mind and perception offers a host of tremendously potent examples of this.

Actually, the presumption here is wrong. It isn't the case that "much of philosophy is concerned with providing a rigorous foundation to truths which are otherwise intuitive and uncontroversial". In particular, that isn't the case in the philosophy of mathematics.

Of course, famously, Frege tried to show that the basic laws of arithmetic (and hence the proposition 1+1 = 2) can be derived from the laws of logic plus definitions. But he did this in order to defend the claim that arithmetical truths are analytic, true in virtue of logic alone, and so explain why those truths are necessarily true and why they necessarily apply to everything. He didn't claim that, prior to his attempted derivation of 1+1 = 2 from pure logic, no one knew it to be true. Rather we weren't in a good position to see clearly the sort of truth that it is, analytic according to Frege.

Unfortunately, one of Frege's putative laws of logic turned out to lead to contradiction, and his foundational edifice crumbled (though neo-Fregeans think that much can be rescued). In part as a response, Russell and Whitehead also famously tried to show that the basic laws of arithmetic can be derived from a small number of more basic laws. But again, it wasn't that they thought that, prior to deriving 1+1 = 2, there is a serious question mark over its truth. In fact, for them, it is the other way about: the rationale for accepting some of the laws of their basic "type theory" is regressive: that is to say, we are to accept their "foundational" laws here rather as we accept laws in physics -- i.e. they generate consequences which we already know to be true.

These days, students are taught how a vast amount of mathematics can be regimented in ZFC (Zermelo Fraenkel set theory with the Axiom of Choice), and in particular are told how to derive proxies for the Peano Axioms for arithmetic, and hence for 1+1 = 2, inside ZFC. One point of this regimenting project is that it gives us a way of calibrating the infinitary commitments of different areas of mathematics by measuring different bits of mathematics against a common yardstick. But again, it isn't as if set theorists think that the basic principles of ZFC are more secure than those of simple arithmetic. On the contrary.

Frege, Russell and Whitehead, and modern set theorists all knew/know that 1+1=2 in the same way we all do. But what that involves is, indeed, another question.

As Peter Smith's examples make clear, sometimes "the philosophy of mathematics" appears in other than philosophy journals and is done by other than people in philosophy departments. Another instance of this is the long current of constructivism in mathematics. The development by mathematicians of constructivist mathematics (most notably, intuitionistic mathematics) is often motivated by their -- for want of a better term -- philosophical reflection on the nature of mathematics.

Three examples to think about. First, Frege's invention of the predicate calculus was driven by philosophical reflection on the nature of quantified propositions, and led in turn to modern mathematical logic. Second, the so-called Hilbert programme was driven in part by more philosophical reflection, this time on the limits of what we can directly "intuit" to be mathematically correct; that programme led in turn to the development of modern proof theory. Third, Kurt Gödel's philosophically driven work on set theory was mathematically hugely important. [Sorry, those reference links are inevitably to material that quickly gets mathematically heavy!]

So, it surely is the case that specific philosophical ideas -- philosophical reflections on foundational matters -- have influenced the development of mathematics. And one might say too that a more general set of philosophical ideas about the proper nature of mathematics drove the whole Bourbaki project which has been so influential in the development of modern mathematics.

On the other hand, it has to be said that a lot of the obsessions of contemporary philosophers of mathematics do leave working mathematicians stone cold! For example, a "hot topic" among the philosophers is the pros and cons of "fictionalism" about mathematics -- the idea that, strictly speaking, it isn't really true that 2 + 2 = 4 , any more than it is strictly speaking true that Sherlock Holmes lived at 222B Baker Street. There aren't really numbers sitting in some Platonic heaven, any more than there is a detective living in Baker Street. Strictly speaking, we should say that according to Conan Doyle's fiction, Sherlock Holmes lived at 222B Baker Street. Likewise, the argument goes, we should say that according to the mathematical fiction, 2 + 2 = 4. But try that on your local friendly number-theorists and they will glaze over, or think you are joking!

Once upon a time, I used to teach introductory logic using Lemmon's textbook. And some exam questions would have the form "Use truth-tables to test the following arguments for validity; in the cases where the argument is valid, provide a proof from the premisses to the conclusion in Lemmon's system". Given that Lemmon's natural deduction system is complete, a student who correctly did a truth-table showing that a particular argument is valid thereby proved that there is a proof from the premisses to the conclusion. But of course, she had to do more to answer the second part of the question, and get the marks! She had to give an actual natural deduction proof.

Which reminds us that, quite often, we aren't just looking for any old proof, but for a proof of a certain style S, a proof that uses certain kinds of resources. And proving that an S-proof of some result exists isn't in general to give an S-proof. This sort of point applies outside the logic classroom too. For example, a number theorist may be quite convinced that there must be an "elementary", purely numerical, proof of some result about the prime numbers (for example) because she knows the result is true since there is a fancy heavy-duty proof of it calling on more exotic mathematics. Actually finding a more elementary proof itself be a hard problem.

But let's suppose now that we are approaching some problem with no particular presumptions about the general kind of proof we want. Then, in this sort of case, is proving that a proof exists as good as finding "the actual proof"?

Well, here's another story. The great mathematician Paul Erdös liked to talk of "The Book" in which God keeps the most beautiful mathematical proofs. And there's a lovely volume Proofs from The Book which gives us lots of really elegant proofs of the kind Erdös had in mind. The very first chapter -- which is pretty accessible even if you know just a smidgin of mathematics -- gives no less than six proofs (taken from a much longer list, say the authors) that there is an infinite number of primes. Which is a vivid reminder that there need be no such thing as "the actual proof" of a result, even if we are only looking at proofs worthy of being put into The Book.

So let's rephrase the question again. Suppose we are approaching some problem "is it the case that P?" with no particular presumptions about the kind of proof we want. Then could something describable as proving that there is a proof that P be one acceptable way of demonstrating that P is true?

To which the answer seems to be "Yes". (Perhaps some cases where we give computer aided proofs, using the computer to prove that a formalized proof is well-structured, could be said to fall under that description.)

There are lots of physicists who study the history of the universe: how the universe began, for example. When they do their calculations concerning, say, the evolution of the universe in the few seconds following the big bang, they do seem to assume that the square root of 81 was 9 even then, when there were no minds. And more generally, it's rather hard to see how the existence or non-existence of minds could affect what the square root of 81 is. Might 81 itself not have existed had there been no minds? How precisely did the existence of minds bring it into being? Was it just impossible before there were minds for there to be 81 stars in a certain region of space? I think not.

This kind of concern has had a good deal of influence on research in logic over the last several decades. It was, for example, a major force behind Boolos's work on plural quantification.

More recently, there has been an explosion of research on what is called "absolutely universal" quantification: quantification over absolutely everything, including all the sets there might be. As you note, there is no "model" of such discourse, in the usual sense; that is, the "intended interpretation" of such discourse cannot be a model, in the usual first-order sense. As Dan noted, one can talk about proper class models, but there is another line of inquiry, deriving from Boolos. One way to develop this approach is to take the domain of the interpretation to be a `plurality', so that the quantifiers range over the sets---not the set ofall sets, or a class of all sets, but simply over the sets, whatever sets there may be. The details have to be worked out here, but it can be done, and in a reasonable way, too, as Tim Williamson and Agustin Rayo have shown.