No answer addresses the "bottleneck" question. It's not surprising to me because the question is vague. But I would like to know whether that is indeed the reason, or perhaps something else. The question is interesting to me and I would be grateful for any help with it.
Unfortunately, there will be a bit of vagueness in this question because of its nature and because of my limitations. I would like to ask for your understanding and help with the formulation, if they're possible.
I know (although without knowing the proof) that the consistency of ZF or ZFC cannot be proven within these theories, but their inconsistency can if they are inconsistent. I have read -- to my relief -- that it is considered unlikely that they are inconsistent. I would like to understand this statement better.
One simple argument that comes to mind is that no contradiction has been found so far, even though the theories have been extensively researched. But this alone seems a bit weak to me. The space of all provable statements in ZF or ZFC is clearly infinite. I have noticed that when mathematicians make statements about the likelihood of the truth of statements about elements of infinite classes, they usually give finer arguments than just the truth of the statement for the elements of some finite subclass. For example, many mathematicians seem to believe that Goldbach's conjecture is true, and they base their belief on theorems about the distribution of prime numbers in natural numbers.
Are there any arguments of this kind (unfortunately, I don't seem to be able to define what "this kind" means precisely here) for there not being a contradiction in ZF or ZFC? I've been thinking about how it could happen that there would actually be a contradiction in, say, ZF. I think we could define the "length" of a theorem in ZF to be the minimal number of symbols in a proof of the theorem. (Please tell me if there is something wrong with such a definition.) If we assume that ZF is inconsistent, then the proof of its inconsistency has a finite length, say $n$. For every natural number $k$ there is a finite number of theorems of length at most $k$, so we should be able to tell when we have proven all theorems of length at most $k$. The mathematical community has proven many theorems in ZF. Is it known how far we have gotten in this scale? For example, have we gotten past $k=10$? Let $m$ be the greatest natural number such that all theorems of length at most $m$ are known. Clearly, $n$ would have to be greater than $m$.
But I think many theorems must have been proven with length greater than $m$. Can we meaningfully talk about the chance of hitting the proof of the contradiction of ZF by making random correct reasonings of length $\geq n$? I've been trying to define an "inference bottleneck" that could cause the contradiction to be hard to hit, but I've failed. Since I haven't defined it, it may be difficult or impossible to understand what I mean by "inference bottleneck", but I hope it's not. I mean a theorem that can be proven by only a "small" number of reasonings, only I have trouble saying exactly in comparison to what it should be small.
I would like to ask if it actually is possible to define such "bottlenecks" and if so, would it be possible to prove that they cannot be too narrow? I'm thinking such a theorem could be a more convincing argument for there not being a contradiction in ZF.
And the more general question, to reiterate it, is what other arguments mathematicians (or philosophers?) give for ZF and ZFC being consistent. The belief in the consistency of those theories seems to me to be very strong among mathematicians, even though they tend to be very careful about saying things about other unproven statements. Why is that?