Zermelo–Fraenkel set theory is the most common foundation of mathematics with eight axioms and axiom of choice (ZFC):


But one can see that the statement of ZFC depends on first-order logic symbols and definitions, for example $=, \in, \forall, \exists$, predicate, formula, etc... And in many books, they didn't concept clearly about axioms of first-order logic, even through use set theory definition.

My question is how set theory and first-order logic can combine in a unique system of axioms as the foundation of Mathematics.

For example,

  1. There are objects called sets, denote by $X,Y,Z,..., A,B,C$

  2. There are symbols $=, \in, \forall, \exists$

  3. Symbols $=, \in$ can be put between two any sets $X,Y$ to be (primary) propositionals: $X\in Y$, $X=Y$.

  4. There are two logic values: $T$ (true), $F$ (false).

  5. Each propositional has a unique value, $T$ or $F$.

  6. There are logic operators $\neg, \vee, \wedge, \rightarrow, \leftrightarrow$

  7. Logic operators can combine propositionals to create new propositionals, their logic values follow the standard logic rules.

  8. For a set $A$ and a propositional $P$, then $\forall A, P,\ \exists A, P$ are propositionals.


There must have a system of axioms for propositionals and sets (include ZFC) and how can we make them be minimal?

  • 6
    $\begingroup$ ZFC is a theory in first-order logic. The fact that people are expected to be familiar with basics of first-order logic before studying a particular theory in first-order logic is reasonable. I am not sure what you are looking for. $\endgroup$
    – Kaveh
    Aug 22, 2012 at 6:40
  • 1
    $\begingroup$ We need first-order logic and set theory in a system of axioms. Every can be run by axioms. Many things are reasonable but they need to be proved. $\endgroup$ Aug 22, 2012 at 6:45
  • 2
    $\begingroup$ I don't follow your first comment. What do you mean by "proved"? These are axioms! $\endgroup$
    – Kaveh
    Aug 22, 2012 at 6:50
  • 2
    $\begingroup$ pps: as William implies in his answer below, we already assume a considerable amount of mathematics (in "meta-theory") before talking about these. There are people who may disagree with assuming these but this is the practice in mathematics. If you don't accept them then there is nothing to talk about. This may confuse people who think logic is on itself and doesn't need any assumptions but that is not the case. We at least needs ability to do simple manipulation of syntactic symbols and this already contains a considerable amount of arithmetic. $\endgroup$
    – Kaveh
    Aug 22, 2012 at 7:06
  • 2
    $\begingroup$ Unlike a construction of a skyscraper, in mathematics one does not begin with the foundations. One begins with the ground floor, builds a good part of the lower half of the building, then one begins to dig and build the foundations. $\endgroup$
    – Asaf Karagila
    Aug 22, 2012 at 9:55

2 Answers 2


