trading \exists for \forall

Stream: new members

[Sergey Cherkis]

Given how useful the following equivalence is in constructing proofs, since it trades \exists and \forall is there a standard name for it in logic? And what is the corresponding theorem called in Lean 4?

import Mathlib
variable {X:Type} {Q:Prop} {P:X→Prop}
theorem anyThen_iff_existsThen {X:Type} {Q:Prop} {P:X→Prop} :
(∀ x, P x → Q) ↔ (∃ x, P x) → Q

[Richard Copley]

Hi! Please see #backticks and #mwe.

It's called exists_imp. One way to find it is to write

import Mathlib.Tactic
example {X:Type} {Q:Prop} {P:X→Prop} : (∀ x, P x → Q) ↔ (∃ x, P x) → Q := by
  exact?

This prints the message Try this: exact Iff.symm forall_exists_index. Then go to the definition of forall_exists_index and look around nearby.

I don't know if this rule has a name in English.

[Yaël Dillies]

Yes, it has. This is called the elimination principle of Exists. It comes from the inductive definition of docs#Exists