Closure

From MathWeb

The term closure is fundamental for our theoretical background. Hence it should be well understood. However, it turned out in KWARC discussions that this is not the case. This page is intended to record our difficulties in this respect.

Basis of discussion is the definition of closure from the book Term Rewriting and All That (p.8): The word closure has a precise meaning: the P closure of R is the least set with property P which contains R.

To build such a least set one "just forms the intersection of the (nonempty) family of all sets meeting these properties" (as stated e.g. in First-Order Logic and Automated Theorem Proving p.11).

Thus by these definitions we have $P \;\mathrm{closure} \; \mathrm{of} R := \bigcap\{S|P(S),S\subseteq R\}$ .

This, however, conflicts with the inution that the P closure of R should itself satisfy the predicate P. The following example - found by Normen - demonstrates this conflict: Let $P(S)\Leftrightarrow |S|=2 \wedge S\subset \mathbb{N}$ and $R = {1}$ . In this case the P closure of R would yield a resultset which itself wouldn't satisfy P.

On the other hand it can be shown that this closure definition satisfy the closure axioms. More precisely, from $C_P(R) := \bigcap\{S|P(S),S\subseteq R\}$ follows