Subobject Classifier Preview

Preview of Omega_tau: Truth4 will serve as the subobject classifier in the earned topos (Part XIII). The four truth values give tau’s internal logic its paraconsistent character.

Subobject Classifier Preview

Summary

Preview of Omega_tau: Truth4 will serve as the subobject classifier in the earned topos (Part XIII). The four truth values give tau’s internal logic its paraconsistent character.

Statement

%
\label{def:omega-tau}
The \textbf{subobject classifier} of the $\tau$ framework is:
\[
    \boxed{%
    \Omega_\tau := \mathrm{Truth4}
    = \{\mathsf{T}, \mathsf{F}, \mathsf{B}, \mathsf{N}\},}
\]
equipped with the lattice structure
(Definition~\ref{def:truth4}),
the negation operation,
and the designated ``true'' element $\mathsf{T}$.
The \textbf{truth morphism} is the map:
\[
    \mathrm{true} : \{*\} \to \Omega_\tau,
    \quad
    * \mapsto \mathsf{T}.
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 94
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part12/ch48-boolean-recovery.tex lines 497-516

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Logic.BooleanRecovery
• Name: Tau.Logic.Omega_tau

Dependencies

• Canonical: I.D21, I.T13

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.