Questions tagged [quantification]

Given a predicate P on a type T, the universal quantification of P, denoted ∀x:T,P(x) (and with many variations in punctuation), is intended to be true if and only if P(a) is true for every possible element a of T. Similarly, the existential quantification of P (also called its particular quantification), denoted ∃x:T,P(x), is intended to be true if and only if P(a) is true for at least one element a of T. (from nLab)

Filter by
Sorted by
Tagged with
8 votes
2 answers
75 views

Is there a way to convert free variables to (meta) universally quantified variables in Isabelle?

Universally quantified variables are the same as free variables in the following two lemmas from the Isabelle (2021) tutorial section 8.1.2 (with slight changes on the second one): Given ...
  • 1,506