Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Wikipedia describes the first-order vs. second-order logic as follows:

First-order logic uses only variables that range over individuals (elements of the domain of discourse); second-order logic has these variables as well as additional variables that range over sets of individuals.

It gives $\forall P\,\forall x (x \in P \lor x \notin P)$ as an SO-logic formula, which makes perfect sense to me.

However, in a post at CSTheory, the poster claimed that $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$ is an FO formula. I think this must not be the case, since in the above formula, $x$ and $y$ are sets of individuals, while $z$ is an individual (and therefore this must be an SO formula).

I mentioned this as a comment, but two users commented that ZF can be entirely described by FO logic, and therefore $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$ is an FO formula.

I'm confused. Could someone explain this please?

share|improve this question
A related question on MO: Second-order term in first-order logic? –  Kaveh Aug 22 '12 at 23:22

3 Answers 3

up vote 26 down vote accepted

It seems to me that you're confusing the first order formulas with their intended interpretations.

The language of set theory consists of just a single 2 place predicate symbol, usually denoted $\in$. The statement you quote is a first order statement - it means just what is says: "for all $x$ and for all $y$, ($x = y$ iff for all $z$, ($z \in x$ iff $z \in y$))", but it does not tell you what $x$ is. When you say "but $x$ is a set and $z$ is an individual, so this statement looks second order!", you're adding an interpretation to the picture which is not specified by the first order formula alone - namely that "for all x" means "for all sets x" and "$\in$" means "the usual $\in$ in set theory".

In first order logic, this "adding of interpretation" is usually called "exhibiting a model".

Here's another way of looking at this same first order statement. Suppose I reinterpret things - I say "for all $x$" means "for all real numbers $x$" and $\in$ means $<$. Then, $\forall x \forall y$ ($x=y$ iff $\forall z$, ($z \in x$ iff $z \in y$)) is a true statement: it says two real numbers are equal iff they have the same collection of smaller things. Notice that in this model, nothing looks second order.

By contrast, in second order logic, you are directly referring to subsets, so that in any model (that is, interpretation), $\forall S$ means "for all subsets of whatever set the variable $x$ ranges over".

share|improve this answer
So, can you tell me why Wikipedia says that $\forall P\,\forall x (x \in P \lor x \notin P)$ is an SO formula? –  Sadeq Dousti Feb 26 '11 at 10:37
Let us consider some domain interpretation for your formula (for example, sets, human beings, ...). Then, the first-order variables (like x,y,z, etc.) must be interpreted as members of your domain (for example, x is a set, x is a human being, etc), while the second-order variables (like P, Q, etc) must be interpreted as subsets of your domain (for example, P is a family of sets, P is a family of human beings, etc). This is the difference. –  boumol Feb 26 '11 at 13:00
Perhaps this would like to you. –  leo Apr 16 '13 at 8:03

The statement is indeed a first order statement in standard Set Theory. But it is no wonder you are a bit confused.

Most people think of sets and elements as different things. However, in standard set theory this is not the case.

In standard set theory, everything is a set (there are no "ur-elements", elements that are not sets). The objects of set theory are sets themselves. The primitive relation $\in$ is a relation between sets, not between ur-elements and sets. So, for example, the Axiom of the Power Set in ZFC states that $$\forall x\exists y(\forall z(z\in y \leftrightarrow z\subseteq x))$$ which is a first order statement, because all the things being quantified over are objects in the theory (namely, "sets").

So you need to forget the notion that "elements" are things in sets and sets are things that contain elements. In ZF, everything is a set.

It's a little hard to see the distinction between first and second order statements in ZF precisely because "sets" are the objects, and moreover, given any set, there is a set that contains all the subsets (the power set). In a way, the Axioms are set up precisely to allow you to talk about collections of sets without having to go to second order logic.

In ZF, to get to second order you need to start talking about "proper classes" or "properties". For instance, that's why Comprehension is not a single axiom, but an entire infinite family of axioms. Comprehension essentially says that for every property $P$ and every object $x$ of the theory (i.e., every set $x$), $\{y\mid y\in x\wedge P(y)\}$ is a set. But trying to quantify over all propositions would be a second order statement. Instead, you have an "Axiom Schema" which says that for each property $P$, you have an axiom that says $$\forall x\exists y\Bigl(z\in y\leftrightarrow\bigl(z\in x\wedge P(z)\bigr)\Bigr).$$ If you try quantifying over "all $P$", then you get a second order statement in ZF.

