I've been self-studying ZFC set theory by following the book "The Joy of Sets". I've also learned that ZFC axioms are expressed in the language of first order logic, but I have ever been trained in logic and philosophy. Since the book I've been following does not contain any introduction to logic, I was trying to grasp some basic knowledge of logic from this wikipedia page and some links found from google.

So far, I've learned that first order logic is built upon zeroth order logic, which has three axiom schemes:

  1. $P\rightarrow(Q\rightarrow P)$,
  2. $(P\rightarrow(Q\rightarrow R))\rightarrow(P\rightarrow Q)\rightarrow(P\rightarrow R)$,
  3. $(\neg P\rightarrow\neg Q)\rightarrow(Q\rightarrow P)$.

where $P$, $Q$, and $R$ are well-formed formulas in the language $\mathscr{L}$. The above axioms are obvious to me. I can see that they are ubiquitous in everyday mathematics.

The first order logic has, in addition, the following extra axiom schemes:

  1. If $x$ does not occur free in $P$, then ($\forall x$)$P\rightarrow P$,
  2. If $P(x)$ is a well-formed formula and $t$ is free for $x$ in $P(x)$, then $(\forall x)P(x)\rightarrow P(t)$,
  3. If $P$ contains no free occurrence of $x$, then $(\forall x)(P\rightarrow Q)\rightarrow(P\rightarrow(\forall x)Q)$.

In addition, in mathematics, one also need the following axioms for equality:

  1. For each variable $x$, $x=x$.
  2. $(t_{k}=x)\rightarrow(f_{i}^{n}(t_{1},\cdots,t_{k},\cdots,t_{n})=f_{i}^{n}(t_{1},\cdots,x,\cdots,t_{n}))$, where $t_{1},\cdots$, $t_{n}$, and $x$ are any terms, and $f_{i}^{n}$ is any $n$-ary function letter of the language $\mathscr{L}$.
  3. $(t_{k}=x)\rightarrow(A_{i}^{n}(t_{1},\cdots,t_{k},\cdots,t_{n})\rightarrow A_{i}^{n}(t_{1},\cdots,x,\cdots,t_{n}))$, where $t_{1},\cdots$, $t_{n}$, and $x$ are any terms, and $A_{i}^{n}$ is any predicate symbol in $\mathscr{L}$.

The axioms $4$, $5$, $6$, $7$, $8$, and $9$ look trivially true to me, but I have no impression that I have ever used these axioms in mathematics. If ZFC set theory is expressed in the language of first order logic, then I believe it is necessary to use these axioms in giving ZFC axioms.

Can anyone give me examples of how these axioms are used in expressing ZFC axioms?

  • $\begingroup$ Example with Ax.5: $(∀x)(x \ge 0) \to (1 \ge 0)$ $\endgroup$ Dec 20, 2022 at 12:16
  • 1
    $\begingroup$ Ax.6 is a way to manage Generalization: every time you prove that some property P holds for an "unspecified" number $n$, you can conclude that P holds for every number. $\endgroup$ Dec 20, 2022 at 12:18
  • 1
    $\begingroup$ Also, your question is somehow not very well-defined. You are not using axioms when you express something. You're using axioms when you are proving something. This is similar to asking where do we use the sound of the word "hello" when we quietly write down "How are you doing?" on a piece of paper. $\endgroup$
    – Asaf Karagila
    Dec 20, 2022 at 12:21
  • 1
    $\begingroup$ See also Axioms of set theory and logic $\endgroup$ Dec 20, 2022 at 12:28
  • 1
    $\begingroup$ You need these axioms to work with ZFC, but not to "express ZFC". For example, the claim that if two sets are equal, then you can use them interchangeably, or the inference rules that you're using for proofs. But again, these are rules for proofs not rules for writing stuff down. $\endgroup$
    – Asaf Karagila
    Dec 20, 2022 at 12:38

1 Answer 1


I've been self-studying logic and set theory for the last few months so maybe I can offer some insight into how to help getting up to speed via self-study.

Here are some suggestions:

  1. I would get very familiar with the essentials of logic prior to starting set theory.

  2. The fol axioms you have quoted are an example of hilbert-style axioms. These type of axioms are very good when studying the properties of the logic system itself, but not very good at all to support every-day proofs in mathematics (including set theory proofs). The axiomatic system that most closely aligns (in my opinion) to the way we do mathematics is natural deduction. Natural deduction and the system of axioms you have quoted above are equivalent (i.e. we can prove each axiom in natural deduction using the hilbert-type system axioms and vice-versa - although I am yet to see a proof of this - but will be attempting one myself soon!).

  3. To study logic I used mostly "Goldrei: Propositional and Predicate Calculus", which is a very good introduction. However, it does not cover natural deduction (it uses a hilbert-type system, which makes sense as this book is about the logic system itself). Surprsingly, I haven't found any really good rigorous descriptions of the natural deduction system of axioms. The best one I found to date is probably in "vanDalen: Logic and Structure".

  4. There are a few ways of expressing natrual deduction proofs. I like the fitch-style tabular notation rather than the diagramatic/inverted tree type notation.

  5. The "Joy of Sets" looks like it is a very good book, but may be a bit advanced for self-studying set theory for the first time. I used mostly "Cunningham: Set Theory A first Course" and "Enderton: Elements of set Theory", both of which I highly recommend.

  6. As others have said, you don't need the FOL axioms to express the ZFC axioms. The ZFC axioms are new additional axioms that are specific to set theory.

  • $\begingroup$ Thank you very much! "The Joy of Sets" is indeed hard to read for me. I got stuck by an exercise from "The Joy of Sets" two months ago. It asks me to prove that the "Axiom of Foundation" is equivalent to "the Von Neumann Universe". But the Von Neumann universe is poorly explained in the book. Now I am starting from the beginning all over again. Hopefully, the books you recommended will be helpful for me to understand it. $\endgroup$
    – Valac
    Dec 21, 2022 at 9:04

You must log in to answer this question.

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