It is well known that intuitive set theory (or naive set theory) is characterized by having paradoxes, e.g. Russell's paradox, Cantor's paradox, etc. To avoid these and any other discovered or undiscovered potential paradoxes, the ZFC axioms impose constraints on the existense of a set. But ZFC set theory is build on mathematical logic, i.e., firstorder language. For example, the axiom of extensionality is the wff $\forall A B(\forall x(x\in A\leftrightarrow x\in B)\rightarrow A=B)$. But mathematical logic also uses the concept of sets, e.g. the set of alphabet, the set of variables, the set of formulas, the set of terms, as well as functions and relations that are in essence sets. However, I found these sets are used freely without worrying about the existence or paradoxes that occur in intuitive set theory. That is to say, mathematical logic is using intuitive set theory. So, is there any paradox in mathematical logic? If no, why not? and by what reasoning can we exclude this possibility? This reasoning should not be ZFC (or any other analogue) and should lie beyond current mathematical logic because otherwise, ZFC depends on mathematical logic while mathematical logic depends on ZFC, constituting a circle reasoning. If yes, what we should do? since we cannot tolerate paradoxes in the intuitive set theory, neither should we tolerate paradoxes in mathematical logic, which is considered as the very foundation of the whole mathematics. Of course we have the third answer: We do not know yes or no, until one day a genius found a paradox in the intuitive set theory used at will in mathematical logic and then the entire edifice of math collapse. This problem puzzled me for a long time, and I will appreciate any answer that can dissipate my apprehension, Thanks!

7$\begingroup$ If yes, what we should do? Read the introductory material in a basic textbook on mathematical logic? $\endgroup$– Gerald EdgarApr 24 '11 at 12:09

15$\begingroup$ I have read serveral basic textbook on mathematical logic, but none of them answers my question successfully. $\endgroup$– zzzhhhApr 24 '11 at 12:36

6$\begingroup$ You mean "circularity", not "paradox". These are distinct notions. $\endgroup$– Harry AltmanApr 24 '11 at 13:12

11$\begingroup$ @Gerald Edgar: Did you have any particular book in mind? If yes, why not reveal it? $\endgroup$– Sergey MelikhovApr 24 '11 at 14:34

3$\begingroup$ @Thierry, in set theory, everything is a set, so whether we're quantifying over sets, or over sets of sets, or sets of sets of sets, etc. these are all firstorder quantifications. $\endgroup$– Amit Kumar GuptaApr 24 '11 at 18:06
I have been asked this question several times in my logic or set theory classes. The conclusion that I have arrived at is that you need to assume that we know how to deal with finite strings over a finite alphabet. This is enough to code the countably many variables we usually use in first order logic (and finitely or countably many constant, relation, and function symbols).
So basically you have to assume that you can write down things. You have to start somewhere, and this is, I guess, a starting point that most mathematicians would be happy with. Do you fear any contradictions showing up when manipulating finite strings over a finite alphabet?
What mathematical logic does is analyzing the concept of proof using mathematical methods. So, we have some intuitive understanding of how to do maths, and then we develop mathematical logic and return and consider what we are actually doing when doing mathematics. This is the hermeneutic circle that we have to go through since we cannot build something from nothing.
We strongly believe that if there were any serious problems with the foundations of mathematics (more substantial than just assuming a too strong collection of axioms), the problems would show up in the logical analysis of mathematics described above.

3$\begingroup$ Finite set is OK, but there are also many infinite sets used freely in mathematical logic, how to transfer from finite set to infinite set safely without fearing any paradox? And, may I ask what is your exact opinion: 1)No paradox (why?), 2)There is paradoxes, but we have successfully excluded them (how?), 3)Not clear, but only hold a belief that there is or there is not any paradoxes? $\endgroup$– zzzhhhApr 24 '11 at 14:07

11$\begingroup$ Actually, I wouldn't say we are using any axioms of set theory. What we are using is some intuitive understanding of how to manipulate finite sequences of characters from a finite alphabet. If you want to formalise this, some fragment of number theory will be enough (as finite sequences can be coded as natural numbers). $\endgroup$ Apr 24 '11 at 21:18

