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)
3
questions
0
votes
1
answer
68
views
Specializing forall quantifiers in Coq
I have an inductively defined type of expressions:
...
3
votes
1
answer
137
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.
...
- 133
8
votes
2
answers
89
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,772