CubeRootOfTrue<p>ChatGPT has a new sister called Monday. I will let you find out about that. Meanwhile here is what ChatGPT says about using enriched categories to model relevance logic:</p><p>An Example Sketch</p><p> Let V=Pos be a poset-enriched monoidal category where each hom-object is a set of “proofs” or “derivations,” ordered by resource usage.</p><p> Then C(A,B) is itself an object in Pos, i.e., a poset of ways to prove B from A.</p><p> The product ⊗ inside C does not come with free projections, so there is no arrow from (A⊗B) to B in general.</p><p> If someone claims “Surely, we can discard A and prove B anyway,” the poset of proofs for C(A⊗B,B) is _empty_, or has no minimal element if your ordering demands using all resources.</p><p>Thus, the absence of a projection morphism is encoded in the structure of the hom-object: it simply does not contain a suitable proof.</p><p>--<br>here 'resource usage' is 'relevant stuff'</p><p>You can write (A⊗B) -&gt; B, in a diagram. But that arrow is "False", so it doesn't really "exist". Enriched categories capture this concept.</p><p><a href="https://mathstodon.xyz/tags/RelevanceLogic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RelevanceLogic</span></a> <a href="https://mathstodon.xyz/tags/categorytheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>categorytheory</span></a> <a href="https://mathstodon.xyz/tags/enrichedcategory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>enrichedcategory</span></a> <a href="https://mathstodon.xyz/tags/rm3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>rm3</span></a></p>