## Stream: new members

### Topic: Does the following require classical reasoning?

#### Martin C. Martin (Jun 03 2022 at 00:23):

example (a : α) : (r → (∃ (x : α), p x)) → (∃ (x : α), r → p x) := sorry


It certainly seems natural to think about the cases of r true vs false separately. In fact, the witness we need depends on the truth value of r. But that doesn't quite seem like a proof to me.

Does the equivalence (p → q) ↔ (¬ p ∨ q) require classical reasoning? If I could convert the implication into the or, then I could use or.elim and not have to use classical (I think).

#### Ruben Van de Velde (Jun 03 2022 at 07:33):

It sure smells like it's classical, but I don't know/worry enough about non-classical logic to be sure :)

#### Yaël Dillies (Jun 03 2022 at 07:39):

Pretty sure this is a weak version of the axiom of choice, actually.

#### Stuart Presnell (Jun 03 2022 at 13:27):

(p → q) ↔ (¬ p ∨ q) is classical, because as a special case it gives (¬ p ∨ p).

#### Martin C. Martin (Jun 03 2022 at 13:31):

Stuart Presnell said:

(p → q) ↔ (¬ p ∨ q) is classical, because as a special case it gives (¬ p ∨ p).

Ah good point!

#### Stuart Presnell (Jun 03 2022 at 13:32):

Thinking constructively about the example: the LHS says "from r we can produce an x and a proof of p x", while the RHS says "we can produce an x, and with r we can prove p x". But in general we can't produce a term of an arbitrary type — let alone produce one that will turn out to have some particular nice property — so the RHS is stronger than the LHS and so the implication fails.

#### Stuart Presnell (Jun 03 2022 at 13:34):

For example, if r is false and α is empty then the LHS holds trivially but the RHS doesn't hold.

#### Reid Barton (Jun 03 2022 at 13:35):

We're also given a : α. But it might not satisfy p.

#### Reid Barton (Jun 03 2022 at 13:35):

I think it is equivalent to LEM.

Proof below

#### Mario Carneiro (Jun 04 2022 at 08:05):

hehe, not to be confused with the other Martin's axiom

Last updated: Dec 20 2023 at 11:08 UTC