Veganism Social

José A. AlonsoHigher order Logic. ~ Mark Jago. <a href="https://youtu.be/fvfzSjNoN9E" rel="nofollow noopener" translate="no" target="_blank">https://youtu.be/fvfzSjNoN9E</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a>

HoldMyTypeconstructive - Why does it matter if canonicity holds for irrelevant types? - Proof Assistants Stack Exchange "It is the untyped λ -calculus with a proof-irrelevant “guard” type G : in order to form any terms of type Λ or to apply the β -rule, we must first exhibit a proof-irrelevant term of type G .The theory has a model in which both G and Λ are interpreted as the empty set. Therefore, there are no closed terms of any type (the only types are G and Λ – we did not assume any extra structure). It is vacuously the case that every closed term is normalizing for any notion of normalization.Observe also that in the non-empty context z:G the untyped λ -calculus springs to life because z can be used to justify the construction of terms and applications of the β -rule. Hence, as soon as we add a (proof-irrelevant!) constant⊢g:Gall hell breaks loose in the empty context (of course the untyped λ -calculus is not normalizing)." <a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a> /nbe <a href="https://proofassistants.stackexchange.com/questions/965/why-does-it-matter-if-canonicity-holds-for-irrelevant-types#:~:text=It%20is%20the,is%20not%20normalizing" rel="nofollow noopener" translate="no" target="_blank">https://proofassistants.stackexchange.com/questions/965/why-does-it-matter-if-canonicity-holds-for-irrelevant-types#:~:text=It%20is%20the,is%20not%20normalizing</a>).

DaLetra EspañolVer la letra de la canción “All I Do” de Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/AllIDo" class="mention hashtag" rel="nofollow noopener" target="_blank">#AllIDo</a> <a href="https://daletra.net/logic/letras/all-i-do.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.net/logic/letras/all-i-do.html</a>

DaLetra EspañolLetra de la canción “Stainless” de Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/Stainless" class="mention hashtag" rel="nofollow noopener" target="_blank">#Stainless</a> <a href="https://daletra.net/logic/letras/stainless.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.net/logic/letras/stainless.html</a>

DaLetra EspañolLetra de la canción “Lord Willin'” de Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/LordWillin" class="mention hashtag" rel="nofollow noopener" target="_blank">#LordWillin</a> <a href="https://daletra.net/logic/letras/lord-willin.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.net/logic/letras/lord-willin.html</a>

𝗖 𝗔 𝗧Just because you can't detect something or verify that it exists doesn't make it non-existent. It just means you can't detect it or verify its existence. If there's no way for you to ever interact with this thing or vis versa, then it would be reasonable to live your life as if this thing doesn't exist just for convenience sake, but that doesn't make it not exist, it just makes its existence, if it does exist, irrelevant to your existence. <a href="https://social.finkhaeuser.de/@jens" class="u-url mention" rel="nofollow noopener" target="_blank">@jens</a> <a href="https://chaos.social/@saxnot" class="u-url mention" rel="nofollow noopener" target="_blank">@saxnot</a> <a href="https://beige.party/@Kierkegaanks" class="u-url mention" rel="nofollow noopener" target="_blank">@Kierkegaanks</a> <a href="https://mastodon.social/@randahl" class="u-url mention" rel="nofollow noopener" target="_blank">@randahl</a> <a href="https://mastodon.social/tags/skepticism" class="mention hashtag" rel="nofollow noopener" target="_blank">#skepticism</a> <a href="https://mastodon.social/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a>

HoldMyTypeConstructive Impredicativity is a simple concern, which says proofs and hence constructions in intuitionist <a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a> can't be circular So we can't use inductive definitions to instantiate dependent types unless they re restricted to specific set ( as that ll be unrestricted. Quantification) Question- can that set be infinite for an extensional type system like <a href="https://mathstodon.xyz/tags/haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#haskell</a> ?

broVbro 🇺🇲The greatest enemy of knowledge is not ignorance, it is the illusion of knowledge. - Daniel J. Boorstin<a href="https://toot.community/tags/CriticalThinking" class="mention hashtag" rel="nofollow noopener" target="_blank">#CriticalThinking</a> <a href="https://toot.community/tags/dunningkrugereffect" class="mention hashtag" rel="nofollow noopener" target="_blank">#dunningkrugereffect</a> <a href="https://toot.community/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a> <a href="https://toot.community/tags/logicalthinking" class="mention hashtag" rel="nofollow noopener" target="_blank">#logicalthinking</a>

