bio | website | andrej.com |
---|---|---|
location | Ljubljana | |
age | 43 | |
visits | member for | 5 years, 5 months |
seen | 2 hours ago | |
stats | profile views | 7,297 |
I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.
Mar 24 |
comment |
About the proof of the proposition “there exists irrational numbers a, b such that a^b is rational”
It is sad that this is a research-level question. |
Mar 24 |
comment |
About the proof of the proposition “there exists irrational numbers a, b such that a^b is rational”
I just feel like saying $(\sqrt{2})^{\log_2 9}$. But more seriously, it is unpedagocial to speak about what we know and do not know when explaining the form of a given proof. The proof in question is not constructive because it employs the inference rule of excluded middle -- and the proof remains non-constructive no matter what else you prove or know. However, the proof can be transformed to a different proof which is constructive (assuming there is a constructive proof of irrationality of $\sqrt{2}^{\sqrt{2}}$). |
Mar 12 |
awarded | Good Answer |
Mar 12 |
revised |
What does a theoretical mathematician do?
Removing gender pronouns because someone complained about them. |
Mar 9 |
comment |
A topological concept dual to compactness
Hmm, @PaulTaylor will come to the rescue here. Maybe I am mixing up external and internal definitions. In his setting we actually work internally with exponentials, so we require an "internal" right adjoint to $\Sigma^{!} : \Sigma^1 \to \Sigma^X$. This makes a difference because the said right adjoint needs to be continuous as well. Is that the problem? |
Mar 8 |
accepted | Why is the path fibration a strong Hurewicz fibration? |
Mar 7 |
comment |
Category of Gödel Codings? [Reference Request]
Categories of represented spaces are locally cartesian closed and regular. (I say "categories" because using the Baire space is just one option.) To get Borel realizability going we'd need to know whether there is a reasonable category of measurable spaces and measurable maps which is at least weakly cartesian closed. I thought about this once but did not get far, and my measure-theory colleagues refuse to think about "weakly cartesian closed". |
Mar 7 |
comment |
Category of Gödel Codings? [Reference Request]
When I write that book on computable mathematics I will present classical computability as an arcane way of thinking about computation. I'll even add a hint of perversion to it. |
Mar 6 |
comment |
Category of Gödel Codings? [Reference Request]
Thanks for pointing out that realizability also incorporates the continuous version, namely TTE and equilogical spaces (and domain-theoretic representations as well). It would be interesting to see if the Borel stuff is of the realizability kind as well. |
Mar 6 |
awarded | Enlightened |
Mar 6 |
awarded | Nice Answer |
Mar 5 |
answered | Category of Gödel Codings? [Reference Request] |
Feb 21 |
comment |
What is $\sum_{i=0}^{n}\binom{n}{i}^3$?
@quid: better now? |
Feb 21 |
revised |
What is $\sum_{i=0}^{n}\binom{n}{i}^3$?
added 78 characters in body |
Feb 20 |
comment |
What is $\sum_{i=0}^{n}\binom{n}{i}^3$?
The algorithm is telling you that there is no closed form in terms of rational functions. Of course, the hypergeometric functions are just a dressing -- but so is the binomial symbol for $k = 2$. |
Feb 20 |
answered | What is $\sum_{i=0}^{n}\binom{n}{i}^3$? |
Feb 20 |
comment |
The groupoid of algebraic expressions and proofs
If you specify precisely how composition works (presumably an application of transitivity of equality) then there will be two ways of applyying transitivity for $a = b = c = d$, leading to the MacLane pentagon. Since you did not equate any proofs, you will not get associativity. |
Feb 20 |
comment |
The groupoid of algebraic expressions and proofs
How do you get composition to be associative? |
Feb 18 |
comment |
Reference Request: Category of explicit maps between primitive recursive sets?
It might be more useful for you to ask the question differently. Tell us what you need a category for, and we may be able to suggest a good constructions. Categorical logicians have a few tricks in the hat, but it would be good to know what sort of rabbit you're looking for. |
Feb 18 |
comment |
Reference Request: Category of explicit maps between primitive recursive sets?
Is it intended that there is a morphism between any two objects (if this is a category at all, for what are the identity morphisms and what is the composition)? I can stick into $\Gamma$ something that is false, say $0 = 1$, and get a morphism from anywhere to anywhere. |