13$\begingroup$ +1 Stefan: "what we are using is some intuitive understanding of how to manipulate finite sequences of characters from a finite alphabet." I find it helpful to consider a computer which is programmed to detect whether a formal proof in a formal theory is valid. The proof is expressed in finitely many symbols, and there is no background set theory sitting inside the computer on which the proofchecking depends. The pattern of flow of electrons through the logic gates is an extralinguistic entity, and this breaks the circularity. $\endgroup$– Todd Trimble ♦Apr 24 '11 at 23:40

3$\begingroup$ Stephan, your answer is GOLD. Yes, one must start somewhere, and what better place than finite strings and their manipulations? I, for one, do not believe in either sets or (platonic) numbers, but I have no problems with manipulating strings (my laptop does not have any issue either, and "it" does not know a thing of numbers and sets, unless by numbers ones means terms and their verifiable equivalence under the rules of arithmetics and term rewriting). The funny (and great) thing is: one can "play" ZFC without believing that anything there has any substance beyond syntactic games... $\endgroup$ Jun 14 '11 at 18:56

8$\begingroup$ @LeeMosher: One can write a huge novel about hobbits and orcs without believing in their existence in any deep sense. $\endgroup$ Sep 26 '12 at 14:20
The short answer is that there is no way to be absolutely certain that mathematics is free from contradiction.
To start with an extreme case, we all take for granted a certain amount of stability in our conscious experience. Take the equation $7\times 8 = 56$. I believe that I know what this means, and that if I choose to ponder it for a while, my mind will not somehow find a way to conclude firmly that $7\times 8 \ne 56$. This may sound silly, but it is not a totally trivial assumption, because I've had dreams in which I have found myself unable to count a small number of objects and come up with a consistent answer. Is there any way to rule out definitively the possibility that the world will somehow reach a consensus that $7\times 8 = 56$ and $7\times 8 \ne 56$ simultaneously? I would say no. We take some things for granted and there's no way to rule out the possibility that those assumptions are fundamentally flawed.
Suppose we grant that, and back off to a slightly less extreme case. Say we accept finitary mathematical reasoning without question. People might disagree about the precise definition of "finitary," but a commonly accepted standard is primitive recursive arithmetic (PRA). In PRA, we accept certain kinds of elementary reasoning about integers. (If you're suspicious about integers, then you can replace PRA with some kind of system for reasoning about symbols and strings, e.g., Quine's system of "protosyntax"; it comes to more or less the same thing.) Now we can rephrase your question as follows: can we prove, on the basis of PRA, that ZFC is consistent?
This, in essence, was Hilbert's program. If we could prove by finitary means that all that complicated reasoning about infinite sets would never lead to a contradiction, then we could use such infinitary reasoning "safely." Sounds like what you're asking for, doesn't it?
Unfortunately, Goedel's theorems showed that Hilbert's program cannot be carried out in its envisaged form. Even if we allow not just PRA, but all of ZFC, we still cannot prove that ZFC is consistent. Thus it's not just that we've all been too stupid so far to figure out how to show that ZFC doesn't lead to contradictions. There is an intrinsic obstacle here that is insurmountable.
So your scenario that someone may one day find a contradiction in ZFC cannot be ruled out, even if we take "ordinary mathematical reasoning" for granted. This is not as bad as it might seem, however. ZFC is not the only possible system on which mathematics can be based. There are many other systems of weaker logical strength. If a contradiction were found in ZFC, we would just scale back to some weaker system. For more discussion of this point, see this MO question.

$\begingroup$ I should restate my question as follows: "Will inconsistency in metatheory go into the theory built on it?" Here the metatheory is naive set theory and the theory built is mathematical logic. I should express my thanks to kakaz and other people who answers and comments in this thread. Only after interaction with them can I formulate my question in a clear form. Now I wonder if the answer is still unknown. It seems that treating infinite sets as a proper class as suggested by Stefan Geschke works. Is that method will possibly produce paradox too? $\endgroup$– zzzhhhApr 24 '11 at 20:47

4$\begingroup$ Your restated question is easy enough to answer: Yes, inconsistent metareasoning could produce an inconsistent formal theory. $\endgroup$ Apr 25 '11 at 14:14

