# Tag Info

## Hot answers tagged axiom-of-choice

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

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

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

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

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

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

Only top scored, non community-wiki answers of a minimum length are eligible