How to construct ZFC from scratch?

Question

I am interested in understanding the foundations of mathematics. This naturally leads to the study of set-theory and its different axiomatizations. My issue is with the different ways to construct such an axiomatization itself.

As fas as I understand (zero understanding of model theory, so please do not assume its langauge) one can formultate the axioms of, say ZFC, in first order logic with or without equality for example. This should be just a matter of convention. However, I am not sure I understand what these conventions practically imply. Furthermore, I do no understand what are all the options available.

For instance, can I formulate ZFC by leting $=$ be a primitive notion, on par with $\in$ and just require it to obey some axioms? (reflexivity, transitivity, symmetry, substitution). If so how should I formulate substitution? Would it make sense to still have an axiom of extensionality or would it be more correct to define an equality of sets instead and then show that this obeys the axioms of equality?

I am aware of similar questions here, but I found the answers to often assume knowledge beyond mine. I would very much appreciate it if someone could explain in very simple terms how a formal theroy such as ZFC is constructed from scratch, what choices can be made and what are the practical implications of the choices made in such construction.

Answer 1

It depends on the underlying logic one is working with if the underlying logic is the usual $\mathbb{FOL}$ with identity then "$=$" is a logical symbol(like $\land$,$\to$,$\neg$) and the rules for $=$ are already in the proof system so you don’t need any extra axioms for $=$.

On the other hand if one is working in $\mathbb{FOL}$ without identity then "$=$" is no longer a logical symbol and so has to be included as a non-logical symbol(like $\in$) in the language of $ZFC$ and one typically has the axiom $\forall A\forall B(A=B\to \forall x((x \in A \to x\in B) \land (x\in B \to x \in A)))$

Answer 2

There are many ways to formalize first order logic with equality and they have various pros and cons.

The basic framework of constructive propositional logic can be interpreted in terms of Heyting algebras. I mostly like entailment as a transitive relation over propositions because my theorem prover of choice has nice support for these.

A natural deduction style does have the nicety that you can encode proof terms as expressions in the Simply Typed Lambda Calculus (along with product types, sum types and unit and empty types.)

The real problems come with formalizing binders, terms and substitution.

In the abstract the rules are fairly simple as axiom schemas.

You can put anything into an existential

$$[x := e] P \vdash \exists x. P$$

You can unpack an existential into a fresh variable

$$\frac{\begin{split} \textbf{fresh}(y)\\ [x := y] P \vdash Q \end{split}}{\exists x. P \vdash Q }$$

Equality is reflexive

$$ \top \vdash e = e' $$

And composition with the identity relation does nothing (substitution)

$$ \exists x. x = e \wedge P \vdash [x := e]P$$

However, actually concretely implementing first order logic with capture avoiding substitution is really painful.

Simple things first. Assuming your terms have no variable binders (no lambda expressions $\lambda x. e$ without pain) and are not mutually inductive with propositions (no set builder notation without pain $\{ x \in A \mid P \}$) you can encode terms as a free monad over a polynomial endofunctor. This sounds fancy but all this means is you have a tree structure with an extra kind of leaf for variable names.

Technically you don't actually need terms but life gets very painful without them. Anyhow because of the lack of variable binding within terms substitution of variables is very simple. Substitution of variables only really gets painful with propositions. Basically you need to rename any bound variables in a proposition you substitute into. This is a massive pain in practice though which is why a lot of metatheory tools implement more complicated mechanisms like HOAS.

Then there's definitorial expansion and adding newly defined terms to language. Basically there's a metatheorem once you prove unique existence of a value adding a new definition is conservative over the theory. It gets pretty hairy. You can also use a definite description operator but they gets hairy in other ways by mixing terms and propositions.