18
votes
Accepted
Do you need a Hilbert style Epsilon operator for definitions in set theory?
The type theories implemented in proof assistants have definitions which allow introduction of new symbols.
Traditional first-order logic avoids definitions by using instead a meta-theorem stating ...
- 10k
17
votes
Accepted
Well-foundedness: classical equivalence of no infinite descent and accessibility
This is not a Coq proof, but it's a proof sketch using the axiom of dependent choice and LEM to exhibit an equivalence. I believe this is the weakest choice principle you can get away with, but I ...
- 516
11
votes
Accepted
What axioms do I need to search the naturals?
This is an axiom in itself, known as Markov's principle. A more compact but equivalent way to state this axiom is
...
- 2,353
10
votes
Well-foundedness: classical equivalence of no infinite descent and accessibility
The Lean proof is here. It uses the axiom of choice as stated here
I can summarise as follows. We'll prove that if a relation is not well founded, then there is an infinite descending sequence (we ...
8
votes
Does one need a type-theoretical axiom of choice for singletons?
Let $\exists! z \in C . P(z)$ be shorthand for $\exists z \in C . (P(z) \land \forall w \in C . P(w) \to z = w)$.
Your question is related to the axiom of unique choice (AUC): given a relation $R : A \...
- 10k
6
votes
Accepted
Partial and multi-valued choice principles/description operators
The principles you seek are there, but they are simply true, unless you work with a hampered foundation or you mix things up and phrase them badly. Allow me to give a short overview. I trust you will ...
- 10k
5
votes
Do you need a Hilbert style Epsilon operator for definitions in set theory?
If you're mainly interested in set theories based on FOL, then you don't need to know concrete details of what existing systems do, but rather you only need to know and understand the precise ...
- 484
5
votes
Accepted
How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?
I think the main practical use of global choice is to be able to make definitions that depend on choice without having to wrap them inside nonempty. For example, ...
3
votes
Well-foundedness: classical equivalence of no infinite descent and accessibility
Interesting question! My guess would be that just using LEM a relation is well-founded iff it does not contain an entire inverse subrelation. Turning this into a descending sequence represented as ...
- 171
3
votes
Determining why my proof depends on the axiom of choice
I tried to replace parts of the proof with sorry, but I was getting confused by the results of doing so, so I made a small ...
- 161
1
vote
Accepted
Eliminating "Exists Unique" in Lean 3
First, in general you do need the axiom of choice (or a derivative theorem). Unique choice doesn't follow from the base rules of Lean, unlike ZF and univalent foundations. Also, Lean is very minimal ...
- 9,653
1
vote
Do you need a Hilbert style Epsilon operator for definitions in set theory?
As Andrej mentioned you can define a little meta-language which compiles to first order logic.
I've been experimenting with this approach and it's simpler and better than you might expect but just not ...
- 2,868
Only top scored, non community-wiki answers of a minimum length are eligible