Does the following require classical reasoning?

Stream: new members

[Martin C. Martin]

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]

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

[Yaël Dillies]

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

[Stuart Presnell]

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

[Martin C. Martin]

Stuart Presnell said:

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

Ah good point!

[Stuart Presnell]

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]

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

[Reid Barton]

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

[Reid Barton]

I think it is equivalent to LEM.

[Reid Barton]

Proof below

axiom martin (α : Type) (p : α → Prop) (r : Prop) (a : α) :
  (r → (∃ (x : α), p x)) → (∃ (x : α), r → p x)

inductive T (p : Prop)
| ff : T
| tt (h : p) : T

lemma lem (p : Prop) : p ∨ ¬ p :=
begin
  have := martin (T p) (@T.rec p (λ _, Prop) (¬ p) (λ _, p)) p T.ff (λ hp, ⟨T.tt hp, hp⟩),
  cases this with a b,
  cases a with a,
  { right, intro hp, exact b hp hp },
  { left, exact a }
end

[Mario Carneiro]

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