1$\begingroup$ A fine point: "There are two main approaches for carrying out consistency proofs. One is to introduce a model of the system in question in the Metatheory. However, it seems to be implausible to assume that one can prove this way the consistency of a theory by using finitary methods, since such methods do not allow the use of sets. Hilbert realized this and suggested therefore that one should instead analyse proofs and show this way directly that it is not possible to derive in the formal system in question a contradiction."  From ehess.fr/revuemsh/pdf/N165R959.pdf $\endgroup$ Apr 25 '11 at 20:33

1$\begingroup$ "... Such theories will then be a substitute for Hilbert's finitary methods, we can call them extended finitary methods. The up to now most successful theories used for this purpose seem to be extensions of MartinLöf type theory, ..." (from the same paper) $\endgroup$ Apr 25 '11 at 20:49
That is to say, mathematical logic is using intuitive set theory. So, is there any paradox in mathematical logic?
Yes, in set theory whose logic is based upon naive set theory there is Berry's paradox.
Consider the expression:
"The smallest positive integer not definable in under eleven words".
Suppose it defines a positive integer $n$. Then $n$ has been defined by the ten words between the quotation marks. But by its definition, $n$ is not definable in under eleven words. This is a contradiction.
A version of Berry's paradox is called Richard's paradox. I don't see an essential difference between the two paradoxes (except that Richard's paradox was brought out by Poincaré, who was concerned with impredicative definitions and Berry's paradox by Russell, who was concerned with types). But the two Wikipedia articles offer very different explanations.
The explanation of Berry's paradox is essentially by type theory (even though it's not named); and the more specific explanation given by recursion theory also seems to fit in the framework of constructive type theory.
Richard's paradox is resolved in the framework of ZFC (and more importantly, of firstorder logic). Roughly, the resolution is that not all of what makes sense in set theory whose logic is based on naive set theory should make sense in ZFC; hence in some sense the paradox is only truly resolved in "the metatheory used to formalize ZFC". I don't know any textbook on such a metaZFC, which makes me feel uncomfortable about this resolution; but so did Poincaré and Russell, as I understand from their writings.
For this particular purpose I think a secondorder ZFC would work just as well as a "metaZFC". But then a higher version of the same paradox would only be truly explained by a thirdorder ZFC, etc. But then again I don't know any textbook on thirdorder ZFC. Luckily, there are quite a few textbooks on higherorder logic/type theory, and as I understand there are no problems of this kind (Richard/Berrytype paradoxes) in a modern type theory, because it serves as its own logic in essence.
On the other hand, a type theory is said to still require a metatheory. Does it mean that there must be deeper paradoxes that would not be resolved by type theory?
Added later. I'm a bit amused by this thread, which keeps growing with "orthodox" answers and with their lively discussion in the comments, whereas the "heretical" answer you're reading now has not been challenged (nor even downvoted) as yet.
Perhaps I should summarize my points so that it's easier to object if anybody cares.
1) The OP's question might be a bit informal or vague, but it does make sense as Berry and Richard paradoxes unambiguously demonstrate. One may hold different views of these paradoxes and their resolution, but one possible view (which I believe I picked from Poincare's writings) is that they are indeed caused by the factual mutual dependence between set theory and logic referred to in the OP. ("Set theory" and "logic" meant in colloquial sense here, not referring to a specific formalization.) You cannot just ignore these paradoxes, can you?
2) Type theories may have a lot of disadvantages compared to ZFC with first order logic (including the lack of a canonical formulation and of an equivalent of Bourbaki) but they do break the circularity between set theory and logic and thus do adequately resolve the paradoxes. ZFC is perfectly able to defend itself against these paradoxes but it does not attempt to explain them; for that it sends you to the metalevel, which then ends up with informal speculations about computers and one's experience with finite strings of symbols. (There are of course issues with such speculations, including: exactly which strings are finite, halting problems for idealized computers and finite memory of physical computers, not to mention potential finiteness of information in the physical universe and one's proofchecking software potentially involving higherorder logic already.) So in this case I see type theory as providing a mathematical solution, and ZFC, at best, a metaphysical one.
3) What I don't understand is whether there might exist a kind of type theory that would not need any metatheory (i.e. would serve as its own metatheory). Perhaps someone saying "You cannot get anything out of nothing" or "You cannot have any theory without metatheory" or "we must start somewhere" or "You have to start somewhere" could as well explain why it is impossible? If indeed it is impossible, can this impossibility be witnessed by a specific paradox to completely clarify matters?

