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
0 votes
1 answer
78 views

Specializing forall quantifiers in Coq

I have an inductively defined type of expressions: ...
Andrii Kozytskyi's user avatar
3 votes
1 answer
158 views

Existential quantification on types in Isabelle

We are currently working on a proof of compactness for classical first order logic using the ultraproduct-based proof. ...
Mesabloo's user avatar
  • 133
8 votes
2 answers
91 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 ...
tinlyx's user avatar
  • 1,896