# Zulip Chat Archive

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

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

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