Predicate Logic

Z3 - Microsoft Research's SMT-solver - checks millions of lines of code for correctness every day. How? It takes a specification «for all inputs x: if P(x) then Q(x)» - written as ∀x (P(x) → Q(x)) - and automatically either proves it or finds a counterexample. The Windows Kernel, LLVM, AWS protocols - all formally verified through predicate logic. This is not an academic language: it is the language in which industrial software guarantees are written.

• **SMT-solvers (Z3, CVC5)**: program verification, LLVM compiler optimization, formal verification of neural networks - DNN safety guarantees are written as ∀x (P(x) → safe(x))
• **SQL semantics**: WHERE = ∃ over rows (find rows where predicate holds), HAVING = ∀ over groups, FK-constraint = ∀row ∃parent (refs(row, parent))
• **Coq/Lean4**: formal proofs of backprop correctness, SGD convergence - written in predicate logic, each step applies quantifier rules
• **Property-based testing**: Hypothesis (@given), QuickCheck - checking ∀x P(x) on random x. Found a counterexample - that is a bug. No counterexample - «probably correct»

Предварительные знания

• Propositional Logic

Predicate P(x) and quantifiers: ∀ vs ∃

Propositional logic hits a wall at the first real engineering task. «All inputs pass validation» - impossible to express without variables. SQL WHERE-clause - impossible. API contract «for every request there is a response» - same problem. This is not a flaw in the theory: propositional logic simply cannot talk about sets. Predicate logic can.

**Predicate P(x)** - a function from the domain into {True, False}. By itself - not a proposition. Becomes one when a value is substituted or a quantifier is added. - P(x) = «x > 5» - predicate (depends on x) - P(3) = «3 > 5» - proposition (False) - **∀x P(x)** - «for all x, P(x) holds» (universal quantifier) - **∃x P(x)** - «there exists x for which P(x) holds» (existential quantifier)

Z3 from Microsoft Research checks millions of lines of code daily - by taking a specification «for all inputs x: if P(x) then Q(x)», writing it as ∀x (P(x) → Q(x)), and automatically either proving it or finding a counterexample. SQL does the same under a different name: SELECT WHERE is ∃ over table rows.

**Proving vs disproving:** - ∀x P(x) - must be proved for all x. One counterexample is enough to disprove. - ∃x P(x) - one witness x is enough. Disproving requires showing P(x) false for all x.

Negating quantifiers: De Morgan for infinite sets

Z3 finds bugs not by proof, but by refutation. The user writes «all inputs are valid» - ∀x P(x). Z3 searches for a counterexample, i.e., solves ¬∀x P(x). By De Morgan's law for quantifiers, this equals ∃x ¬P(x) - «there exists x for which P(x) is false». One rule, and counterexample search reduces to a SAT problem.

**De Morgan's laws for quantifiers:** - **¬∀x P(x) ≡ ∃x ¬P(x)** - «not all» = «at least one exception exists» - **¬∃x P(x) ≡ ∀x ¬P(x)** - «none exists» = «all fail the predicate» Analogy to propositional logic: ¬(p ∧ q) ≡ ¬p ∨ ¬q - the same De Morgan, but for infinite AND/OR over the domain.

Lean4 and Coq - formal proof systems - apply exactly these laws when proving ML algorithm correctness. Convergence of SGD, correctness of backprop - all of it is chains of quantifiers where each step applies De Morgan or another equivalence. Predicate logic is not an academic relic: it is the language in which safety guarantees of neural networks are written.

**Common mistake:** «not all» is not «none». - ¬∀x P(x) = ∃x ¬P(x) - «there is at least one violator» (weaker) - ∀x ¬P(x) - «no one satisfies it» (stronger) Example: «not all tests pass» is not «no test passes». The second is a disaster; the first is just a bug.

Nested quantifiers: ∀x ∃y vs ∃y ∀x - order decides everything

«Every user has a password» and «there exists one password for all users» differ by two transpositions. The first is standard practice; the second is a security catastrophe. In quantifier notation: ∀x ∃y vs ∃y ∀x. Two symbols swapped - opposite meanings. Databases, matrices, distributed systems - everywhere this order is essential.

**The order of quantifiers is critically important:** - **∀x ∃y R(x, y)** - «for each x there is its own y» (y depends on x) - **∃y ∀x R(x, y)** - «there exists one y shared by all x» (y is fixed) If ∃y ∀x is true, then ∀x ∃y is also true - but not the other way around. «One for all» is strictly stronger than «to each their own».

In linear algebra ∃y ∀x R(x,y) captures the existence of an eigenvector direction. In relational databases ∀x ∃y is the FK-constraint: every child row references its own parent row. SMT-solvers eliminate nested ∃ via skolemization - each ∃ becomes a function of the preceding ∀ variables, reducing the formula to a pure ∀ form that can be checked.

**Mnemonic:** read left to right. ∀x ∃y - «for each x» (fix x), «find y» (y may depend on x). ∃y ∀x - «fix one y up front», «it works for every x». The second is much stronger.

Key Ideas

• **Predicate P(x)** - a function into {True, False}. Substituting a value or adding a quantifier turns it into a proposition
• **∀x P(x)** - «for all», **∃x P(x)** - «there exists». In code: all() and any(). In SQL: WHERE (∃) and FK-constraint (∀∃)
• **De Morgan for quantifiers:** ¬∀x P(x) ≡ ∃x ¬P(x) and ¬∃x P(x) ≡ ∀x ¬P(x). Z3 uses this to search for counterexamples
• **Quantifier order is critical:** ∀x ∃y - «to each their own» (weaker), ∃y ∀x - «one for all» (stronger). From ∃y ∀x follows ∀x ∃y, but not vice versa
• **Skolemization** - how SMT-solvers eliminate ∃: each ∃y becomes a function f(x) of the preceding ∀ variables

Related Topics

Predicate logic is the foundation for mathematical proofs and formal verification:

• Propositional Logic — Predicate logic is a superset: adds quantifiers, variables, and domains
• Proof Methods — Proofs use quantifiers: ∀-introduction, ∃-introduction, counterexample
• Relations and Functions — R(x,y) is a binary predicate; reflexivity = ∀x R(x,x), transitivity = ∀x∀y∀z (R(x,y)∧R(y,z)→R(x,z))

Вопросы для размышления

• Z3 converts ∀x ∃y into a skolem function f(x) - why exactly that direction? What happens if ∀ and ∃ are swapped?
• The statement ∀user ∃session (authenticated(user, session)) - is this a FK-constraint or something stronger? How does it differ from ∃session ∀user?
• Hypothesis searches for counterexamples to ∀x P(x). If none found after a thousand tries - has it proved the theorem? What does property-based testing actually guarantee?

Связанные уроки

• dm-02 — Propositional logic is the foundation; quantifiers extend it
• dm-04 — Set membership x∈A is a predicate; set theory uses quantifiers throughout
• dm-07 — Proof methods: ∀-introduction, ∃-introduction, counterexample search
• dm-05 — R(x,y) is a binary predicate defining a relation on a set
• alg-01-big-o — Big O definition: ∀n>=n0: f(n)<=c*g(n) - a quantified statement
• ml-01