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?

  • $\begingroup$ A related question on MO: Second-order term in first-order logic? $\endgroup$
    – Kaveh
    Aug 22, 2012 at 23:22
  • 2
    $\begingroup$ A high-level explanation is that if you hope to acquire conceptual understanding by studying Wikipedia, then you will waste a lot of time. Wikipedia might be in some cases a useful reference source to look up details that you don't remember, but Wikipedia isn't carefully enough written to rely upon if you want to learn non-trivial mathematics. $\endgroup$ Nov 30, 2023 at 20:23

3 Answers 3


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

  • 2
    $\begingroup$ So, can you tell me why Wikipedia says that $\forall P\,\forall x (x \in P \lor x \notin P)$ is an SO formula? $\endgroup$ Feb 26, 2011 at 10:37
  • 3
    $\begingroup$ 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. $\endgroup$
    – boumol
    Feb 26, 2011 at 13:00
  • $\begingroup$ Perhaps this would like to you. $\endgroup$
    – leo
    Apr 16, 2013 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.

  • 2
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Feb 26, 2011 at 5:15
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Feb 27, 2011 at 10:20
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Feb 27, 2011 at 10:22
  • 3
    $\begingroup$ @NickKidman: In first order logic, all quantifiers ("for all" and "there exists") refer always to objects in the theory (elements in Group Theory, sets in Set Theory, etc). In higher order logic, the quantifiers may refer to collections of objects, or to collections of formulas about objects. So it is not enough to "look at the sentence", in so far as you need to know the context of the sentence. In the context of set theory, since the objects are sets, and the quantifiers refer only to sets, it is first order. (cont) $\endgroup$ Jul 12, 2012 at 23:18
  • 3
    $\begingroup$ @NickKidman: By contrast, consider the usual paraphrase of the Axiom of Replacement in Set Theory: "For all properties P and all sets A, $\{x\in A\mid P(x)\}$ is a set". This is not a First Order statement in the language of Set Theory, because we are quantifying over all formulas with a certain property ($P$). Instead, if you want your axiomatization to be First Order, we get a collection of Axioms of the form "$\forall A(\exists z (x\in A\land P(x)\to x\in z))$." and then say we get one axiom for each $P$. Then $P$ is not a variable, so it doesn't have to be quantified. $\endgroup$ Jul 12, 2012 at 23:20

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

  • 2
    $\begingroup$ +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!) $\endgroup$ Feb 27, 2011 at 12:00
  • 5
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Feb 27, 2011 at 12:13
  • $\begingroup$ Just to be sure I understand, in a many sorted first order theory, by creating sorts all you're doing is partitioning the domain of interpretation, wherein each domain object is assigned a unique sort. To continue your example, if you let the domain objects be nats and sets of nats, then that could form a natural partition into the two sorts. However, in a first order theory there's no way to enforce that the elements of the 2nd sort are only sets of nats, and in fact you can construct models in which that isn't the case. Is that about right? $\endgroup$
    – Motorhead
    Jan 5 at 17:36
  • $\begingroup$ yes, the main difference is that in second order arithmetic we restrict the semantic interpretation of the second order sort semantically, and interpret membership as identical to the mean membership. If you don't have those semantic restrictions on possible models, it would be no different from first order theory with 2 sorts. $\endgroup$
    – Kaveh
    Jan 7 at 1:46

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .