The Interactive Semioverse¶

Abstract¶

I'll construct an Interactive Semioverse: a mathematical environment in which we work with things only through semiotic interaction, and where all induced semantic material lives inside a disciplined closure system.

Concretely, the Semioverse includes:

a semantic field $H$ that is a complete Heyting algebra, equipped with
a join-continuous modal closure $j:H\to H$, and
a join-continuous Heyting–comonadic temporal trace $G:H\to H$;
a finitary operator algebra $\mathsf{Op}^{\mathrm{def}}$ generated by a typed $\lambda$-calculus and interpreted as semantic endomorphisms $H^n\to H$;
a system of fragments, i.e. finitely generated modal–temporal Heyting subalgebras of $H$;
three closure mechanisms—semantic, syntactic (with finitary justification), and fusion—whose composite $\mathcal{S}$ has a least fixed point.

On top of that core, I introduce a thing-facing layer:

things as persistent handles (not identified with any single semantic element);
an interaction calculus (a term language) whose evaluation yields semantic generators in $H$;
a way to generate thing fragments and compute a semiotic footprint of a thing relative to a state;
thing identity as a groupoid of handle co-reference;
failure semantics as a conservative enrichment compatible with Heyting structure and closure;
provenance as intensional histories over fragments, and a fibration that organizes locality;
evaluation as an ordered-monoid valuation compatible with closure, trace, and modality;
delta and subtraction for comparing and removing semantic influence.

Throughout: I introduce definitions and design choices in the first person; then we use them together to build consequences and constructions.

1. Ambient Semantic Field¶

I'll fix the semantic ambient once and for all.

1.1 Complete Heyting Algebra¶

A complete Heyting algebra is a complete lattice $(H,\le)$ equipped with:

binary meet $\wedge$,
binary join $\vee$,
top $\top$,
bottom $\bot$,
implication $\Rightarrow$,

such that for all $a,b,c\in H$: $c \le (a \Rightarrow b)\quad\text{iff}\quad c\wedge a \le b.$

We will treat $(H,\le)$ as a thin category:

objects are elements of $H$,
there is a unique arrow $a\to b$ iff $a\le b$.

This “thinness” is not a limitation; it is the point: semantic movement is order-theoretic.

I'll fix a modal closure operator $j:H\to H$ satisfying:

(Extensive) $a\le j(a)$,
(Monotone) $a\le b\Rightarrow j(a)\le j(b)$,
(Idempotent) $j(j(a))=j(a)$,
(Join-continuous) for any family $\{a_i\}_{i\in I}$, $$ j\Big(\bigvee_{i\in I} a_i\Big)=\bigvee_{i\in I} j(a_i). $$

The stable fragment is: $H^{\mathrm{st}} := \{a\in H : j(a)=a\}$.

Lemma 1.1 (Stable fragment is Heyting).
$H^{\mathrm{st}}$ is a complete Heyting subalgebra of $H$, and the inclusion preserves Heyting operations.

Sketch. Join-continuity of $j$ and the adjunction definition of $\Rightarrow$ give closure of $H^{\mathrm{st}}$ under Heyting operations.

1.3 Temporal Trace as a Heyting–Comonadic Endofunctor¶

I'll also fix a temporal trace $G:H\to H$ that is simultaneously:

a comonad on the poset-category underlying $H$, and
a complete Heyting algebra endomorphism,
join-continuous.

Formally, comonad structure is:

a monotone endofunctor $G:H\to H$,
a counit $\epsilon_a: G(a)\le a$,
a comultiplication $\delta_a: G(a)\le G(G(a))$,

natural in $a$, satisfying the comonad laws in the thin-category sense.

Axiom 1.2 (Heyting–comonadic coherence).
$G$ preserves all Heyting structure and all joins: $$ G\Big(\bigvee_i a_i\Big)=\bigvee_i G(a_i),\qquad G(a\wedge b)=G(a)\wedge G(b),\qquad G(a\Rightarrow b)=G(a)\Rightarrow G(b), $$ and $G(\top)=\top$, $G(\bot)=\bot$.

This is the coherence that makes temporal unfolding compatible with logic.

1.4 Modality–Trace Interaction and Stability¶

I'll require two interaction principles.

Axiom 1.3 (Basic interaction).
For all $a\in H$, $$j(G(a)) \le G(j(a)).$$

Axiom 1.4 (Stability w.r.t. trace).
For all $a\in H$: - if $a\in H^{\mathrm{st}}$ then $G(a)\in H^{\mathrm{st}}$; - if $G(a)\in H^{\mathrm{st}}$ then $a\in H^{\mathrm{st}}$.

So: $$G(a)\in H^{\mathrm{st}} \iff a\in H^{\mathrm{st}}.$$

Now we can safely work “inside stability” without losing trace structure.

2. Syntactic Operator Algebra¶

I'll now set up the syntactic side: a finitary source of operators we can interpret into $H$.

2.1 Types and Terms¶

We fix:

a type grammar $\mathsf{Ty}$ generated from:
a base type $P$,
function types $A\to B$,
product types $A\times B$;
a typed $\lambda$-calculus with variables, $\lambda$-abstraction, application, pairing, projections, and a chosen set of primitive constants.

For each $n\ge 0$:

$\mathsf{Op}_n$ is the set of closed terms $f$ of type $P^n\to P$,
we quotient by definitional equality (e.g. $\beta\eta$), writing $\mathsf{Op}_n/\equiv$.

Let: $$\mathsf{Op}^{\mathrm{raw}} := \bigcup_{n\ge 0} \mathsf{Op}_n/\equiv.$$

2.2 Definable Operators¶

I'll define $\mathsf{Op}_n^{\mathrm{def}}\subseteq\mathsf{Op}_n/\equiv$ as the smallest set that:

contains all primitive operator constants of arity $n$,
is closed under $\lambda$-definability (abstraction and application staying at type $P^n\to P$),
is closed under composition at type $P$.

Set: $$\mathsf{Op}^{\mathrm{def}} := \bigcup_{n\ge 0} \mathsf{Op}_n^{\mathrm{def}}.$$

We’ll treat $\mathsf{Op}^{\mathrm{def}}$ as a finitary algebra: everything we do syntactically is built from primitives via definability and composition.

3. Fragments and Fragmentwise Reasoning¶

I'll formalize locality: how we reason in finitely generated regions of $H$.

3.1 Modal–Temporal Subalgebras¶

A subset $F\subseteq H$ is a modal–temporal Heyting subalgebra if it is closed under:

Heyting operations $\wedge,\vee,\Rightarrow,\bot,\top$,
modality $j$,
trace $G$.

A fragment is a finitely generated modal–temporal subalgebra: there exists a finite $S\subseteq F$ such that $F$ is the smallest modal–temporal subalgebra containing $S$.

Let $\mathcal{F}(H)$ denote the set of fragments, ordered by inclusion.

3.2 Fragment-Preserving Operators and Restriction¶

Let $f:H^n\to H$.

If $f(F^n)\subseteq F$, we can restrict: $$f|_F : F^n\to F.$$

Definition 3.1 (Fragment-preserving).
$f$ is fragment-preserving if for every fragment $F\in\mathcal{F}(H)$, $$f(F^n)\subseteq F.$$

Fragment-preservation is our “locality discipline” for semantic operators.

3.3 Fragmentwise Equality and Hereditary Extensionality¶

For fragment-preserving $f,g:H^n\to H$ and fragment $F$, we write $f\equiv_F g$ if: $$f(a_1,\dots,a_n)=g(a_1,\dots,a_n)\quad\forall a_i\in F.$$

Definition 3.2 (Hereditarily extensional family).
A family $\mathcal{E}$ of fragment-preserving operators is hereditarily extensional if:

whenever $f,g\in\mathcal{E}$ and $f\equiv_F g$ for some fragment $F$, then for any fragment $F'$ obtained from $F$ by finitely many applications of: - Heyting operations, - $j$, - $G$, - any operator in $\mathcal{E}$, we have $f\equiv_{F'} g$.

Now we can trust that “equal on a fragment” propagates through the ways we actually build semantics.

4. Interpretation into $H$¶

I'll now connect syntax to semantics.

4.1 Interpretation of Definable Operators¶

An interpretation is a family of maps: $$\llbracket - \rrbracket_n : \mathsf{Op}_n^{\mathrm{def}} \to \mathrm{Hom}(H^n,H)$$ such that each $f\in\mathsf{Op}_n^{\mathrm{def}}$ satisfies:

(Monotone & join-continuous) $\llbracket f\rrbracket$ is monotone in each argument and preserves directed joins in each argument.
(Heyting compatibility) the operators corresponding to $\wedge,\vee,\Rightarrow,\bot,\top$ are interpreted as those Heyting operations on $H$.
(Modal homomorphism) $$ j(\llbracket f\rrbracket(\vec a))=\llbracket f\rrbracket(j(\vec a)). $$
(Trace compatibility) $$ G(\llbracket f\rrbracket(\vec a))=\llbracket f\rrbracket(G(\vec a)). $$
(Definitional equality preservation) if $f\equiv g$ syntactically, then $\llbracket f\rrbracket=\llbracket g\rrbracket$.
(Fragment preservation) for every fragment $F$, $$ \llbracket f\rrbracket(F^n)\subseteq F. $$
(Hereditary extensionality) the family $\{\llbracket f\rrbracket : f\in\mathsf{Op}^{\mathrm{def}}\}$ is hereditarily extensional.

We will use these properties constantly without re-mentioning them.

5. Partial States and Closure¶

Now I’ll define the state space in which the Semioverse closes.

5.1 Partial States¶

A partial state is a pair: $$X=(H_X,\Op_X)$$ with $H_X\subseteq H$ and $\Op_X\subseteq \mathsf{Op}^{\mathrm{def}}$.

Let: $$\mathcal{U} := \mathcal{P}(H)\times \mathcal{P}(\mathsf{Op}^{\mathrm{def}})$$ ordered by: $$(H_X,\Op_X)\le (H_Y,\Op_Y)\quad\text{iff}\quad H_X\subseteq H_Y\ \text{and}\ \Op_X\subseteq\Op_Y.$$

Then $(\mathcal{U},\le)$ is a complete lattice under pointwise union/intersection.

5.2 Fusion: Congruence and Naming¶

Fusion enforces coherence between syntax and semantics.

Given $X=(H_X,\Op_X)$, let $\mathcal{F}(H_X)$ be the set of fragments $F\in\mathcal{F}(H)$ with $F\subseteq H_X$.

Define $f\sim_X g$ for $f,g\in\Op_X$ if:

for every fragment $F\in \mathcal{F}(H_X)$, $$ \llbracket f\rrbracket \equiv_F \llbracket g\rrbracket, $$
this equivalence is hereditarily extensional under Heyting operations, $j$, $G$, and operators in $\Op_X$.

Fusion also permits naming semantic behaviors already present.

An operator $h:H^n\to H$ is an admissible behavior over $X$ if it is:

monotone,
join-continuous,
fragment-preserving,
modal (commutes with $j$),
trace-compatible (commutes with $G$),
in the hereditarily extensional closure of $\{\llbracket f\rrbracket : f\in\Op_X\}$.

Let $\Op_X^{\mathrm{fus}}$ be the smallest set such that:

$\Op_X\subseteq \Op_X^{\mathrm{fus}}$,
operators equivalent under $\sim_X$ are identified (up to definitional equality),
any admissible behavior may be named by a fresh symbol $f_h$ with $\llbracket f_h\rrbracket=h$.

Define the fusion closure: $$\mathcal{S}_{\mathrm{fus}}(X) := (H_X,\Op_X^{\mathrm{fus}}).$$

5.3 Semantic Closure¶

