Does $\mathsf{ZFC} + \neg\mathrm{Con}(\mathsf{ZFC})$ suffice as a foundations of mathematics? I've heard people make the argument that:

$\mathsf{ZFC}$ suffices as a foundations of mathematics because almost all theorems in the mathematics literature can be proven using $\mathsf{ZFC}$, so long as they're suitably translated into the language of sets.

Now let $\mathrm{Con}(\mathsf{ZFC})$ denote the statement that $\mathsf{ZFC}$ is consistent, formalized in the language of $\mathsf{ZFC}$. By Godel's second incompleteness theorem, if $\mathsf{ZFC}$ is consistent, then so too is $\mathsf{ZFC}+\neg\mathrm{Con}(\mathsf{ZFC})$.
Observe also that the above argument works for $\mathsf{ZFC}+\neg\mathrm{Con}(\mathsf{ZFC})$.
Thus, would $\mathsf{ZFC}+\neg\mathrm{Con}(\mathsf{ZFC})$ suffice as a foundations? And if so, why is nobody using it? (okay, clearly there are psychological reasons why nobody is using it - but are there deeper reasons?)
 A: The problem with the system you propose is that we add to ZFC a statement that in the background we assume (or hope) that is false. Specifically, doing mathematics using ZFC relies on the fact that (a sizeable fragment of) ZFC is consistent. We don't want to have a contradictory system, because contradictions are analytic falsehoods that never take place and (hence) imply everything (at least in the most common logical systems).
The statement $\mathrm{Con(ZFC)}$ is a statement about finite objects (e.g. numbers) and the fact that we have a lot more intuition about these kinds of objects implies that we have a lot more expectations about the accuracy (with respect to our intuition) of a theory that describes these objects. 
So, if ZFC is inconsistent so is the theory that you propose (since it extends ZFC). On the other hand, if ZFC is consistent, any model of the theory that you propose will have numbers (or finite objects) that should not exist. The witness of the existential statement that you propose we add will not be an actual natural number (or something that our intuition will describe as a natural number).
Personally, I think this is a strong argument as to why this system is not a good extension of ZFC. We want set theory to accurately describe finite objects, and the extra axiom that you propose goes against that.
A: There are three main problems with the theory you propose. 


*

*Often when we want to use forcing we assume there are countable transitive models of $\sf ZF$ (with additional axioms, of course, such as choice, large cardinals, and so on).
Indeed this problem is merely cosmetic, we can work around it using several approaches, but it would require us to say "Let $M$ be a countable transitive model of enough axioms of $\sf ZF$" every time, which is quite annoying. 

*A more severe problem would be with large cardinals. If $\sf ZFC$ is internally inconsistent, then there are no large cardinals in the universe, and there are no set models of $\sf ZFC$ with large cardinals. Since those are needed for more than a handful results, and they do make a wonderful and deep research topic in set theory, the assumption that $\sf ZFC$ is internally inconsistent would simply eliminate this entire field.

*Often we like to think of the integers in the meta-theory (i.e. in the logic outside the universe) as the same integers as those of the universe. But in a universe where $\sf ZFC$ is internally inconsistent there is a proof of that, but this proof cannot be encoded by a standard integer. Therefore there must be a non-standard integer.
As with the issue about forcing, this too is probably a cosmetic and convenience issue to some extent, but it is also a psychological point that I find reassuring to think that the "real" universe of sets have the same integers as those we can write in the first-order logic of its meta-theory.
From the last point, let me draw my final conclusion, which is probably a psychological issue here. Foundational theories should be something that you believe is a good basis to develop mathematics within. If you believe that $\sf ZFC$ is a reasonable foundation, then of course you can talk about models of $\sf ZFC+\lnot\rm Con(\sf ZFC)$ because it is a larger theory. But it would mean that from a foundational point of view, you probably don't think that $\sf ZFC$ is consistent, so your entire foundation is inconsistent.
The fact that $\sf ZFC+\lnot\rm Con(\sf ZFC)$ is consistent, if $\sf ZFC+\rm Con(\sf ZFC)$ is consistent, is a peculiarity of how mathematics works. Much like the many other peculiarities that we can find in universes of set theory.
