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.
Tim Campion created a stub for monad with arities. I have edited the formatting a bit, as usual.
I have added at HomePage in the section Discussion a new sentence with a new link:
If you do contribute to the nLab, you are strongly encouraged to similarly drop a short note there about what you have done – or maybe just about what you plan to do or even what you would like others to do. See Welcome to the nForum (nlabmeta) for more information.
I had completly forgotton about that page Welcome to the nForum (nlabmeta). I re-doscivered it only after my recent related comment here.
More than half of this list is devoted to listing various proof assistants and formalization projects. Does this topic really warrant such an oversized representation in an article with a generic title “mathematics”?
Also, Categories and Sheaves, Sheaves in Geometry and Logic, Higher Topos Theory are good books, but do they really deserve such a prominent placement on top of the article? I suggest removing them.
Created:
Arthur Sard was a mathematician at Queens College.
He got his PhD in 1936 from Harvard University, advised by Marston Morse, in which he proved the Morse–Sard theorem, named after him and Anthony P. Morse (no relation to Marston Morse).
On the Morse–Sard theorem:
Created:
Not to be confused with Marston Morse.
Anthony Perry Morse was a mathematician at the University of California, Berkeley, primarily working in geometric measure theory.
He got his PhD degree in 1937 from Brown University, advised by Clarence Raymond Adams.
On the Morse–Kelley set theory:
On the Morse–Sard lemma:
Added:
A definitive source (by one of the authors of the theory) is
Checking what we have on free coproduct completion I was redirected to this old entry here. I think it will be easier to have a standalone entry on free coproduct completion, and I will create that now and change the redirects.
But while I was here, I added some missing hyperlinks here and there. Such as to free cocompletion
Added a table of contents to topos, a section on "special classes" and one on "higher toposes".
added to identity type a mentioning of the alternative definition in terms of inductive types (paths).
created some minimum at Cardy condition.
Back then some kind soul provided these cobordism pictures at Frobenius algebra. Is that somebody still around and might easily provide also the picture for the Cardy condition?
added a little bit more to split exact sequence.
I pasted in something Mike wrote on sketches and accessible models to sketch. But now it needs tidying up, and I’m wondering if it might have been better placed at accessible category. Alternatively we start a new page on sketch-theoretic model theory. Ideas?
starting something, in order to have a place for connecting various strands (such as the quantum adiabatic theorem, Berry phases, anyon braiding, parameterized quantum computation and dependent linear type theory)
am splitting this off from braid group statistics, meant to host discussion of the anyon model due to:
Daniel P. Arovas, Robert Schrieffer, Frank Wilczek, Anthony Zee, Statistical mechanics of anyons, Nuclear Physics B 251 (1985) 117-126 (reprinted in Wilczek 1990, p. 173-182) doi:10.1016/0550-3213(85)90252-4
Yi-Hong Chen, Frank Wilczek, Edward Witten, Bertrand Halperin, On Anyon Superconductivity, International Journal of Modern Physics B 03 07 (1989) 1001-1067 (reprinted in Wilczek 1990, p. 342-408) doi:10.1142/S0217979289000725, CWWH-AnyonSuperfluidity.pdf:file
which – unfortunately – does not seem to go by a more canonical term than the “fictitious gauge field” that it involves.
I did a bit of reorganization and added more examples at paraconsistent logic, including some comments about linear logic.
Here I copy an old discussion from that page:
I made a big change here; I would argue that the failure of means that ‘’ simply doesn't mean ; but in any case, I've always seen the definition given in terms of negation. In particular, dual-intuitionistic logic has (just as intuitionistic logic has ) but is still considered paraconsistent.
Finn: Hmm. (I presume you meant the ’)’ to come before ’but is still…’; as it stands that last statement is false.) The definitions I’ve seen correspond to what I wrote, but you make a good point – if we want to think of as paraconsistent then the definition by means of ex falso quodlibet does seem wrong. If this is the standard definition, then I certainly won’t object – I’ll just avoid relying on philosophers for information about logic in future.
Toby: Yeah, I'm sure about the standard; our links agree with me too. (And thanks for catching my parenthesis.) As for philosophers, they're not always as precise as mathematicians; that may be the problem. Not to mention, there's a tendency not to include as a logical constant but instead to simply define it as (after proving that these are all equivalent, but ignoring the possibility of an empty model), which leads to conflating the two versions. (In a paraconsistent logic where need not hold, one ought to catch the inapplicability of this definition, but maybe not.)
Finn: I think you’ve hit the nail on the head there: I think ’ex falso quodlibet’ means (as you said above, this says that ’’ means , the least truth-value), but it seems my sources may have meant , without saying so. This is why I never cared much for what’s called ’philosophical logic’ – even though I’m a philosophy graduate studying logic (albeit in a computer science department), it was always too fuzzy for my tastes.
Thanks for clearing this up. Obviously your version should stand.
Toby: You're welcome. But your fancy Latin reminds me that what we have here is technically really the combination of the law of non-contradiction (any contradiction is false: ) and ex falso quodlibet (anything follows from falsehood: ), so I changed the name above.
Finn: Right – I was going to mention that (no, really), but forgot. Perhaps we should incorporate some of this discussion into the article proper, to help resolve any imprecision in other sources. I’ll do that, if you’d rather not, but not now – it’s way past bedtime here in GMT-land.
added pointer to today’s article by Ross Street:
A general abstract formulation of Rost 96 in terms of string diagrams in additive braided monoidal categories is in