For all, there exists
Quantifiers turn logic into mathematics. You will introduce universally quantified variables, instantiate hypotheses at specific values, provide witnesses for existence claims, and extract witnesses from existential hypotheses.
Sign in to track your progress
- Prove a statement about every numberintro n picks an arbitrary n. Whatever you prove holds for all of them.9 min
- Use a universal hypothesisA ∀-hypothesis is a function: apply it to the value you need.8 min
- Provide a witnessTo prove ∃ n, …, name the n and prove the property for it.9 min
- Use an existential hypothesisobtain ⟨n, hn⟩ := h gives you the witness and its property.11 min
- Specialize a hypothesisNarrow a general fact to the one instance your goal needs.9 min
- Combine both quantifiersBuild an existence proof whose witness comes from a universal fact.12 min