$\begingroup$ Thank you. Do you mean the modern type theory is sure to include no paradox inherent in the naive set theory, such as Russell's or Richard's or any other paradox, discovered or undiscovered yet? $\endgroup$– zzzhhhApr 24 '11 at 15:42

1$\begingroup$ Modern type theory avoids Russel's and Richard's paradoxes by design, while one's belief that ZFC avoids e.g. Russeltype paradoxes is based largely on experience. As to paradoxes that are not as yet discovered you'd better ask Voevodsky; he has strong opinions on such matters mathoverflow.net/questions/40920. $\endgroup$ Apr 24 '11 at 16:03
There are a few problems you seem to be having. First of all, the statement "mathematical logic depends on ZFC" doesn't make sense.
As mathematical logicians, when we study formal systems, we should imagine placing that formal system in a box. The box is full of formulas and deductions in the object language. For example, ZFC is a firstorder theory with one binary predicate symbol and a bunch of axioms. It holds a privileged position since we tend to think of it as 'the' formal set theory, but there's no reason we couldn't instead use MK or NF or other set theories for the same purposes.
Mathematical logic is the act of studying formal systems using mathematical (not necessarily formal) methods, and ZFC is just one particular formal system. The important point is that mathematical logic is not a formal system, and although the statement "ZFC is consistent" is well formed, the statement "mathematical logic is consistent" is not. To claim a theory is inconsistent is to claim that there is a formal proof of false in some formal system. Russel's paradox, for example, can be cast as a formal proof of false in ZFC with unrestricted comprehension.
Without the context of firstorder logic, and the collections of variables and symbols that are required to write down formulas and formal proofs, the statement "_ is (in)consistent" is not meangingful. The blank must be filled in with a firstorder theory, or more generally, some formal system with a notion of formal proof. You can ask 'are we justified in forming and manipulating these collections?' But that's an informal question. As other users have pointed out, it has very good informal answers, for example, the fact that computers work gives us confidence that we shouldn't worry about doing arithmetic and manipulating strings informally.
In order to answer the question 'is the informal set theory we used to formulate first order logic consistent' either affirmitively or negatively, we must define the notion of consistency, and in doing so use the informal set theory in question. The point, again, is that consistency is only defined in the context of first order logic, where we take these collections as primitive and define consistency from there. In the same way we cannot speak of a simple group ouside the context of groups, we cannot speak about formal consistency outside the context of formal theories.
In short: One cannot provide a formal proof of anything without first defining formal proof! Hence, we must start somewhere and take the collections of symbols in first order logic as primitive, or convince ourselves informally that we are justified in forming such collections.

$\begingroup$ I'm not a logician, but I consider myself a "formalist" as for the foundation of mathematics and logic, and I don't agree on your sentence: «mathematical logic is not a formal system». When you form and manipulate such strings of symbols, you should not be allowed to use (formal or informal) reasoning involving e.g. infinite sets, induction etc. Once you place yourself in such a restriction, I think in principle you can do formal mathematical logic (i.e. "blind" manipulation of symbols) without problems. Do you agree? $\endgroup$– QfwfqSep 26 '12 at 16:42

$\begingroup$ The computable strings on a finite alphabetwhich include many infinite strings as well as well as all the finite stringsshould suffice to encode all the naive sets that you need for a full mathematical description of a set theory such as Zf. I do not think that any paradoxes will turn up if you use only these computable strings. $\endgroup$ Sep 26 '12 at 19:44
You cannot get anything out of nothing :) But do not worry.
Mathematics existed long before ZFC was formulated, and well before “formal reasoning” rose to a kind of religion. Mathematically, there is nothing more formal in a “formal reasoning” than in any other “logically justified” (i.e. commonly accepted) reasoning. The true reason of encoding math in a single theory is to gather all doubts in a single place, earn confidence that our new theory is consistent (as long as the foundations are consistent), and help communicating with other mathematicians.
Moving back to your question. Let me distinguish between four cases – according to your terminology  a theory can be:
 naïve and formal – this means that by using formal reasoning we may show that there is an inconsistency in the theory (for example: ZFC with unrestricted comprehension)
 naïve and informal – this means that we see that there is an inconsistency in reasoning within the theory, but a proof of this fact is outside our math (the same example)
 nonnaïve and formal – this means that we believe that the theory is consistent, and (sometimes) can “formally” prove its consistency relatively to another (formal or informal) commonly accepted theory
 nonnaïve and informal – just like above with the last part of the sentence skipped.
So, as you may see, being formal cannot make a theory consistent/inconsistent, but can provide additional arguments for/against the theory – simply – correctness is invariant under changes of formality. For most situations the picture of formality looks like follows:
 there is an informal concept like “firstorder logic”
 there is a formal theory of sets expressible in firstorder logic
If we would like to investigate foundations themselves than we could extend the picture by introducing one (or more) additional level:
 there is an informal theory of sets (metatheory; it has to be a bit stronger than the "inner" set theory to show that the "inner" set theory is consistent, but it may be far weaker to express the "inner" theory)
 there is a formal firstorder logic expressible in the metatheory
 there is a formal theory of sets expressible in firstorder logic

1$\begingroup$ The question is not formalization, but consistency(paradox), so let's temporarily forget ZFC and consider only the consistency problem. First we need the concept of set in mathematical logic, for example, the justification of proof by induction on structure of wffs relies on the concept of set. Second, we are using the concept of set in mathematical logic freely as we do in naive set theory. Third, there exists paradox in naive set theory in metauniverse, so by analogy I'm afraid there are also paradoxes in the naive set theory used in mathematical logic. This is why I post this thread. $\endgroup$– zzzhhhApr 24 '11 at 19:16

1$\begingroup$ To restate my question: Will inconsistency in metatheory go into the theory built on it? Here the metatheory is naive set theory and the theory built is mathematical logic. No formalization is involved in my question. $\endgroup$– zzzhhhApr 24 '11 at 20:23

1$\begingroup$ What does "go" mean? If you work in an inconsistent theory then any result of the theory is meaningless. If you define semantics of firstorder logic with respect to an inconsistent set theory, then you will get a metaproof saying that every set of sentences of the logic is consistent and a metaproof saying that every set of sentences is inconsistent. But these meaningless proofs will not make any theory consistent or inconsistent :) $\endgroup$ Apr 24 '11 at 20:52

1$\begingroup$ <<It now seems that every theory is inconsistent, that is, "there is no way to be absolutely certain that mathematics is free from contradiction." from Timothy Chow's answer.>> There is a giant difference between knowing nonsomething and not knowing something. $\endgroup$ Apr 24 '11 at 23:17

1$\begingroup$ So the parts of mathematics that follow an inconsistent theory may be meaningful just because they follow another (narrower) theory, not because they follow this inconsistent one. Put it another way – you may toss a coin to decide whether or not the Riemann hypothesis is true. With a great probability you will guess the right answer, but the answer will not be correct because of your toss, but for some other, far different reasons. $\endgroup$ Apr 24 '11 at 23:19
You cannot have any theory without metatheory. Opposite statement is not true and is simple kind of ideology in the fundamentals of mathematics. Of course You may use the same language for both of them! Then You would build mathematics in language which is its own metalanguage  just like natural language, but it is not very useful for strict analysis regarding paradoxes and circularities. But is is how mathematics works in everyday practice;)
Of course If You try to be strict and analise certain dilemma in fundamentals You have to build more or less strict metahteory for Your theory  here logic. So You have to separate theory and its metatheory. Assuming You agree with that, You question is: "is it possible that metalgic is inconsistent?" The answer is: Yes, it is!
Most of the logic may be performed in finite sets, but not all. The former part, which require infinite sets and quantifications over sets of symbols etc. requires to have its metatheory in order top be sure it may be consistent (and even for writing statements of a theory  mathematics is created for the people and by the people). So situation is as follows  You metatheory:
 it ma be related to naive set theory ( natural language) which obviously may be inconsistent. It does not mean that logics have to be inconsistent! It ma be, but there is not a must!
 Of course You may use ZFC as a metatheory! Then Your problem is transformed into question about consistency of ZFC. It may be also not related directly to logic!
Interesting question here is: may be theory consistent even if its metatheory is not? It seems that it may be one of the possible the cases...

