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
2 votes
1 answer

Negating universal/existential quantifier in type theory, propositions on elements of the empty type

The universal/existential quantifier: In classical logic, ~∀x P(x) is equivalent to ∃x ~P(x). Looking at the existential quantifier in Lean4, the object ∃ x:nat P(x) is essentially the tuple (x:nat, P(...
Snowybluesky's user avatar
0 votes
2 answers

Is there a multiway system which is equivalent to taking ZFC as axioms?

My understanding is that Stephen Wolfram's concept of a multiway system begins with certain rules and then generates all possible combinations of those rules. There are many distinct mathematical ...
Julius Hamilton's user avatar
1 vote
1 answer

Proving function existence in Coq

Coq beginner here! My question is how to formalize reasoning of the kind "...consider the following function, it has some property, therefore..." in Coq. The challenge is to prove the ...
userl6kgPo0ixv's user avatar
0 votes
1 answer

How to prove commutation of a recursive function over a finite set encoded with binary nat in coq

I needed to define some things in finite set, the original library seemed too complex so I took my friend's advice and I used a library he was developing for this purpose. The library uses BinNat ...
asha soroushpoor's user avatar
0 votes
2 answers

What is the meta-language of ZFC?

This is a good post which says that all proof assistants are founded in HOL, first order logic, or dependent types. Does this mean that the axioms of ZFC are just expressions obtainable from the ...
Julius Hamilton'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
1 vote
1 answer

How do I prove that an element is a within a set in Lean?

Given this code, inductive Test : Type | T1 | T2 example : Test.T1 ∈ { t: Test | t = Test.T1 } := begin sorry end How do I prove that ...
Andrea Nardi's user avatar
7 votes
1 answer

Cardinality of Type in a given universe

I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities: ...
Matt Diamond's user avatar
1 vote
2 answers

How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?

Disclaimer: this question is not asking for code -- it's asking for a proof strategy. For simplicity we may use Fin n (for the usual ...
ice1000's user avatar
  • 6,186
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
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
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
8 votes
1 answer

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 ...
Ember Edison's user avatar
21 votes
1 answer

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 ...
user21820's user avatar
  • 484
8 votes
2 answers

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/...
ACL's user avatar
  • 233
20 votes
0 answers

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 ...
Wojowu's user avatar
  • 1,058
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