Predicate Logic

When to Use

Use this skill when working on predicate-logic problems in mathematical logic.

Decision Tree

1. Quantifier Analysis

- Identify: ForAll (universal), Exists (existential) - Scope of quantifiers and free/bound variables - z3_solve.py prove "ForAll([x], P(x)) implies P(a)"

1. Prenex Normal Form

- Move all quantifiers to front - Standardize variables to avoid capture - sympy_compute.py simplify "prenex(formula)"

1. Skolemization (for Exists)

- Replace existential quantifiers with Skolem functions - Exists x. P(x) -> P(c) or P(f(y)) depending on scope - Needed for resolution-based proofs

1. Resolution Proof

- Convert to CNF, negate conclusion - Apply resolution rule until empty clause or saturation - z3solve.py prove "resolutionvalid"

1. Model Theory

- Construct countermodel to refute invalid argument - Finite model for finite domain - z3_solve.py model "Exists([x], P(x) & Not(Q(x)))"

Tool Commands

Z3_Forall

uv run python -m runtime.harness scripts/z3_solve.py prove "ForAll([x], Implies(P(x), Q(x)))"

Z3_Exists

uv run python -m runtime.harness scripts/z3_solve.py sat "Exists([x], And(P(x), Not(Q(x))))"

Z3UniversalInstantiation

uv run python -m runtime.harness scripts/z3_solve.py prove "Implies(ForAll([x], P(x)), P(a))"

Z3_Model

uv run python -m runtime.harness scripts/z3_solve.py model "Exists([x], P(x))"

Cognitive Tools Reference

See .claude/skills/math-mode/SKILL.md for full tool documentation.