Skip to main content

Questions tagged [set-theory]

Set theory is the branch of mathematics that studies unordered collections of objects. Questions with this tag will involve proofs about sets or operations on them.

Filter by
Sorted by
Tagged with
16 votes
3 answers

Do you need a Hilbert style Epsilon operator for definitions in set theory?

I've started to play with mechanizing some set theory stuff. I'm not sure if I want a constructive flavor or not yet. Anyhow you can do stuff like axiomize the empty set $$ \top \vdash \exists P. \...
Ms. Molly Stewart-Gallus's user avatar
26 votes
2 answers

What set-theoretic definitions can't easily be formalized in a type theory?

Most proof assistants (with some exceptions like Isabelle/ZF or the B method) rely on type theory. See also the MathOverflow question What makes dependent type theory more suitable than set theory for ...
ErikMD's user avatar
  • 406
14 votes
4 answers

Open source proof assistants for first order logic with equality and set theory

I have been trying to find open source proof assistants for first order logic with equality and set theory. To date, the closest that I have found is Metamath ( and ...
user695931's user avatar
7 votes
2 answers

Is it possible to make a proof assistant program based on ZFC?

I heard that many proof assistant programs are made based on the type theory. For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it. So I have a question. Is it ...
with-forest's user avatar
4 votes
2 answers

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 ...
Ms. Molly Stewart-Gallus's user avatar