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

18 questions
Filter by
Sorted by
Tagged with
67 views

### Proving factors of GCD in Dafny

While trying to prove various properties of GCD I ran into a proof I am a bit stumped with. Gcd can be defined as the max element in the intersection of the divisors of two numbers. In the code I used ...
• 181
82 views

### 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(...
243 views

### 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 ...
1 vote
102 views

### 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 ...
94 views

### 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 ...
1 vote
312 views

### 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 ...
1k views

### 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 ...
• 387
1 vote
94 views

### 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 ...
• 113
392 views

### 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: ...
• 183
1 vote
197 views

### 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 ...
• 6,316
2k 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 ...
• 429
439 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 ...
1k 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. \...
369 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 ...
• 279
1k 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 ...
• 484
266 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/...
• 233
276 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 ...
• 1,058