The usual approach is to define a concept of a first order language $\mathcal{L}$. They are usually specified by the nonlogical symbols. Well-formed formulas in the language $\mathfrak{L}$ are strings of symbols of $\mathfrak{L}$ along with the logical symbols such as $($, $)$, $\wedge$, $\neg$, variables etc. You can look up in a logic textbook the inductive definition of well-formed formulas, but something like $x \wedge y$ is a well-formed formula, but $(()\neg\wedge xy \neg$ is not a well-formed formula.

A first order theory $T$ in the language $\mathfrak{L}$ is then a collection of well-formed sentences (no free variable) in the language $\mathfrak{L}$. You would then define the deduce relation $T \vdash \varphi$ to mean that there exists a proof of $\varphi$ using $T$. A proof is just a string of of sentences $\phi_1, ..., \phi_n$ such that $\phi_n = \varphi$, each $\phi_i$ is in $T$, a logical axiom of first order logic, follows from modus ponen or generalization using previous $\phi_j$, where $j < i$.

So the above is the definition of a arbitrary first order theory in an arbitrary first order language $\mathfrak{L}$. Now let $\mathfrak{L} = \{\in\}$ a first order language consisting a single binary relation. $ZFC$ is then the first order theory in the language $\mathfrak{L}$ consisting of the "eight axioms" you mentioned above. (Note that ZFC has infinitely may axioms. For example, the axiom schema of specification is actually one axiom for each formula.)

The benefit of this approach where the general definition of first order logic is developed first is that you apply this to study first order logic in general and other first order theories such that the theory of groups, rings, vector space, random graphs, etc. Also first order logic is developed in the metatheory. That is for example, a theorem of ZFC (even if it is about infinite cardinals greater than $\aleph_1$) has a finite proof in the metatheory. However, within ZFC you can formalize first order logic. Then you can consider question about whether $ZFC$ can prove it own consistency.

By taking the approach of developing first order theories in general, you also gain a certain perspective. Some people think that ZFC is something special since it can serve as a foundation for much of mathematics. Through this approach, $ZFC$ is really just another first order theory in a very simple language consisting of a single non-logical symbol. People often have a hard time grasping the idea that $ZFC$ can have different models, for instance one where the continuum hypothesis holds and one where it does not. However, almost everyone would agree that that there exists more than one model of group theory (i.e. more than one group). Sometimes it is helpful to know that results about arbitrary first order theory still apply when one is working in ZFC set theory.

  • $\begingroup$ Thank Willian for your clearly answer. But for example, when you write $L=\{\in\}$ you regard $L$ as a singleton set, but the existence of such kind of set is proved by Axiom of Pairs in ZFC. Are there any pure statements and don't depend on set theory axioms? $\endgroup$ Aug 22, 2012 at 7:26
  • 1
    $\begingroup$ @MinhNguyen When I wrote that, I had not develop ZFC yet. It is in the metatheory. I am not saying "$L$ is a set". For that statement to even make sense, I need to define what a $"set"$ is and one way of doing this could route of using $ZFC$ set theory. Here I am just saying formulas of $ZFC$ are made with logical symbols and that one single binary relation $\in$. $\endgroup$
    – William
    Aug 22, 2012 at 7:37
  • $\begingroup$ @MinhNguyen To understand that we are working in the Metatheory, just ask yourself do you need $L = \{\in\}$ to be a set (whatever that is). Similarly, without the axiom of infinity, you can not prove $\mathbb{N}$ is a set. However, in the metatheory, why do I need $\mathbb{N}$, itself? All proofs are finite. The Metatheory is like your textbook. You may be reading a textbook about set theory proving all sorts things about infinite set, but your textbook only has finitely many pages. I hope these example show that you don't need "sets" to do logic. In reality, I don't even know what a set is. $\endgroup$
    – William
    Aug 22, 2012 at 7:49
  • $\begingroup$ I think when writing $L=\{\in\}$, you forgot identity somewhere ... $\endgroup$ Sep 2, 2012 at 11:43
  • $\begingroup$ @HagenvonEitzen Most of the time, all first order theory are assumed to have the logical symbols $=$, parenthesis, $\wedge$, etc. Hence, you can specify the the particular language you are working in by writing just the nonlogical symbols. $\endgroup$
    – William
    Sep 2, 2012 at 15:45

Note that before talking about theories and provability we need to first select a language to express formulas/statements. Here the language is the language of first-order logic.

A language is just a set of symbols and how we can combine those symbols to create meaningful expressions (well-founded formulas).

After selecting a language we can start talking about proof systems (mathematical reasoning systems). A proof system is an (efficient) algorithmic way of checking if a given string is a proof of a given formula (encodes as a string). Think of it as an algorithm that getes two inputs $P(\pi,\varphi)$ (a binary computable predicate) which is true if and only if string $\pi$ is a proof of formula $\varphi$ in $P$. People sometimes write $\pi : P \vdash \varphi$ or omit $\pi$ and write $P \vdash \varphi$. Often the $P$ is put below the symbol like $\vdash_P \varphi$, and when it is clear from the context it is omitted completely $\vdash \varphi$.

What is $P$? We would like that $P$ captures our intuitive notion, i.e. we would like it to satisfy the following conditions:

  • soundness: $P$ accepts $\pi$ and $\varphi$, then $\varphi$ is true.

  • completeness: if $\varphi$ is true, then $P$ accepts $\pi$ and $\varphi$.

The conditions above presume a notion of semantic truth and are what ties a syntactic objects like proofs to the semantic notion of truth. For validity in first-order logic we can satisfy these conditions, i.e. first-order logic has a sound and complete proof system. However this is not the case for stronger systems like PA or ZF where by incompleteness theorem there is no way of algorithmicly enumerating the true statements (in dependent of the way you define the truth as long as we agree that some basic statements are true, e.g. Robinson's arithmetic theory $Q$).

It is usual in mathematics to take $P$ to be proofs in first-order logic + some first-order theory. ZF is one of such theories. William explains some reasons for this in his answer. A key point here is that first-order logic is very simple and intuitive. It is simpler than the amount of mathematics that one needs to do the stuff I explained above. It is seldom disputed (at least not classical mathematics). By separating the first-order logic part from the first-order theory part we can focus on the disputed part of reasoning. There are mathematicians who would not accept ZF and but you will have a difficulty finding anyone who doesn't accept first-order logic.

If you remove the axioms for first-order logic, then you cannot prove even simple things because the axioms for first-order logic are the part that give us the meaning of the symbols. For example, we have axioms $P \land Q$ implies $P$, $P \land Q$ implies $Q$, and $P$ and $Q$ imply $P \land Q$. If you don't have these axiom, then meaning of the symbol $\land$ can be arbitrary. There is nothing forcing it to act as "and" other than these axioms. Same applies to other axioms of first-order logic. I would suggest that you have a look at a proof system for first-order logic to understand (e.g. LK) to understand that the meaning and use of the symbols is a result of these axioms and without them the symbol is meaningless.

Let me add something that confuses people who are new to mathematical logic. Logic is not build on nothing! We are already assuming a considerable amount of arithmetic in manipulating symbols. For example, if $f$ is a function symbol and $x$ is a variable, we assume that we can create $f(x)$, $f(f(x))$, etc. and this can be views as similar to the successor function over natural numbers. The minimum amount that is needed not too much, but it at least will contain a form of induction over natural numbers. The usual theory that people assume for this meta theory when talking about strong theories is PRA (but there are weaker theories that are sufficient, the bounded arithmetic theory VTC is the weakest meta-theory that I know which allows relatively easy development, see "Logical Foundations of Proof Complexity" for more detail.) Also see Petr Hajek and Pavel Pudlak's book "Metamathematics of First-Order Arithmetic".

  • $\begingroup$ Yes, I agree with you. But could you only concept a language $\mathcal{L}$ for set theory? and before use ZFC, your statements should be pure. $\endgroup$ Aug 22, 2012 at 7:36
  • $\begingroup$ for example, no function, no pair or singleton set, since the existence is implied from ZFC. $\endgroup$ Aug 22, 2012 at 7:38
  • 1
    $\begingroup$ @Minh, take a look at the page for PRA that I linked in the answer. Hopefully you would consider it to be pure enough. :) ps: No, one can do those stuff without assuming set theory, for simple objects like finite strings we don't need to assume the axioms of set theory. Note that computers already do these kind of stuff (given enough time and memory). What makes set theory set theory is infinite sets. For finite sets (containing finite objects) we can do a lot without any axiom about existence of infinite sets. Also note that without the axioms of infinity, ZF is equivalent to PA. $\endgroup$
    – Kaveh
    Aug 22, 2012 at 7:40
  • $\begingroup$ Are you sure PA is equivalent to ZF? where you can refer to? $\endgroup$ Aug 22, 2012 at 7:46
  • $\begingroup$ @Minh, Yes, I am sure that ZF-Inf (+TC) is equivalent to PA. E.g. see Ali Enayat's answer. $\endgroup$
    – Kaveh
    Aug 22, 2012 at 7:51

You must log in to answer this question.

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