$\begingroup$ To avoid divergence, please let me rephrase part of your idea as follows: Any theory must be built on metatheory. We should separate them. Here the metatheory is "naive set theory" and the theory built is "mathematical logic". If so, my question is: "Will inconsistency in metatheory go into the theory built on it?" I offered three answers to this question in my original post, the item 1 of your answer denies my second answer "if yes". Do you mean "if no" is also not certain, so there is not a must, as my third answer in my post indicates  the answer is unknown, maybe yes, maybe no? $\endgroup$– zzzhhhApr 24 '11 at 19:52

$\begingroup$ "Any theory must be built on metatheory."  are You sure? I am not. But is sometimes usable method. Theorymetatheorymetametatheory and so on hierarchy model resolves only certain problems. There are problems which in this type of reasoning are not resolved at all. For example claim beginning from the sentence: "for every level of theoremmetatheorem hierarchy .... " is not a part of any level of it, but still may be good, provable theorem... $\endgroup$– kakazApr 24 '11 at 22:16
The old (Hilbert) idea was to have a foundation of mathematics on elementary concepts that have a "itself evidence", and there was a intuitive "halphreal" (platonic?) idea about mathematics, it live in a pseudorealty, then cannot have antinomy (a thing cannot be a book and a nobook). Of course there was the hope of find a proof of consistency of mathematics (necessarily inside mathematics itself). After K.GOdel all these hopes crush down, mathematics is building on the set theory rock, but this rock isnt "absolute", or "itself evidence natural", but is juast a formal logical theory. Inside "set theory (in some form) you can make mathematical logic. Then before make the "Set theory" (ZFC for example) what is the mathematical foundation of the logic? ANd why logics use the concept of set (before make the Set thory)?
The paradox is evident, you cannot found mathematics from itself: 1) Is a phylosophical contadiction, for make a first step on bulding mathematics is absurd supposing that you just have a "mathematical ground"..
2) FOr GOdel theorem: cannot have a first foundation step that is its own foundation or for a faith on its natural itselfevidence (or proof of consistency in itself).
THen MAthematics could have a foundation only from something that is external. For "mathematics" we mean of course the article, the books, the ZF axioms , the various literature about mathematical fields, but is also what make all these thgis, this is the human think, cannot think to mathematics without remember that doingmathematics (thought) is what produce mathematics (in its formalism, articles ecc.).
Then the question become phylosophical (we have just see above that cannot have a logical formal resolution..): what is the sense of thinking mathematics? What is the sence of elementary concept used for buldind mathematics before its formal logical axiomatization?
When we think that "a element belong to a set" we mean a primitive concept that has its mean before a formalizated set theory and its axioms? (I think yes), Can we found mathematics on category theory ground, without have obligation about ZF when we say "this morphisms is a element of this set, or collection..."?
(excuse mine bad English)

1$\begingroup$ You don't need a theory of sets prior to a theory of categories, any more than you need a theory of sets prior to a theory of sets. $\endgroup$– Todd Trimble ♦Feb 17 '12 at 17:28
I think this problem shows itself at many stages of the human thinking. So we can form the expression "This expression is wrong" and immediately the liar paradox appears. So really this has nothing to do with mathematics proper, but with logic itself. And the solution is multistaged itself: at the basic level we can use Russell's (naive) type theory as a remedy. In fact when we talk about mathematics we already make sure we don't break certain rules on the metalanguage level. Next when we want to do set theory, we use the axioms of ZermeloFraenkel. Problem solved. Of course we can formalize the metalanguage and we can use again a ZF set theory in this task instead of type theory, but in doing so, we use an informal metametalanguage for which no way to ignore type theory. So, type theory is the ultimate building block of "human logic" and not just "mathematical logic".
I happen to realize the same apparent circularity in mathematical logic. If it purports to establish a foundation for mathematics, it seems to me its methods need to be different from mathematical methods. However, I have the uneasy feeling that one still is doing mathematics when studying mathematical logic. In spite of all this ambivalence, I think it presents a rather satisfying foundation for other branches of mathematics such as abstract algebra. It then seems to be a pretension to think that mathematical logic offers a foundation for "all" mathematics; maybe, philosophy can help with this matter.