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.
16
questions
0
votes
2
answers
191
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 ...
- 175
1
vote
1
answer
75
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 ...
0
votes
1
answer
45
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 ...
0
votes
2
answers
223
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 ...
- 175
7
votes
2
answers
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 ...
- 357
1
vote
1
answer
74
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
7
votes
1
answer
278
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:
...
- 173
1
vote
2
answers
182
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 ...
- 5,877
14
votes
4
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 ...
- 419
4
votes
2
answers
370
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 ...
- 2,768
16
votes
3
answers
989
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. \...
- 2,768
8
votes
1
answer
324
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 ...
- 209
21
votes
1
answer
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 ...
- 485
8
votes
2
answers
237
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
19
votes
0
answers
248
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,038
26
votes
2
answers
952
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 ...
- 407