Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created a stub for no-cloning theorem.
For the moment what I wanted to highlight is that under the identification of linear logic as quantum logic it is this theorem which is the “linearity” of the logic.
added pointer to
added section on definitions in structural set theories, and added links to subset and improper subset
Anonymous
Added an "Examples"-section to well-pointed topos and to Boolean topos mentioning Set and models for ETCS.
Three questions at axiom of foundation.
created a currently fairly empty entry quantum measurement, just so as to have a place where to give a commented pointer to the article
added a sentence on entanglement and this historical reference:
starting article on Mostowski set theory, which Mike Shulman proved in
to be equivalent in strength to ETCS
Anonymous
added the original reference for the term q-bit:
one more in the list of quantum programming languages
I have been trying to collect some information at Coq.
a stub enty, for the moment just to give a home to:
Roux Cody kindly alerted me of the fact that analog of synthetic mathematics under “computational trinitarianism” in programming theory is that of domain specific embedded programming languages. To record this neat insight I have now created a minimum entry on the latter and cross-linked a bit.
I created a stub certified programming.
That’s motivated from me having expanded the Idea-section at type theory. I enjoyed writing the words “is used in industry”. There are not many Lab pages where I can write these words.
I am saying this only half-jokingly. Somehow there is something deep going on.
Anyway, in (the maybe unlikely) case that somebody reading this here has lots of information about the use and relevance of certified programming in industry, I’d enjoy seeing more information added to that entry.
I added to excluded middle a discussion of the constructive proof of double-negated LEM and how it is a sort of “continuation-passing” transform.
collected some references on the interpretation of the !-modality as the Fock space construction at !-modality.
Cross-linked briefly with he stub entries_Fock space_ and second quantization.
stub for suspension spectrum
started entry on stabilization (in the sense of sending an (oo,1)-category to its free stable (infinity,1)-category)
I want to eventually state more properties of the effect of stabilization on objects here.
adding reference
Anonymous
Jamie Vicary is kindly adding information to the Lab on the higher-category-theory-proof-assistant that he and collaborators are developing, at:
I have added a few more hyperlinks to related nLab entries.
And I have changed the page name from lower case “globular” to upper case “Globular” to fit our conventions on entry titles.
Currently, lower case “globular” still redirects to the entry. But if anyone has links to the lower case version from elsewhere, please consider changing them, for eventually the lower case “globular” really ought to go to a page that disambiguates all sorts of globular-related entries on the nLab, such as globe and globular set, etc.
adding reference
Anonymous
I started an article about Martin-Löf dependent type theory. I hope there aren't any major mistakes!
One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?
starting page for category:people reference and to put the source
Anonymous
I found the organization at Zorn’s lemma a bit rough, so I have tried to smoothen it out a bit
For instance
at one point it had suddenly said “proof of the converse” without a clear statement of the other direction having appeared before. I have created two Theorem-environments and tried to make the statements clearer.
the Idea-section had started out saying that “Zorn’s lemma is a trick”. I think that’s misleading or at least misses the important nature of the thing, so I rewrote that and expanded a bit.
But the foundationalists among you please check!
starting something, to go alongside necessity and possibility
(will adjust page name in a second)
not much here yet, though, under construction
Reading the blog entry
and the reactions to it made me realize that apparently there is no comprehensive list either in print or online of all the insights into QFT in general and observed standard model physics in particular, that have been obtained via results in string theory.
So I have entertained myself with starting to collect notes for such a list:
In the process I have created a bunch of new entries, most of them stubs, linked to from there.
I have given necessity and possibility (which used to redirect to S4-modal logc) an entry of their own.
The entry presently
first recalls the usual axioms;
then complains that these are arguably necessary but not sufficient to characterize the idea of necessity/possibility;
and then points out that if one passes from propositional logic to first-order logic (hyperdoctrines) and/or to dependent type theory, then there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of and , respectively.
You may possibly complain, but not necessarily. Give it a thought. I was upset about the state of affairs of the insufficient axiomatics considered in modal logic for a long time, and this is my attempt to make my peace with it.
David Corfield and I came to start something at EPR paradox
stub entry, for the moment I just needed a place to record this discussion in terms of finite quantum mechanics in terms of dagger-compact categories:
Review in:
stub for homotopy type theory
wrote something at Nullstellensatz, prompted by this old MO comment by Lawvere.
added pointer to:
(I was looking for references which one might point to concerning the term “quantum/classical divide”. For instance, who actually introduced that specific term? People use it to refer to Bohr’s writings, but Bohr never wrote down the specific words “quantum/classical divide”, did he?)
starting page on propositional equality, to contrast with judgmental equality and typal equality (the latter which redirects to identity type)
Anonymous
starting article based off a suggestion from Urs to disambiguate between two-level type theory and other theories with two layers in the nForum page for propositional equality.
Anonymous