2,298 reputation
1327
bio website math.berkeley.edu/~sramesh
location Berkeley, CA
age 29
visits member for 4 years, 10 months
seen Dec 15 at 19:56

I was a graduate student in the Logic program at Berkeley, broadly interested in categorical logic and foundations of mathematics, as well as in applications of category theory to the semantics of programming languages. I work for Google now.


Sep
19
comment Reductio ad absurdum or the contrapositive?
If a proof if $p$ implies $q$ by contrapositive (establishing $\neg q$ implies $\neg p$) is useful because one learns intermediately that ($\neg r_1$ implies $q$), ($\neg r_2$ implies $q$), etc., then a proof of $p$ implies $q$ by contradiction (establishing $\neg (p \wedge \neg q)$) is useful because one learns intermediately ($p \wedge \neg r_1$ implies $q$), ($p \wedge \neg r_2$ implies $q$), etc.
Sep
17
comment Groupoid interpretation of type theory
Does "groupoid" really need a diaeresis over the "i"?
Sep
2
comment Intuitionistic consistency of surjection from naturals to reals
(Also, returning to the dependent choice-based argument against a surjection from N to R, I'm not sure this argument would work when R = MacNeille reals, since it depends on the dichotomy "Either $a_n > (3u + 2v)/5$ or $a_n < (2u + 3v)/5$", which seems an example of precisely the sort of thing which isn't guaranteed for general MacNeille reals)
Sep
1
comment Intuitionistic consistency of surjection from naturals to reals
Well, that's the embedding I'm thinking of too, but it's not obvious to me that $1 \in e(q) \Rightarrow q$. After all, the (only classically injective) lattice homomorphism from $\Omega$ to $\Omega_{\neg \neg}$ is also given by $e(p) = \sup \{1 | p \}$ (as is any suplattice-with-top morphism on the domain $\Omega$).
Sep
1
comment Intuitionistic consistency of surjection from naturals to reals
I like that argument! But it's not obvious to me that the unique complete lattice homomorphism from truth values into MacNeille $[0,1]$ is an embedding. For example, the regular truth values form a nontrivial complete lattice, into which truth values map via double-negation. But this is only an embedding if truth values were Boolean to begin with. So simply being a nontrivial complete lattice is not enough.
Aug
31
comment Intuitionistic consistency of surjection from naturals to reals
Right... I guess what I'm wondering, then, is what goes wrong for injecting MacNeille reals into N in IITM realizability that doesn't go wrong for Dedekind reals. Because if the MacNeille [0, 1] does inject into N, then we will have a surjection from N to MacNeille [0, 1] by sending each natural to the supremum of its preimage. (Or did I misunderstand which notion of reals injects into N? Was that not the Dedekind reals?)
Aug
31
comment Intuitionistic consistency of surjection from naturals to reals
Also, motivated by the dependence of my original argument on the existence of suprema... is there anything interesting to say about intuitionistic surjections from N onto the MacNeille reals?
Aug
31
comment Intuitionistic consistency of surjection from naturals to reals
Also, just to make sure: the provided link only demonstrates an injection $\mathbb{N}^{\mathbb{N}} \to \mathbb{N}$. I'm assuming essentially the same ideas work when the domain is switched to $\mathbb{R}$?
Aug
31
accepted Intuitionistic consistency of surjection from naturals to reals
Aug
31
comment Intuitionistic consistency of surjection from naturals to reals
Thanks! For what it's worth, the part of my self-convincing that doesn't go through must be the idea that subsingletons of reals surject onto reals (I was imagining this could work by sending a subset of the reals to its least upper bound (I suppose by "reals" here, I really mean something like $[0, 1]$)); had that been so, an injection from $\mathbb{R}$ to $\mathbb{N}$ could be reversed into a surjection from $\mathbb{N}$ to $\mathbb{R}$.
Aug
31
comment Intuitionistic consistency of surjection from naturals to reals
Ah, I was right to be unconvinced by my self-convincing, then... :)
Aug
31
revised Intuitionistic consistency of surjection from naturals to reals
deleted 1 characters in body
Aug
31
asked Intuitionistic consistency of surjection from naturals to reals
Aug
15
awarded  Nice Answer
Aug
2
comment Are all the theorems true?
(I suppose I should point out, in case you are not aware, that the reason ZFC + "ZFC is inconsistent" is equiconsistent with ZFC is because of Goedel's second incompleteness theorem)
Aug
2
comment Are all the theorems true?
The example I gave is also not restricted to PA. It works in exactly the same way for any base theory capable of speaking of itself; e.g., if ZFC is consistent, then ZFC + "ZFC is inconsistent" is consistent but not "good".
Aug
2
comment Are all the theorems true?
If question 3 is restricted to theories which are "good", then of course they will be consistent as well... consistency is part of your definition of "goodness"! What could question 3 be asking about, if not the question of whether there is a consistent, non-"good" theory?
Aug
1
answered Are all the theorems true?
Jul
10
comment Fiction books about mathematicians?
Mathematicians should not do, and certainly not enjoy, anything other than mathematical research, lest they give themselves away as human beings with a variety of interests and not a 100% devotion to just the one.
Jun
16
comment Ingenuity in mathematics
[Pedantic note: 0 and n - 1 can both occur if there is only 1 person at the party. But perhaps it is implicit in "party" that there are at least two people.]