Semantic Closure Strict Novelty Criterion

Abstract

Strict common-kernel refinement is exactly escape from semantic closure.

Theorem 1.1 (A candidate is strictly novel exactly when it splits an old kernel pair).

$$\begin{array}{c}\forall X,O:\mathrm{Type},\\ \Gamma :\mathrm{Set}\left(\mathrm{Concept}\left(X,O\right)\right),p:\mathrm{Concept}\left(X,O\right),\\ \mathrm{StrictSubset}\left(\mathrm{jointKernel}\left(\lambda d:\mathrm{insert}\left(p,\Gamma \right),\mathrm{readout}\left(d\right)\right),\mathrm{jointKernel}\left(\lambda d:\Gamma ,\mathrm{readout}\left(d\right)\right)\right)\iff \neg (p\in \mathrm{SemanticClosure}\left(\Gamma \right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeLaws/SemanticClosureStrictNoveltyCriterion.semantic_closure_strict_novelty_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Gamma is an arbitrary family of output-valued concepts on X. The old and extended common kernels are the canonical jointKernel objects, with the candidate inserted into the same family.

The extended kernel is always contained in the old kernel. The inclusion is strict exactly when the frozen zero-gain equality criterion fails, equivalently when the candidate is outside SemanticClosure Gamma.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeLaws/SemanticClosureStrictNoveltyCriterion.semantic_closure_strict_novelty_criterion
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeLaws/SemanticClosureZeroGainCriterion