top_ne_bot
plain-language theorem explainer
In the topos-of-sets parse of the PRC formal-system interface, the two global points of the subobject classifier are distinct: truth is not falsity. Anyone citing the category-theory realization of δ or the expressivity of the topos system needs this non-degeneracy fact. The proof is a three-line term argument: equality of propositions is biconditional, so True = False yields False from the trivial proof of True.
Claim. Identifying the subobject classifier $\Omega$ with $\mathrm{Prop}$, one has $\top \neq \bot$, i.e. $\mathrm{True} \neq \mathrm{False}$ as elements of $\Omega$.
background
This module parses ordinary category theory (the topos of sets) into the minimal FormalSystem interface used by the Primitive Recognition Calculus inevitability theorem. Tokens are global points of the subobject classifier; discrimination is inequality of those points; endpoints are top and bottom; expression order is derivation-length order.
Here $\Omega$ is abbreviated to $\mathrm{Prop}$, the type of truth values. Its two canonical global points are truth and falsity. In a topos, subobjects of the terminal object are classified by maps into $\Omega$; the characteristic values of the full and empty subobjects of $1$ are precisely $\top$ and $\bot$.
Non-degeneracy is the statement that these two points differ. A topos with $\top = \bot$ collapses to the terminal category (where $0 \cong 1$) and cannot host a nontrivial discrimination relation.
proof idea
Term-mode proof by contradiction. Assume $\mathrm{True} = \mathrm{False}$ as propositions. Rewrite that equality via eq_iff_iff to obtain $\mathrm{True} \leftrightarrow \mathrm{False}$. Apply the forward direction to the canonical inhabitant trivial of $\mathrm{True}$, producing an inhabitant of $\mathrm{False}$, which is absurd. No external lemmas beyond propositional equality-as-iff are required.
why it matters
This is the non-degeneracy hinge of the category-theoretic parse. Downstream, toposSystem_expressive is literally a one-line rephrasing of this fact (expressivity of the topos system is defined as $\top \neq \bot$). The packaged theorem category_theory_realizes_delta conjoins subobject classification of top and bottom, this inequality, and the existence of a PRC embedding into the topos system, stating that the topos of sets realizes the $\delta$ core.
In the broader Recognition Science foundation, $\delta$ is the minimal discrimination structure that any adequate formal system must exhibit. Showing that ordinary topos theory supplies a non-degenerate two-point classifier is the categorical half of that inevitability argument: without $\top \neq \bot$, the parse would be the terminal (empty) theory and could not carry recognition structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.