Lesson 4 — Exercises: Predicates and Quantifiers

Ex 1 Predicate over a Finite Domain lambda

Define a predicate $P(x)$: "$x$ is even" as a Python lambda over the domain $\{1, 2, \ldots, 10\}$.

Ex 2 Universal Quantifier — Finite Domain ∀

Check whether $\forall x \in D,\; P(x)$ holds by testing every element of the domain $D = \{1, 2, 3, 4, 5\}$.

Test $P_1(x)$: "$x > 0$" — does it hold for all elements?
Test $P_2(x)$: "$x$ is even" — does it hold for all elements?
For $P_2$, find and print the counterexample (the first $x$ where $P_2(x)$ fails).

Hint: Use all(P(x) for x in domain) and next(x for x in domain if not P(x)).

Ex 3 Existential Quantifier — Finite Domain ∃

Check whether $\exists x \in D,\; P(x)$ holds over the domain $D = \{-5, -4, \ldots, 5\}$.

Hint: Use any(P(x) for x in domain) and next(x for x in domain if P(x), None).

Ex 4 Z3: Universal Quantifier over ℝ Z3 · ForAll · prove

Use Z3 to reason about universal quantification over the real numbers.

Prove $\forall x \in \mathbb{R},\; x^2 \ge 0$ using z3.prove(ForAll([x], x**2 >= 0)).
Show that $\forall x \in \mathbb{R},\; x^2 > 0$ is not valid by finding a counterexample with a Solver.
Print the counterexample value of $x$.

Hint: To find a counterexample to $\forall x\; P(x)$, add $x^2\leq 0$ to the solver and check for model.

Ex 5 Z3: Existential Quantifier — Real vs Integer Z3 · Solver

Use Z3 to determine the satisfiability of $\exists x,\; x^2 = 2$ in two different domains:

Over $\mathbb{R}$ using z3.Real('x') — expected result: sat (since $x = \sqrt{2}$).
Over $\mathbb{Z}$ using z3.Int('x') — expected result: unsat (no integer solution).

What does this demonstrate about the importance of the domain in quantified statements?

Lesson 4 — Predicates and Quantifiers