share|improve this answer
I think that the last paragraph is not correct, for example in set theory MK, we have two sorts, one for classes and one for proper sets, but the language is still first order. –  Kaveh Feb 26 '11 at 5:15
@Kaveh: Well, it's poorly phrased. I meant to put it entirely in the context of ZF, but did not do so correctly. Thanks –  Arturo Magidin Feb 26 '11 at 19:29
I don't know any second order set theory and the concept seems a little bit strange for me. Higher order theories are higher order because they restrict the possible interpretation of some sorts, e.g. the sort of subsets of the first sort needs to be really the subsets of the first sort, i.e. they enforce (semantically not syntacticly by axioms) some amount of set theory on the higher sorts in the interpretations, this makes sense for example for higher order arithmetics, but (although possible) it seems strange for a set theory to have some set theoretic restrictions on interpretations. –  Kaveh Feb 27 '11 at 10:20
ps: In MK you can quantify over all properties (even those not expressible as first order formulas) by quantifying over the second sort which is classes=properties, and it is still first order. As I said in the the comment above a second or higher order logic enforces some semantical restriction on the possible interpretations of the higher sorts. –  Kaveh Feb 27 '11 at 10:22
I'm sorry but I don't know or see how the question is really answered: Is there a way to read off of any given statement if it's first-order logic just by looking at the symbols, or does one have to say "Oh, and P is supposed to be a property here, and x is not." Because at first I though by looking at $\forall P\,\forall x (x \in P \lor x \notin P)$ that the sequence "$x \in P$" and the fact that never "$P\in ...$" would tell you that, but you wouldn't know from a single sentence that therefore $P$ has to be the second sort. –  NikolajK Jul 12 '12 at 21:54

Replace the non-logical relational symbol ∈ with R and the confusion goes away. Your problem arises from the fact that the symbol ∈ makes you confuse the neutral symbol of the language of set theory (which has no properties other than those expressed by axioms of the theory) with the intended interpretation of the symbol about real sets. The set theories like ZF have very strange models which has nothing to do with the intended model and interpretation of the relation $R$ has nothing to do with the real membership relation between sets.

A first-order theory can have many sorts and the intended meaning of some of those sorts can be higher type objects, e.g. we can have a two sorted theory where the intended meaning of the objects of the first sort are natural numbers and the intended meaning of the objects of the second sort are sets of natural numbers. We can quantify over them and the theory is still first order, though it has two sorts. The models of this theory needs to have two sets, one for interpreting the objects of the first sort and the other for interpreting the objects of the second sort, but there does not need to be any relation between these two sets that are used for interpreting objects even if the intended interpretation for the second sort of sets of objects from the first sort. The only properties of that these two sets need to satisfy are those expressed by axioms of the theory. You can add axioms of a set theory like ZFC for the second sort and consider objects of the first sort as urelements of the set theory that satisfying some other axioms e.g. first order Peano Arithmetic. This is still a first order theory. And the theory will have models where the interpretations of the two sort are not related in the intended way, i.e. the objects of the second sort will not be the sets of objects of the first sort, and there are no way to enforce this syntactically, i.e. using axioms.

A second- or higher-order theory enforces some restriction on possible interpretations of some sort which are called the higher sort. These restrictions are not syntactical, i.e. they are not axioms of theory, but semantical, i.e. we restrict the models of the theory to those that satisfy some certain conditions, e.g. the members of the set interpreting the second sort in the two sorted number theory I mentioned above are really the sets of objects of the first sort. This is like assuming some amount of set theory semantically. Without these semantical restrictions about interpretation the theory is still first order.

The higher-order theories are interesting for studying things like natural numbers. The (complete/full) second-order Peano arithmetic will force the set interpreting the second sort to be exactly the powerset of the first sort. Note that this theory is not axiomatizable, i.e. there are no set of first order axioms that will capture exactly these models. (In fact even weaker version of this second-order set theory which do not require the existence of all subsets of the first sort are not axiomatizable.)

On the other hand, I don't know any higher order set theory, and in fact the concept itself seems a little bit unnatural (of course it can be due to my lack of knowledge).

share|improve this answer
+1. Thanks! I just read parts of this topic on SEP, and your answer confirmed my understanding. Do you suggest a book to read further on? (SEP suggests several books, but I cannot afford reading all of them!) –  Sadeq Dousti Feb 27 '11 at 12:00
I always find SEP articles nice. The answer depends on what you want to learn, do you want to learn about higher order arithmetics or philosophy of higher order logics or descriptive complexity or ...? Enderton 2001 (textbook) and Shapiro 1991 (philosophy) are nice general readings. Simpson 1999 is the bible for second order arithmetic and its subsystems, might be too heavy if you are not going to do research in that area (but might want to read the intro part). I haven't read Väänänen 2001 but it should be a good, also Boolos 1975. Other references seems to be either old or technical papers. –  Kaveh Feb 27 '11 at 12:13
Thanks a lot! –  Sadeq Dousti Feb 27 '11 at 22:12
@Kaveh: +1 for your excellent answer! –  user17090 Sep 29 '12 at 11:12

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.