4
$\begingroup$

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?

$\endgroup$
4

2 Answers 2

7
$\begingroup$

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

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Welcome to Proof Assistants! $\endgroup$ Jun 15, 2022 at 16:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.