# The sets in mathematical logic

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., first-order 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!

-
If yes, what we should do? Read the introductory material in a basic textbook on mathematical logic? –  Gerald Edgar Apr 24 '11 at 12:09
I have read serveral basic textbook on mathematical logic, but none of them answers my question successfully. –  zzzhhh Apr 24 '11 at 12:36
You mean "circularity", not "paradox". These are distinct notions. –  Harry Altman Apr 24 '11 at 13:12
@Gerald Edgar: Did you have any particular book in mind? If yes, why not reveal it? –  Sergey Melikhov Apr 24 '11 at 14:34
@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 first-order quantifications. –  Amit Kumar Gupta Apr 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.

-
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? –  zzzhhh Apr 24 '11 at 14:07
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). –  Stefan Geschke Apr 24 '11 at 21:18
+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 proof-checking depends. The pattern of flow of electrons through the logic gates is an extra-linguistic entity, and this breaks the circularity. –  Todd Trimble Apr 24 '11 at 23:40
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... –  Mirco Mannucci Jun 14 '11 at 18:56
@LeeMosher: One can write a huge novel about hobbits and orcs without believing in their existence in any deep sense. –  Michael Greinecker 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.

-
I should restate my question as follows: "Will inconsistency in meta-theory go into the theory built on it?" Here the meta-theory 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? –  zzzhhh Apr 24 '11 at 20:47
Your restated question is easy enough to answer: Yes, inconsistent meta-reasoning could produce an inconsistent formal theory. –  Timothy Chow Apr 25 '11 at 14:14
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 Meta-theory. 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/revue-msh/pdf/N165R959.pdf –  Sergey Melikhov Apr 25 '11 at 20:33
"... 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 Martin-Löf type theory, ..." (from the same paper) –  Sergey Melikhov Apr 25 '11 at 20:49

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 first-order 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 first-order 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 first-order 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.

-
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? –  Qfwfq Sep 26 '12 at 16:42
The computable strings on a finite alphabet-which include many infinite strings as well as well as all the finite strings-should 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. –  Garabed Gulbenkian Sep 26 '12 at 19:44

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 first-order 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 meta-ZFC, 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 second-order ZFC would work just as well as a "meta-ZFC". But then a higher version of the same paradox would only be truly explained by a third-order ZFC, etc. But then again I don't know any textbook on third-order ZFC. Luckily, there are quite a few textbooks on higher-order logic/type theory, and as I understand there are no problems of this kind (Richard/Berry-type 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 meta-theory. 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 meta-level, 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 proof-checking software potentially involving higher-order 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?

-
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? –  zzzhhh Apr 24 '11 at 15:42
Modern type theory avoids Russel's and Richard's paradoxes by design, while one's belief that ZFC avoids e.g. Russel-type 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. –  Sergey Melikhov Apr 24 '11 at 16:03

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)
• non-naï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
• non-naï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 “first-order logic”
• there is a formal theory of sets expressible in first-order 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 (meta-theory; 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 first-order logic expressible in the meta-theory
• there is a formal theory of sets expressible in first-order logic
-
I'm a bit confused. Please let me rephrase some notions as following: The intuitive set theory containing Russell's paradox is naive and informal, the current mathematical logic is naive but formal, right? So my question is, for any theory that involves naive notion of sets like current mathematical logic, is there always any paradox as we encountered in the naive set theory (like Russell's paradox)? –  zzzhhh Apr 24 '11 at 15:14
"The intuitive set theory containing Russell's paradox is naive and informal, the current mathematical logic is naive but formal, right?" I do not understand your term "intuitive". Formerly, you used it as a synonym for "naive". If this is correct, then "yes" - "intuitive set theory" is a "naive set theory", and as I said it may be formal or informal. "So my question is, for any theory that involves naive notion of sets like current mathematical logic" Mathematical logic does not involve "naive notion of sets". –  Michal R. Przybylek Apr 24 '11 at 15:57
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 meta-universe, 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. –  zzzhhh Apr 24 '11 at 19:16
To restate my question: Will inconsistency in meta-theory go into the theory built on it? Here the meta-theory is naive set theory and the theory built is mathematical logic. No formalization is involved in my question. –  zzzhhh Apr 24 '11 at 20:23
<<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 non-something and not knowing something. –  Michal R. Przybylek Apr 24 '11 at 23:17

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 non-logicians 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:

1. 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!
2. 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...

-
To avoid divergence, please let me rephrase part of your idea as follows: Any theory must be built on meta-theory. We should separate them. Here the meta-theory is "naive set theory" and the theory built is "mathematical logic". If so, my question is: "Will inconsistency in meta-theory 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? –  zzzhhh Apr 24 '11 at 19:52
"Any theory must be built on meta-theory." - are You sure? I am not. But is sometimes usable method. Theory-metatheory-metametatheory 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 theorem-metatheorem hierarchy .... " is not a part of any level of it, but still may be good, provable theorem... –  kakaz Apr 24 '11 at 22:16

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 "halph-real" (platonic?) idea about mathematics, it live in a pseudo-realty, then cannot have antinomy (a thing cannot be a book and a no-book). 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 itself-evidence (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 doing-mathematics (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..."?

-
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. –  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 Zermelo-Fraenkel. 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 meta-meta-language for which no way to ignore type theory. So, type theory is the ultimate building block of "human logic" and not just "mathematical logic".

-