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
12 votes
3 answers
1k views

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 (http://us.metamath.org/index.html) and ...
user avatar
1 vote
2 answers
216 views

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 ...
user avatar
14 votes
3 answers
796 views

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. \...
user avatar
8 votes
1 answer
225 views

Kunen's inconsistency axiom-free proof on Metamath

Kunen's inconsistency theorem is an important theorem in set theory on upper bounds for large cardinals. It has long been thought to be able to be encoded on ZFC, but the full implementation has never ...
user avatar
18 votes
1 answer
839 views

Proof-theoretic comparison table?

I read this CSTheory SE post, which suggests that it is often not clear what variant of MLTT or CIC is being referred to. But I would like to know the proof-theoretic strengths of the various ...
user avatar
  • 420
8 votes
2 answers
198 views

Can the development of proof assistants make mathematicians switch their framework?

The Stack Exchange bot reminded me that I had committed myself to asking some questions, but please allow a possibly naive question, possibly of a philosophical nature rather than mathematical/...
user avatar
  • 183
18 votes
0 answers
193 views

Can we automatically get around set-theoretic difficulties?

One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
user avatar
  • 968
28 votes
2 answers
646 views

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 ...
user avatar
  • 442