Topological Knowledge Operator

Abstract

Topological interior satisfies the four knowledge-operator laws.

Theorem 1.1 (Interior is a topological knowledge operator).

$$\begin{gathered} \forall X:\mathrm{Type}, \\ \mathrm{TopologicalSpace}(X)\Rightarrow \\ (\forall P:\mathrm{Set}(X),\mathrm{interior}(P)\subseteq P)\wedge \\ (\forall P,Q:\mathrm{Set}(X),P\subseteq Q\Rightarrow \mathrm{interior}(P)\subseteq \mathrm{interior}(Q))\wedge \\ (\forall P,Q:\mathrm{Set}(X),\mathrm{interior}(\mathrm{intersection}(P,Q))=\mathrm{intersection}(\mathrm{interior}(P),\mathrm{interior}(Q)))\wedge \\ (\forall P:\mathrm{Set}(X),\mathrm{interior}(\mathrm{interior}(P))=\mathrm{interior}(P)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Epistemic/TopologicalKnowledgeOperator.topological_knowledge_operator_laws (✓ std3). ∎

Source. Repository-derived.

Commentary.

The knowledge operator is the canonical interior operation of the given topology; it is not defined from any target law.

The public statement separately exposes factivity, monotonicity, finite-intersection preservation, and positive introspection.

Each conjunct directly applies the corresponding pinned library law for topological interior.

References

• Truth anchor: D5/S3/ConceptDynamics/Epistemic/TopologicalKnowledgeOperator.topological_knowledge_operator_laws