2,223 reputation
1324
bio website math.berkeley.edu/~sramesh
location Berkeley, CA
age 28
visits member for 4 years, 2 months
seen Apr 13 at 20:50
I am 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.

Nov
17
revised Tarski's Theorem and Gödel's Second Incompleteness Theorem
added 56 characters in body
Nov
17
revised Tarski's Theorem and Gödel's Second Incompleteness Theorem
added 67 characters in body; added 32 characters in body
Nov
17
answered Tarski's Theorem and Gödel's Second Incompleteness Theorem
Nov
2
comment Entailment and implication
It's also worth noting that the trivial topos, like all toposes, internally considers itself to be non-trivial. It just happens to also consider itself to be trivial...
Nov
2
comment Entailment and implication
In the internal logic of the trivial topos, "there is no rational square root of two" is true. It's just that "there is a rational square root of two" is also true. The internal logic of the trivial topos happens to validate all statements; that's what makes it so trivial. But it also means it doesn't harm anything, or make any difference to the model-theoretically valid statements, to consider it a legitimate model.
Oct
21
comment Properly “transfinitely” Euclidean domains
I don't think the omnific integers can admit an ordinal-valued (as opposed to omnific integer-valued) Euclidean function; an ordinal-valued Euclidean function should still lead to being a unique factorization domain, in the usual way, but the omnific integers lack unique factorization (e.g., 2, 3, 5, 7, ..., all remain prime, but $\omega$ is divisible by all infinitely many of them).
Oct
21
asked Properly “transfinitely” Euclidean domains
Oct
4
answered wellfounded sets and predecessors
Oct
3
comment “Mathematics talk” for five year olds
Naive question: what is the sense in which these final tessellations live in FOUR-space?
Sep
23
comment Is it possible to have t triangles in some graph on n vertices?
It's not clear to me that {1, 2, ..., n} is contained in $T_n$. How do I get 2 or 3 triangles with just 3 vertices?
Sep
19
comment Reductio ad absurdum or the contrapositive?
("If a proof if" should be "If a proof of", of course. I am too lazy to delete the comment and retype the whole thing just to fix it)
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