# Is there a "standard" encoding or model of material set theory in type theory?

I am a little aware of various attempts to axiomize set theory within a theorem prover. Is there a standard kind of encoding of sets? An organic model to interpret set theories into? I would like to be sure my axioms have reasonable interpretations.

Something like this page on pure sets on nlab seems close but also seems a bit hairy.

It feels like these sort of encodings would be easiest with some hairy uses of functional or propositional extensionality which is mildly inconvenient.

You also have classical or choice principle issues. Something like CZF feels like it would be easiest to model in type theory (but hairier to axiomize.)

From what I grasp of the pure set page you want something like

Inductive pregraph :=
| sup X (f: X -> pregraph).

Fixpoint monic p :=
let 'sup X f := p in
f x == f y -> x = y
/\ forall x, monic (f x).

Existing Class monic.

Definition graph := { p: graph | monic p }.

Definition member P '(sup X ps) :=
exists x. ps x == P.


But you need to define equivalence of pregraphs or assume some flavor of extensionality. Then you need to carve out well-founded sets. I feel like there ought to be an easier way.

Maybe it would be nicer to first model proper classes and then model pure sets as classes which are members of other classes?

• I believe the standard way is through Aczel's encoding. In CIC it was implemented by Werner. @MarioCarneiro might offer a neat answer. Commented Jun 14, 2022 at 19:13
• gist.github.com/mstewartgallus/4ad5b8b4ab0a9f0edcbc1385e1c5aac7 started working on some silliness. Should read up on the Aczel stuff Commented Jun 15, 2022 at 0:01
• Ahah I found "Sets in Coq, Coq in Sets" useful Commented Jun 15, 2022 at 0:12
• A material set is a Tarski universe. So an inductive recursive model ought to work. But it's very ugly in languages which don't directly support induction recursive. You'd probably want to interpret an inductive recursive model into Aczel's encoding anyway though Commented Nov 8, 2022 at 21:27

## 2 Answers

(Building on comments by Pedro Sánchez Terraf) As for encoding ZFC in dependent type theory their seems to be the following progression of work

Also, here is a quote from the Flypitch paper which I think captures the essence of both the Aczel-Werner encoding and its extension in that paper.

As with Coq, Lean is able to encode extremely complex objects and reason about their specifications using inductive types. However, the user must be careful to choose the encoding so that properties they wish to reason about are accessible by structural induction, which is the most natural mode of reasoning in the proof assistant. After observing (1) that the Aczel-Werner encoding of ZFC as an inductive type is essentially a special case of the recursive name construction from forcing (c.f. Section 3), and (2) that the automatically-generated induction principle for that inductive type is $$\in$$-induction, it is easy to see that this encoding can be modified to produce a Boolean-valued model of set theory where, again, $$\in$$-induction comes for free.

Depends on which type theory :-)

ZF set theory has been formalised in Isabelle as Isabelle/ZF by directly assuming the ZF axioms (and optionally AC). For those who prefer higher-order logic (also known as simple type theory), it's been done many times.

Details here and an application here. See also an impressive application of Isabelle/ZF.

• Welcome to Proof Assistants! Commented Jun 15, 2022 at 16:35