18,993 reputation
347108
bio website andrej.com
location Ljubljana
age 43
visits member for 5 years, 5 months
seen 2 hours ago
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.