Andrej Bauer
|
Registered User
|
I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.
|
|
9h |
comment |
In what rigorous sense are Sperner’s Lemma and the Brouwer Fixed Point Theorem equivalent? In this particular case a general topos would work to show that they are not equivalent. But in general, when discussing equivalence of statements $A$ and $B$, we have to do it in a context where not both of them are provable (or refutable), lest they are "lost in the background theory". The idea is to a fragment of mathematics that is just strong enough to express the statements. See François's answer, where he identifies the relevant weak logical setting for Spenne'r Lemma and Brouwer's fixed point theorem. |
|
1d |
accepted | Lawvere’s fixed point theorem and the Recursion Theorem |
|
1d |
comment |
Lawvere’s fixed point theorem and the Recursion Theorem A special case of Lavwere's fixed point theorem is a special case of Recursion theorem. |
|
2d |
revised |
Lawvere’s fixed point theorem and the Recursion Theorem added 213 characters in body |
|
2d |
revised |
Lawvere’s fixed point theorem and the Recursion Theorem added 86 characters in body; deleted 1 characters in body; deleted 4 characters in body |
|
2d |
comment |
Lawvere’s fixed point theorem and the Recursion Theorem That's an answer for logicians, yes. Are we all logicians here? I can be. |
|
2d |
answered | Lawvere’s fixed point theorem and the Recursion Theorem |
|
May 19 |
comment |
Importance of separability vs. second-countability And this would be Paul Taylor: paultaylor.eu The photo is a bit blurry, but that's how I percieve Paul most of the time anyway. |
|
May 19 |
comment |
Importance of separability vs. second-countability Overtness is exactly as complicated as compactness. nLab has a bit written about it: ncatlab.org/nlab/show/overt+space |
|
May 19 |
comment |
Importance of separability vs. second-countability This might not be the right decade to make this comment, but separability seems to be just the poor man's version of overtness, something Paul Taylor has been pointing out. If this is indeed the case, then separability would indeed be a suboptimal notion. |
|
May 15 |
comment |
On the large cardinals foundations of categories @Michal: It is a joke of course, but what you seem to worry about is how many jokes it is. Well, the thing to notice is that it is a sequence, not a series. |
|
May 15 |
comment |
On the large cardinals foundations of categories @Asaf: perhaps this may help. The universes are typically taken to be such that $\mathcal{U}_i$ is an element of $\mathcal{U}_{i+1}$. Cummulativity means that $\mathcal{U}_i$ is also a subtype (subset in your parlance) of $\mathcal{U}_{i+1}$. So we can obviously distinguish them because each contains something that another does not. |
|
May 15 |
comment |
On the large cardinals foundations of categories @Asaf: the notion of a universe in type theory is quite flexible. It's good if the universe is closed under many operations, perhaps so many that it forms a small model of type theory, but it doesn't have to. Actually, I am not sure what you're getting at. What does "distinguish between them" mean? |
|
May 14 |
comment |
On the large cardinals foundations of categories The nice embedding is guaranteed by universe cummulativity. By the way, the entire Coq standard library fits into three or four universes. |
|
May 14 |
answered | On the large cardinals foundations of categories |
|
May 9 |
awarded | ● Good Answer |
|
May 9 |
comment |
A question in category theory The modern version is: tell me who your Facebook friends are and I will tell you not only who you are, but also how you use your credit cards. |
|
May 9 |
comment |
A question in category theory Let's be honest here: category theorists are their own friends, which is why the slogan works. |
|
May 9 |
comment |
Is rigour just a ritual that most mathematicians wish to get rid of if they could? We are not machines. Not. Damn you Freud! |
|
May 9 |
comment |
Is rigour just a ritual that most mathematicians wish to get rid of if they could? This answer hit the nail on its head. We are machines, we trust other people, and prefer to hear what ideas they have than why they think those ideas might be true. |
|
May 9 |
awarded | ● Nice Answer |
|
May 8 |
revised |
Is rigour just a ritual that most mathematicians wish to get rid of if they could? added 240 characters in body; deleted 6 characters in body |
|
May 8 |
revised |
Is rigour just a ritual that most mathematicians wish to get rid of if they could? added 208 characters in body; added 39 characters in body |
|
May 8 |
answered | Is rigour just a ritual that most mathematicians wish to get rid of if they could? |
|
May 7 |
awarded | ● Nice Answer |
|
May 6 |
comment |
Definition of subobject classifier in presheaves Steve says the first edition has a rather unfortunate number of typos. |
|
May 6 |
revised |
Definition of subobject classifier in presheaves edited title |
|
May 6 |
answered | Definition of subobject classifier in presheaves |
|
May 5 |
answered | Useful tricks in experimental mathematics |
|
Apr 28 |
comment |
Is there any nontrivial monad on the category of graphs? I think this proves I am very smart. Had I been doing things randomly, at least some of these would be actual examples. It takes a special talent to produce four plausibly-sounding non-examples. |
|
Apr 26 |
comment |
Can nonstandard analysis be used to prove results in constructive or computable analysis? Sam says he is going to give an answer in "due time", whatever that means. |
|
Apr 26 |
comment |
Can nonstandard analysis be used to prove results in constructive or computable analysis? It think Sam Sanders is the expert on this question, I'll alert him to its existence. |
|
Apr 25 |
comment |
Connection between codata and greatest fixed points I don't know what they mean. When I wrote my PhD dissertation I meant "greatest fixed-point in the complete lattice of partial equivalence relations on a partial combinatory algebra". So I did apply Tarski's theorem to a complete lattice. But I do not know how to do it just for sets. |
|
Apr 25 |
comment |
A Model where Dedekind Reals and Cauchy Reals are Different Well, I'd be delighted to see a difference between Cauchy and Dedekind reals which originates from making classical mathematics so weak that even excluded middle cannot rescue the coincidence of reals. |
|
Apr 24 |
awarded | ● Nice Answer |
|
Apr 24 |
comment |
A Model where Dedekind Reals and Cauchy Reals are Different I'll let the expert in the room figure out how many powersets I consumed :-) |
|
Apr 24 |
comment |
A Model where Dedekind Reals and Cauchy Reals are Different What is this "background"? The meta-matheamtical level which I am using to answer the question, or the formal system of which we are considering the models? I was taking about meta-mathematical level, which in my answer is something that suffices to build categories of sheaves. In any case, the original question does not specify any formal system or anything like that. Therefore, the answers should not focus on formal system. They should explain the ideas, either through topological considerations (continuous vs. locally constant), or computability considerations (am looking forward to). |
|
Apr 24 |
comment |
A Model where Dedekind Reals and Cauchy Reals are Different I am not particularly amused when a "background theory" is imposed on an informal argument which I make. It is the logicians' wishful thinking that informal mathematics stands on formal mathematics. But since you raised the issue, possible backgrounds for my answer could be ZFC, IZF, ETCS, IHOL, BZ, or HOTT. Take your pick. |
|
Apr 24 |
answered | Can Inequivalent Topologies Have Same Sheaves/Cohomology? |
|
Apr 24 |
answered | A Model where Dedekind Reals and Cauchy Reals are Different |
|
Apr 23 |
comment |
Connection between codata and greatest fixed points Actually, I think the cool and correct way to do codata is to use set theory with antifoundation. See Barwise's book "Vicious Circles", books.google.si/… |
|
Apr 22 |
comment |
Connection between codata and greatest fixed points Well, if you only care abut the carrier sets, you could look at greatest fixed points, I suppose. I will write another answer. |
|
Apr 22 |
answered | Connection between codata and greatest fixed points |
|
Apr 19 |
revised |
Is there any nontrivial monad on the category of graphs? deleted 252 characters in body |
|
Apr 18 |
comment |
Is there any nontrivial monad on the category of graphs? But surely, there are billions and billions of them. |
|
Apr 18 |
comment |
Is there any nontrivial monad on the category of graphs? Ugh, maybe I should just delete the answer. |
|
Apr 18 |
revised |
Is there any nontrivial monad on the category of graphs? added 70 characters in body |
|
Apr 18 |
comment |
Is there any nontrivial monad on the category of graphs? Oops, that would be a comonad then. Thanks! |
|
Apr 18 |
answered | Is there any nontrivial monad on the category of graphs? |
|
Apr 14 |
comment |
Does “induction” for a functor algebra imply it is initial? @Bruce Westbury: no. |