Steven CarneiroThe ternary computing system: <a href="https://social.vivaldi.net/tags/number" class="mention hashtag" rel="nofollow noopener" target="_blank">#number</a> <a href="https://social.vivaldi.net/tags/computing" class="mention hashtag" rel="nofollow noopener" target="_blank">#computing</a> <a href="https://social.vivaldi.net/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a> <a href="https://social.vivaldi.net/tags/mathematics" class="mention hashtag" rel="nofollow noopener" target="_blank">#mathematics</a> <a href="https://social.vivaldi.net/tags/scienceandtechnology" class="mention hashtag" rel="nofollow noopener" target="_blank">#scienceandtechnology</a> :calculator:<a href="https://www.scientificamerican.com/article/this-number-system-beats-binary-but-most-computers-cant-use-it/" rel="nofollow noopener" translate="no" target="_blank">https://www.scientificamerican.com/article/this-number-system-beats-binary-but-most-computers-cant-use-it/</a>

DaLetra DeutschText des Liedes “Anziety” von Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/Anziety" class="mention hashtag" rel="nofollow noopener" target="_blank">#Anziety</a> <a href="https://daletra.top/logic/liedtexte/anziety.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.top/logic/liedtexte/anziety.html</a>

DaLetra EspañolConsulta la letra de la canción “Under Pressure” de Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/UnderPressure" class="mention hashtag" rel="nofollow noopener" target="_blank">#UnderPressure</a> <a href="https://daletra.net/logic/letras/under-pressure.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.net/logic/letras/under-pressure.html</a>

DaLetra DeutschText des Liedes “Under Pressure” von Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/UnderPressure" class="mention hashtag" rel="nofollow noopener" target="_blank">#UnderPressure</a> <a href="https://daletra.top/logic/liedtexte/under-pressure.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.top/logic/liedtexte/under-pressure.html</a>

RonSupportsYouJonathan Martin said on MSNBC: "If Obama was guilty of treason (and he isn't) then Trump would not have spoken to him about golf at Jimmy Carter's funeral." <a href="https://mastodon.social/tags/politics" class="mention hashtag" rel="nofollow noopener" target="_blank">#politics</a> <a href="https://mastodon.social/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a>

DaLetra EspañolConsulta la letra de la canción “Growing Pains Iii” de Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/GrowingPainsIii" class="mention hashtag" rel="nofollow noopener" target="_blank">#GrowingPainsIii</a> <a href="https://daletra.net/logic/letras/growing-pains-iii.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.net/logic/letras/growing-pains-iii.html</a>

Yasmin™<a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a>, you're just crazy. I'm not high, I'm basic

SexGamesCCNSFW Sex Game

DaLetra EnglishCheck out the lyrics for the song “Fade Away” by Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/FadeAway" class="mention hashtag" rel="nofollow noopener" target="_blank">#FadeAway</a> <a href="https://daletra.com/logic/lyrics/fade-away.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.com/logic/lyrics/fade-away.html</a>

DaLetra EspañolConsulta la letra de la canción “Ballin'” de Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/Ballin" class="mention hashtag" rel="nofollow noopener" target="_blank">#Ballin</a> <a href="https://daletra.net/logic/letras/ballin.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.net/logic/letras/ballin.html</a>

DaLetra FrançaisParoles de la chanson “Homicide” de Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/Homicide" class="mention hashtag" rel="nofollow noopener" target="_blank">#Homicide</a> <a href="https://daletra.art/logic/paroles/homicide.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.art/logic/paroles/homicide.html</a>

DaLetra EnglishLyrics for the song “Homicide” by Logic <a href="https://mastodon.social/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mastodon.social/tags/Homicide" class="mention hashtag" rel="nofollow noopener" target="_blank">#Homicide</a> <a href="https://daletra.com/logic/lyrics/homicide.html" rel="nofollow noopener" translate="no" target="_blank">https://daletra.com/logic/lyrics/homicide.html</a>

Recent searches

Search options

Administered by:

Server stats:

#logic