Define: $$\mathcal{S}_{\mathrm{sem}}(X) := (H_X',\Op_X),$$ where $H_X'$ is the smallest subset of $H$ such that:

$H_X\subseteq H_X'$,
(Interpretation closure) if $f\in\Op_X$ and $\vec a\in (H_X')^n$, then $\llbracket f\rrbracket(\vec a)\in H_X'$,
(Heyting closure) $H_X'$ is closed under $\wedge,\vee,\Rightarrow,\bot,\top$,
(Modal–trace closure) $H_X'$ is closed under $j$ and $G$,
(Fixed-point closure) if $h:H\to H$ is admissible (as above), then any least/greatest fixed point of $h$ above some element of $H_X'$ is included in $H_X'$.

5.4 Syntactic Closure with Finitary Justification¶

I’ll define “finitary justification” as a compactness principle for adding operators.

Let $X=(H_X,\Op_X)$, $f\in\mathsf{Op}^{\mathrm{def}}$, and $F\subseteq H_X$ a fragment. Say:

$f$ is semantically justified by $F$ over $X$ if there exists $g\in\Op_X$ such that
$$ \llbracket f\rrbracket \equiv_F \llbracket g\rrbracket $$ and this equivalence is hereditarily extensional under Heyting operations, $j$, $G$, and operators in $\Op_X$.

Define: $$\mathcal{S}_{\mathrm{syn}}(X) := (H_X,\Op_X'),$$ where $\Op_X'$ is the smallest set such that:

$\Op_X\subseteq\Op_X'$,
$\Op_X'$ is closed under $\lambda$-definability and composition,
fixed-point constructs are included when their interpretations arise from $\Op_X'$,
(Finitary justification) if $f$ is semantically justified by some finite fragment $F\subseteq H_X$, then $f\in \Op_X'$.

This yields an algebraic compactness statement: $$\mathcal{S}_{\mathrm{syn}}(X)=\bigcup_{F\subseteq_{\mathrm{fin}} H_X}\mathcal{S}_{\mathrm{syn}}(F,\Op_X).$$

5.5 Global Closure and Least Fixed Point¶

Define the composite closure: $$\mathcal{S} := \mathcal{S}_{\mathrm{fus}}\circ \mathcal{S}_{\mathrm{syn}}\circ \mathcal{S}_{\mathrm{sem}} : \mathcal{U}\to\mathcal{U}.$$

$\mathcal{S}$ is monotone and inflationary.

By Knaster–Tarski, $\mathcal{S}$ has a least fixed point: $$X^\star = \bigwedge\{X\in\mathcal{U} : \mathcal{S}(X)\le X\}.$$

Definition 5.1 (Semioverse core).
I’ll call $X^\star=(H_\star,\Op_\star)$ the core semioverse state.

Now we can treat “the Semioverse” as the closure discipline encoded by $\mathcal{S}$ together with its least fixed point $X^\star$.

5.6 Universal Property (Initiality)¶

A semioverse structure consists of:

a complete Heyting algebra $K$ with closure $j_K$ and trace $G_K$ satisfying analogues of Axioms 1.2–1.4,
an interpretation $\llbracket-\rrbracket_K$ of $\mathsf{Op}^{\mathrm{def}}$ into $K$ satisfying the analogues of Section 4,
a fixed point $X_K$ of the induced closure operator extending the same primitive data.

Morphisms preserve all structure (Heyting, $j$, $G$, and interpretation), and 2-equality is fragmentwise extensional equality.

Theorem 5.2 (Initiality).
The core semioverse state $X^\star$ is initial among semioverse structures, up to fragmentwise extensional equality.

Sketch. Standard closure/fixed-point minimality argument plus fusion-as-reflection behavior.

6. Things and Interaction Calculus¶

Up to now, we’ve built a closure-controlled semantic environment. Now I’ll introduce things as the entities we interact with inside it.

6.1 Thing Handles¶

Let $\mathsf{Thing}$ be a set of thing handles. A handle is not an element of $H$; it is an external index that can participate in interaction terms.

I’ll fix an interpretation of handles as semantic seeds: $$\eta : \mathsf{Thing}\to H.$$

We will write: $$\llbracket \tau \rrbracket := \eta(\tau)$$ for $\tau\in\mathsf{Thing}$.

This is the only place where a thing handle touches semantics directly; everything else is mediated by interaction terms and closure.

6.2 Interaction Terms¶

I’ll define interaction terms as the smallest set $\mathsf{IxTerm}$ generated by: $$t ::= \tau \mid k(t_1,\dots,t_n),$$ where $\tau\in\mathsf{Thing}$ and $k\in \mathsf{Op}^{\mathrm{def}}$.

Interpretation extends recursively: - $\llbracket \tau\rrbracket = \eta(\tau)$, - $\llbracket k(t_1,\dots,t_n)\rrbracket = \llbracket k\rrbracket(\llbracket t_1\rrbracket,\dots,\llbracket t_n\rrbracket)$.

Now we can treat interaction terms as semiotic “touches” that yield semantic material in $H$.

6.3 Interaction Surfaces¶

Given a partial state $X$, an interaction surface is auxiliary data: $$\mathrm{Ix}_X : \mathsf{Thing}\to \mathcal{P}(\mathsf{IxTerm}),$$ typically finite-valued.

For a handle $\tau$, write: $$\mathrm{Ix}_X(\tau)\subseteq \mathsf{IxTerm}.$$

I’ll emphasize: $\mathrm{Ix}_X$ is not itself semantic content. Semantic consequences are mediated through fragments.

6.4 Thing Fragments¶

Given $X$ and $\tau$, define its interaction denotation set: $$T_{\tau,X} := \{\llbracket t\rrbracket : t\in \mathrm{Ix}_X(\tau)\}\subseteq H.$$

Define the thing fragment: $$F_{\tau,X} := \text{the least fragment containing } T_{\tau,X}.$$

Lemma 6.1 (Monotonicity in interaction surface).
If $\mathrm{Ix}_X(\tau)\subseteq \mathrm{Ix}'_X(\tau)$, then $F_{\tau,X}\subseteq F'_{\tau,X}$.

Proof. Inclusion of generators implies inclusion of generated fragments.

6.5 Closing a Fragment Inside a State¶

Since $\mathcal{S}$ acts on partial states, I’ll define a convenient shorthand.

If $F\subseteq H_X$ is a fragment, define the restricted partial state: $$X|_F := (F,\Op_X).$$

Then define: $$\mathcal{S}_X(F) := \mathcal{S}(X|_F).$$

This is “closing $F$ using the operator context of $X$”.

6.6 Semiotic Footprint of a Thing¶

Now we can define what we actually use.

Definition 6.2 (Footprint).
For $\tau\in\mathsf{Thing}$ in state $X$, define the semiotic footprint: $$\mathrm{Foot}_X(\tau) := \mathcal{S}_X(F_{\tau,X}).$$

This is a closed partial state built from the thing’s fragment.

Theorem 6.3 (Boundedness by the semioverse core).
For any $X\le X^\star$ and any $\tau$, $$\mathrm{Foot}_X(\tau) \le X^\star.$$

Proof. $X^\star$ is the least fixed point extending the primitive data; closure of any substate is below it by monotonicity and minimality.

6.7 Local Persistence¶

Sometimes interactions “stay local” and do not promote globally.

Definition 6.4 (Locally persistent interaction).
An interaction term $t\in \mathrm{Ix}_X(\tau)$ is locally persistent if: $$ \llbracket t\rrbracket \in F_{\tau,X} \quad\text{but}\quad \llbracket t\rrbracket \notin H_{\mathrm{Foot}_X(\tau)}. $$

Now we can distinguish “locally generating” from “globally closing”.

7. Identity of Things¶

Now I’ll formalize co-reference: the same thing can be addressed by different handles.

7.1 Handle Co-Reference¶

Introduce a symmetric relation $\approx$ on $\mathsf{Thing}$. Informally, $\tau\approx\tau'$ means “these handles co-refer”.

I’ll require semantic seed coherence: $$\tau\approx\tau' \Rightarrow \eta(\tau)=\eta(\tau').$$

7.2 Identity Groupoid¶

Define a groupoid $\mathcal{G}$ with:

objects: $\tau\in\mathsf{Thing}$,
morphisms: $(\tau,\tau')$ whenever $\tau\approx\tau'$,
identities $(\tau,\tau)$,
inverses $(\tau',\tau)$,
composition $(\tau,\tau')\circ(\tau',\tau'')=(\tau,\tau'')$.

Theorem 7.1.
$\mathcal{G}$ is a small groupoid.

7.3 Transport on Interaction Terms¶

If $\tau\approx\tau'$, define transport $t[\tau'/\tau]$ by replacing occurrences of $\tau$ with $\tau'$ inside $t$.

Lemma 7.2 (Interpretation coherence under transport).
If $\tau\approx\tau'$, then for any interaction term $t$ whose evaluation is defined, $$\llbracket t\rrbracket = \llbracket t[\tau'/\tau]\rrbracket$$ in any fragment containing the relevant seeds.

Proof. Transport preserves leaf denotations ($\eta(\tau)=\eta(\tau')$) and definable operators are extensional on fragments.

8. Failure Semantics and Partiality¶

Now I’ll add failure as a conservative enrichment. The guiding rule is: failure is never “silently healed.”

8.1 Failure Value and Failure Marks¶

We designate $\bot\in H$ as a semantic failure value: $$\bot_{\mathrm{fail}} := \bot.$$

A failure-annotated partial state is: $$X=(H_X,\Op_X,\mathsf{Fail}_X),$$ where $\mathsf{Fail}_X\subseteq H_X\cup \Op_X \cup \mathsf{IxTerm}$ is a set of marked elements.

If an interaction term is ill-formed or an application is undefined, we interpret it as $\bot_{\mathrm{fail}}$ and mark the corresponding element.

8.2 Failure Fragment¶

Define the failure fragment as the least fragment containing $\bot_{\mathrm{fail}}$: $$\mathcal{F}_{\mathrm{fail}} := \{\bot_{\mathrm{fail}}\}.$$

Lemma 8.1 (Failure propagation inside a fragment).
If any generator of a fragment is $\bot_{\mathrm{fail}}$, then the fragment collapses to $\mathcal{F}_{\mathrm{fail}}$.

8.3 Closure Compatibility¶

We require that closure operators record failures monotonically:

if a closure step introduces $\bot_{\mathrm{fail}}$, then $\bot_{\mathrm{fail}}$ remains present thereafter,
failure marks only grow under monotone extension.

This is bookkeeping, not new semantics; the Heyting algebra already contains $\bot$.

9. Provenance Semantics¶

Now I’ll attach intensional histories to semantic elements inside fragments.

9.1 Provenance Histories¶

A provenance history for $a\in F$ is a finite sequence of construction steps, each step being one of:

introduction as $\llbracket t\rrbracket$ for some $t\in\mathsf{IxTerm}$,
formation by a Heyting operation, $j$, or $G$,
application of a definable operator $\llbracket f\rrbracket$,
inclusion under fragment extension.

Two histories are comparable if one refines the other by inserting/collapsing intermediate steps.

9.2 Provenance Category of a Fragment¶

For each fragment $F$, define a small category $P(F)$ where:

objects are provenance histories of elements of $F$,
morphisms are refinement relations (coarser $\to$ finer).

Composition is concatenation of refinements.

9.3 Fragment-Indexed Structures and Provenance Functor¶

Let $\mathcal{F}$ be the poset-category of fragments under inclusion.

Define a total category $\mathcal{E}$:

objects are pairs $(F,X)$ where $F$ is a fragment and $X$ is a partial state with $H_X\subseteq F$,
morphisms $(F,X)\to(F',X')$ exist when $F\subseteq F'$ and $X\le X'$.

Projection: $$\pi:\mathcal{E}\to\mathcal{F},\quad \pi(F,X)=F.$$

Define: $$\mathcal{P}:\mathcal{E}\to \mathbf{Cat},\quad \mathcal{P}(F,X):=P(F),$$ and on morphisms, extend histories along fragment inclusions.

Lemma 9.1.
$\mathcal{P}$ is functorial.

10. Evaluation Semantics¶

Now I’ll add a quantitative layer without baking in any normative reading.

10.1 Evaluation Monoid and Valuation¶

Fix a commutative ordered monoid $(M,\le_M,+,0)$.

A valuation is a monotone map: $$\mu:H\to M$$ satisfying:

$\mu(\bot_{\mathrm{fail}})=0$,
$\mu(a\vee b)\le_M \mu(a)+\mu(b)$,
$\mu(j(a))\ge_M \mu(a)$,
$\mu(G(a))\ge_M \mu(a)$.

10.2 Fragment and Footprint Valuations¶

For a finitely generated fragment $F$ with a chosen finite generator set $\mathrm{gens}(F)$, define: $$\mu(F):=\sum_{a\in \mathrm{gens}(F)} \mu(a).$$

For a closed partial state $Y=(H_Y,\Op_Y)$, define: $$\mu(Y):=\sup\{\mu(F) : F\subseteq H_Y \text{ is a fragment}\}.$$

For a thing $\tau$ in state $X$, define: $$\mu(\tau;X) := \mu(\mathrm{Foot}_X(\tau)).$$

Now we can compare footprints quantitatively.

11. Delta: Difference Across Interactions, Fragments, Footprints¶

Now I’ll define the three deltas we use.

11.1 Interaction-Surface Delta¶

For finite interaction surfaces $A,B\subseteq \mathsf{IxTerm}$: $$\Delta_{\mathrm{ix}}(A,B) := (A\setminus B)\cup (B\setminus A).$$

11.2 Fragment Delta¶

For fragments $F,G\subseteq H$: $$\Delta_{\mathrm{frag}}(F,G) := \text{least fragment containing }(F\cup G)\setminus(F\cap G).$$

11.3 Footprint Delta for Things¶

Given $\tau,\tau'\in\mathsf{Thing}$ in state $X$, define: $$ \Delta_{\mathrm{foot}}(\tau,\tau';X) := \mathcal{S}X\big(\Delta)\big). $$}}(F_{\tau,X},F_{\tau',X

We can also measure magnitude: $$\mu\big(\Delta_{\mathrm{foot}}(\tau,\tau';X)\big).$$

12. Subtraction: Removing Semantic Influence¶

Now I’ll define a disciplined removal operation.

12.1 Heyting Subtraction on Elements¶

For $a,b\in H$, define: $$a\ominus b := a \wedge (b\Rightarrow \bot).$$

This uses the Heyting pseudo-complement $(b\Rightarrow\bot)$.

Lemma 12.1.
For all $a,b\in H$: 1. $a\ominus b \le a$, 2. if $c\wedge b\le \bot$ then $c\le a\ominus b$.

12.2 Fragment Support and Fragment Subtraction¶

Define fragment support: $$s(F):=\bigvee_{x\in F} x.$$

Define fragment subtraction: $$F\ominus G := \text{least fragment containing }\{a\ominus s(G) : a\in F\}.$$

12.3 Subtracting a Thing From a State¶

Let $X=(H_X,\Op_X)$ and $\tau\in\mathsf{Thing}$.

Define the subtraction of $\tau$ from $X$ as: $$X\ominus \tau := (H_X',\Op_X)$$ where $$H_X' := \text{least fragment containing }\{a\ominus s(F_{\tau,X}) : a\in H_X\}.$$

Intuitively: we remove the semantic support induced by $\tau$’s fragment from every element of the current carrier, then re-fragment.

12.4 Relation to Syntactic Forgetting¶

Sometimes we want to “forget” a handle syntactically.

Define: $$X\setminus \tau := \big(H_X\setminus\{\eta(\tau)\},\ \Op_X\setminus\{f\in\Op_X : f\ \text{mentions}\ \tau\}\big).$$

Then the restricted closure is $\mathcal{S}(X\setminus\tau)$.

Theorem 12.2 (Subtraction vs forgetting).
For all $X$ and $\tau$, $$\mathcal{S}(X\ominus \tau)\le \mathcal{S}(X\setminus \tau).$$

Sketch. Forgetting deletes syntactic access routes as well as semantic seeds; subtraction removes semantic support but preserves operator vocabulary.

13. Interaction Operators (Capabilities)¶

13.1 Interaction Operators¶

An interaction operator is a monotone map: $$E:\mathcal{U}\to \mathcal{U}$$ compatible with:

fragments (preserves fragment structure of carriers),
closure (respects $\mathcal{S}$ up to inequality),
failure monotonicity (does not unmark failures),
provenance (admits a lifting on provenance histories),
evaluation monotonicity (does not decrease $\mu$).

I’m not asserting that all these compatibilities are free; I’m defining the operator class by them.

13.2 Monoidal Category of Interaction Operators¶

Let $\mathbf{Int}$ be the category:

single object $\bullet$,
morphisms $\bullet\to\bullet$ are interaction operators,
composition is function composition.

Tensor is composition: $$E\otimes F := E\circ F,$$ identity is $\mathrm{id}$.

Then $\mathbf{Int}$ is a strict monoidal category.

13.3 2-Category of Partial States¶

Define a strict 2-category $\mathbf{Part}$ where:

0-cells are partial states $X\in\mathcal{U}$,
1-cells are monotone maps $f:X\to Y$,
2-cells are refinements $f\Rightarrow g$ when $f(X)\le g(X)$ pointwise.

Then $\mathbf{Int}$ acts on $\mathbf{Part}$ by evaluation: $$(E,X)\mapsto E(X).$$

Now we can talk about composing capabilities and comparing them by refinement.

14. Interface Algebra (External Actions)¶

Now I’ll define an external action syntax and compile it into interaction operators.

14.1 Interface Actions¶

Let $\mathsf{Act}$ be the set of interface actions generated by:

$\mathsf{Inscribe}(\tau,A)$ where $\tau\in\mathsf{Thing}$ and $A\subseteq \mathsf{IxTerm}$ finite,
$\mathsf{Compare}(\tau,\tau')$,
$\mathsf{Subtract}(\tau,\mathrm{Ctx})$ where $\mathrm{Ctx}\in\mathcal{U}$,
$\mathsf{RefineFrag}(F,\varphi)$ where $F$ is a fragment and $\varphi$ is a refinement directive,
$\mathsf{Evaluate}(F)$ (observational),
finite compositions.

14.2 Compilation¶

Define a compilation map: $$\llbracket - \rrbracket_{\mathrm{iface}} : \mathsf{Act}\to \mathbf{Int}$$ by recursion:

$\llbracket \mathsf{Inscribe}(\tau,A)\rrbracket_{\mathrm{iface}} := E^{\mathrm{ix}}_{\tau,A}$, which updates $\mathrm{Ix}_X(\tau)$ to include $A$ (auxiliary) and then optionally re-closes induced fragments as artifacts;
$\llbracket \mathsf{Compare}(\tau,\tau')\rrbracket_{\mathrm{iface}} := E^{\Delta}_{\tau,\tau'}$, which computes and may materialize $\Delta_{\mathrm{foot}}(\tau,\tau';X)$ as comparison artifacts;
$\llbracket \mathsf{Subtract}(\tau,\mathrm{Ctx})\rrbracket_{\mathrm{iface}} := E^{\ominus}_{\tau,\mathrm{Ctx}}$;
$\llbracket \mathsf{RefineFrag}(F,\varphi)\rrbracket_{\mathrm{iface}} := E^{\mathrm{ref}}_{F,\varphi}$;
$\llbracket a_2\circ a_1\rrbracket_{\mathrm{iface}} := \llbracket a_2\rrbracket_{\mathrm{iface}}\circ \llbracket a_1\rrbracket_{\mathrm{iface}}$.

Lemma 14.1.
Every compiled action is an interaction operator, i.e. $\llbracket a\rrbracket_{\mathrm{iface}}\in \mathbf{Int}$.

15. Fragment Fibration and Sheaf Semantics¶

Now I’ll make locality categorical and support gluing of local views.

15.1 Grothendieck Fibration of Fragments¶

Recall:

$\mathcal{F}$ is the poset-category of fragments under inclusion,
$\mathcal{E}$ is the total category of fragment-indexed states,
$\pi:\mathcal{E}\to\mathcal{F}$ is projection.

Theorem 15.1.
$\pi$ is a Grothendieck fibration.

Sketch. Cartesian lifts are given by extending the ambient fragment while holding the state fixed; uniqueness follows from thinness/inclusion structure.

15.2 Presheaf of Semantic Carriers¶

Define a presheaf: $$\mathcal{H}:\mathcal{F}^{op}\to \mathbf{Set}$$ by: $$\mathcal{H}(F):=F,$$ and on inclusions $F\subseteq F'$ by restriction.

15.3 Sheaf Condition (Gluing)¶

Say $\{F_i\}_{i\in I}$ covers $F$ if: $F = \bigvee_i F_i,$ i.e. $F$ is the least fragment containing $\bigcup_i F_i$.

Theorem 15.2 (Sheaf condition).
If $a_i\in F_i$ agree on all intersections $F_i\cap F_j$, then there exists a unique $a\in F$ restricting to each $a_i$.

Sketch. Functional closure under Heyting operations and fragment generation makes gluing unique.

15.4 Closure Preserves Sheaf Semantics¶

Theorem 15.3.
If $\{F_i\}$ covers $F$, then $\mathcal{S}_X(F) = \bigvee_i \mathcal{S}_X(F_i)$ inside the presheaf, up to fragmentwise extensional equality.

16. Coherence Theorems¶

Now I’ll state the coherence results that let us treat this as one object instead of a pile of parts.

16.1 Identity Stability¶

If $\tau\approx\tau'$, then interaction transport preserves footprints: $\mathrm{Foot}_X(\tau)=\mathrm{Foot}_X(\tau')$ whenever the interaction surfaces are transported coherently.

16.2 Provenance Coherence¶

For any interaction operator $E$ that admits a provenance lifting, and any inclusion $F\subseteq F'$, the natural square on provenance categories commutes up to canonical refinement equivalence: $$ \begin{array}{ccc} P(F) & \xrightarrow{E^\sharp_F} & P(E(F)) \ \downarrow & & \downarrow \ P(F') & \xrightarrow{E^\sharp_{F'}} & P(E(F')) \end{array} $$

16.3 Evaluation Coherence¶

For any interaction operator $E$ and any state $X$: $$ \mu(H_X)\le_M \mu(H_{E(X)}), \qquad \mu\big(\mathcal{S}(E(X))\big)\ge_M \mu\big(\mathcal{S}(X)\big). $$

16.4 Stability Under Closure¶

For any finite composition of interaction operators $E_n\circ\cdots\circ E_1$ and any $X\le X^\star$: $\mathcal{S}\big(E_n(\cdots E_1(X)\cdots)\big)\le X^\star.$

This is the “nothing escapes the core semioverse” property.

17. The Interactive Semioverse (Assembled Object)¶

I’ll now package everything into one definition.

Definition 17.1 (Interactive Semioverse).
The Interactive Semioverse is the structure: $$ \mathcal{V} := \big( H, \le, \wedge,\vee,\Rightarrow,\bot,\top, j, G, \mathsf{Op}^{\mathrm{def}}, \llbracket-\rrbracket, \mathcal{F}, \mathcal{U}, \mathcal{S}{\mathrm{sem}},\mathcal{S}}},\mathcal{S{\mathrm{fus}},\mathcal{S}, X^\star, \mathsf{Thing}, \eta, \mathsf{IxTerm}, \mathrm{Ix}, \mathcal{G}, \mathcal{E}\xrightarrow{\pi}\mathcal{F}, \mathcal{P}, \mathcal{H}, (M,\le_M,+,0), \mu, \Delta, \ominus, \mathbf{Int},\mathbf{Part}, \llbracket-\rrbracket_{\mathrm{iface}} \big), $$ equipped with the axioms and coherence conditions stated throughout.}},\Delta_{\mathrm{frag}},\Delta_{\mathrm{foot}

This object supports:

defining things by handles and interaction surfaces,
generating thing fragments and closing them into footprints,
comparing footprints (delta),
removing influence (subtraction and forgetting),
tracking provenance and evaluation,
organizing locality via a fragment fibration and sheaf semantics,
acting via interaction operators and compiling external actions into them.

Theorem 17.2 (Coherence).
$\mathcal{V}$ is well-defined: all operations are compatible with Heyting structure, modality, temporal trace, fragments, closure, provenance, evaluation, and interaction operators.

Sketch. Each layer is defined to be internal to the ambient algebraic/categorical structure, and the coherence statements ensure compatibility across layers.

18. Conclusion¶

I’ve defined an Interactive Semioverse in which things are accessed only via interaction, and where interaction yields semantic material that is controlled by fragments and closure.

Now we can:

treat “thing work” as disciplined fragment generation and closure,
compare things by delta of footprints,
remove influence by subtraction or forgetting,
reason locally via fragments and glue via sheaf semantics,
implement capabilities as interaction operators compiled from external actions.

The Semioverse is not a theory of what things “really are”; it is a theory of what happens—mathematically—when we interact with things through semiotic structure.