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!

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. 


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. 


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. 


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? 


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:
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:
If we would like to investigate foundations themselves than we could extend the picture by introducing one (or more) additional level:



This is an answer to another question that unfortunately has been closed just before I could post it and that essentially revolves around the same, or very similar, points as the question of the above OP. Even if, from the point of view of a logician (which I'm not), the question is elementary, I think it's worth trying to give an answer, so to clarify things (also to myself) and settle some doubts that many nonlogicians like me often have about the foundations model theory and logic. Forget for a moment about $ZFC$. When investigating any (let's say first order) formal theory (such as Peano Arithmetic $PA$, or Algebraically Closed Fields $ACF$) logicians tacitly assume to work within the framework of a metatheory $T$, which must be some kind of "set theory" (where the term is intended loosely, possibly including certain systems of second order arithmetic like $ACA_0$ or of category theory like $ETCS$ or of class theory like $NBG$, according to personal taste) otherwise they wouldn't be able to talk (in principle with rigour, i.e. formally) of all the classical syntactic concepts, such as: languages, signatures, sets of formulas, finite strings of symbols and concatenation thereof; but also of all the classical semantic concepts, like structures, interpretations, models, isomorphisms. Or at least they wouldn't be able to codify in principle all the above concepts in the metatheory. The metatheory $T$ is hence momentarily assumed to embody "ontological" concepts, i.e. to formalize the concept of the "real universe of sets" (as opposed to specific concepts of sets arising from theories that are under scrutiny within $T$). As far as I understand, logicians (even if they usually don't like to explicitely spell out the metatheory they're tacitly using) are perfectly content in assuming the metatheory is the standard set theory $ZFC$ (after all, Logic is a part of Mathematics like any other). Anyway, I presume much less is needed to "formalize Logic"; for example I think $ZF$ would be enough, or weaker theories such as $ACA_0$ would be ok, and I think (but some professional logician should say if my guess is correct) essentially nothing would be changed in Logic in switching from one suitable metatheory to another: that's why they usually don't bother themselves specifying the metatheory. How does this formalization work, roughly? Let's consider for example the first order formal theory of groups (call it $GT$). It must be dealt with inside a metatheory (which is a "set theory") which we call $T$. So here we have sentences of $T$ talking about the "objects" $T$ is apt talking about (it could be sets, or sets of natural numbers...), and we have some way to codify the syntactic and the semantic concepts of Logic within $T$: for example some sentences of $T$ will talk about some particular sets that we (informally) interpret as being strings of symbols of $GT$, others as being elements of the language of $GT$, and so on. Of course there will also be sentences of $T$ talking about sets that are structures for the signature of $GT$ (that is, magmas equipped with an arbitrary element $1$ that need not be a unit, and maybe with an arbitrary unary function $x\mapsto (x)^{1}$ which need not be the inverse), and sets that are models of $GT$ (that is, plain groups). Now let's come back to $ZFC$. As in the case of $GT$, we must deal with the first order formal theory $ZFC$ within a metatheory ("set theory") $T$. Your question is: what about if $T$ is Zermelo Frenkel set theory with Choice? For the syntactic aspect, nothing special happens. You have sentences of $T$ talking about sets that we take to codify various syntactic notions of $ZFC$. Example: a certain sentence of $T$ will define a unique "set" (in the sense of "object of which $T$ is apt talking about"  in this case it means "set in the sense of Zermelo Frenkel set theory with Choice") which stands for the following finite concatenation of symbols in the language of $ZFC$: $$\forall\forall\in\in\in\to\in x \in ((y(())\in\in = = \in, $$ others will be more meaningful, e.g. displaying an axiom, a theorem (or a conjecture) of $ZFC$. For the semantic aspect, indeed, there are some subtleties. In the case of $GT$ we consider models which are sets of $T$ equipped with some structure: $(G,\mu,\iota,1)$. Note that, in the language of $GT$, variables stand for (i.e. are interpreted as) elements of a group, and (the support of) a model is the set of all such elements. If we were asked to prove the existence of models of $GT$, we would have no problem: we would simply exhibit any group, for example $(\mathbb{Z}/ 2 \mathbb{Z},+,,0)$ (or even the trivial group, for what it matters!). In the case of $ZFC$, what would be a model? A model $(X,E)$, properly, would be a set $X$ of $T$ equipped with a relation $E \subseteq X \times X$ satisfying the axioms of $ZFC$ when we interpret (via $T$) the relation symbol "$\in$" of $ZFC$ as meaning $E$. Note that variables, in the language of $ZFC$, stand for sets, and the support $X$ of the model must be interpreted as the collection of all such elements, that is $X$ has to be interpreted as the class of all sets. So far, nothing problematic: set theorists consider models (in the framework of Zermelo Frankel set theory with Choice) of $ZFC$ all the time. For example, if $\xi$ is an inaccessible cardinal, then $(V_{\xi},\in)$ will be a model of $ZFC$ (where $V_{\xi}$ is the slice of the cumulative hierarchy defined by $\xi$). What about proving the existence of models of $ZFC$? This is the subtlety: when we take $T$ to be Zermelo Frenkel set theory with Choice, we cannot prove in $T$ that $ZFC$ has models, because otherwise we would contradict Goedel's second incompleteness theorem! For example, we don't know, on the grounds of $T$ alone, whether there exists an inaccessible cardinal. So, seen from the point of view of the metatheory $T$, the whole "ontologic" problem of existence of models of $ZFC$ is somehow "suspended". In order to be granted the existence of those models, we have to assume stronger axioms than the ones of $T$; for example, some large cardinal axioms. The existence of an inaccessible would be sufficient for having the mere existence of a model $(X,E)$ (in which, in this case, $E$ is the restriction of the "ambient" membership relation $\in$ itself) without further requirements. There's another subtlety. In $T$, via some Russel like paradox, one can easily prove that there is no set $V$ such that every set belongs to $V$. This implies that, if for some reason we are handled a model $(X,E)$ of $ZFC$, then either the relation $E$ is not the restriction to $X$ of the "ambient" membership relation $\in$ of $T$ (those are the so called nonstandard models of set theory), or there are properties of some set $S$ defined in $ZFC$ that are not true "ontologically" about its interpretation in the model (i.e. the corresponding sentences of $T$ are false when applied to the interpretation $S^{\mathrm{int}}$ of $S$ in $(X,E)$). For example, if $(X,\in)$ is a countable (standard) model, then of course the notion of cardinality cannot be transferred literally from $ZFC$ to $(X,E)$, because $ZFC$ proves there are uncountable sets, yet the interpretation of any set in $(X,\in)$ will be "ontologically" countable just because $X$ is. To be more concrete, define $\mathbb{R}$ in $ZFC$ in one of the usual ways, then of course $ZFC$ proves « $\mathbb{R}$ is uncountable». In a countable standard model $(X,\in)$ there is a countable set $\mathbb{R}^{\mathrm{int}}$ which is the interpretation of $\mathbb{R}$. Being $X$ a model, the sentence «$\mathbb{R}^{\mathrm{int}}$ is $($ uncountable $)^{\mathrm{int}}$ » of $T$ is true, where «$($ uncountable $)^{\mathrm{int}}$» is the interpretation of the notion of uncountability in the model, but this is the appearent paradox, which is called Skolem paradox the sentence of $T$ «$\mathbb{R}^{\mathrm{int}}$ is uncountable» is false. The appearent confusion comes from mixing up the notion of uncountability in the theory and in the metatheory. 


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:
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... 


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. 


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) 


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". 

