The sets in mathematical logic

Question

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!

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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?

Answer 5

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

Answer 6

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

Answer 7

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

(excuse mine bad English)

Answer 8

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

Answer 9

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.