Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

2.8K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#linearlogic

0 posts0 participants0 posts today
maonu<p>Good question <a href="https://mathstodon.xyz/tags/linearlogic" class="mention hashtag" rel="tag">#<span>linearlogic</span></a></p>
CubeRootOfTrue<p>Rosen stated: &quot;I argue that the only resolution to such problems [of the subject-object boundary and what constitutes objectivity] is in the recognition that closed loops of causation are &#39;objective&#39;; i.e. legitimate objects of scientific scrutiny. These are explicitly forbidden in any machine or mechanism.&quot;</p><p>Saying that closed causal loops are objective leads directly to the need for non-binary logic. Binary logic cannot deal with causal loops, which are impredicative, like the set that contains itself. Recent developments in modern category theory make this all clear. We can handle this now with monoidal closed categories, a generalization of the old cartesian categories used in binary logic. <a href="https://mathstodon.xyz/tags/RM3" class="mention hashtag" rel="tag">#<span>RM3</span></a> <a href="https://mathstodon.xyz/tags/LinearLogic" class="mention hashtag" rel="tag">#<span>LinearLogic</span></a> <a href="https://mathstodon.xyz/tags/paraconsistent" class="mention hashtag" rel="tag">#<span>paraconsistent</span></a> <a href="https://mathstodon.xyz/tags/paradox" class="mention hashtag" rel="tag">#<span>paradox</span></a></p>
Counting Is Hard<p>Because of Russell&#39;s Paradox, mathematicians realised that unrestricted comprehension is bad and so set about designing systems where the bad thing just couldn&#39;t be defined. But there is another, kinda bonkers way: you can weaken your logic so that \(R \Leftrightarrow \neg R\) does not imply a contradiction.</p><p>In order to derive a contradiction you first use R once, this implies not R, and that *together with R* gives you a contradiction (similarly if you start with not R). But since R is being used twice, you would avoid this inconsistency in a system based on the !-free fragment of linear logic.</p><p>(This curiosity was found in Braüner&#39;s introduction to linear logic <a href="https://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">brics.dk/LS/96/6/BRICS-LS-96-6</span><span class="invisible">.pdf</span></a>)</p><p><a href="https://mathstodon.xyz/tags/linearlogic" class="mention hashtag" rel="tag">#<span>linearlogic</span></a> <a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="tag">#<span>logic</span></a> <a href="https://mathstodon.xyz/tags/types" class="mention hashtag" rel="tag">#<span>types</span></a> <a href="https://mathstodon.xyz/tags/lolwut" class="mention hashtag" rel="tag">#<span>lolwut</span></a></p>
SearchLive feeds
About