30,562 reputation
381171
bio website dorais.org
location Hanover, NH
age
visits member for 5 years, 8 months
seen 2 hours ago

I like math and a few other things...


Jul
23
awarded  Notable Question
Jul
1
revised What is the reverse mathematical strength of the fundamental theorem of algebra?
small correction
Jul
1
revised What is the reverse mathematical strength of the fundamental theorem of algebra?
added 543 characters in body
Jul
1
answered What is the reverse mathematical strength of the fundamental theorem of algebra?
Jun
28
comment Largest symmetric matrix given rank
Wouldn't the adjacency matrix of a graph also have zeros on the diagonal?
Jun
28
revised Preserving $\omega_1$ is Inaccessible to the reals
fixed grammar
Jun
26
comment Type theory: can multiple elimination rules be defined, in principle?
You may end up with two terms that are 'visibly identical' but not definitionally equal unless you add more rules to fix this. Why not define the first as a special case of the second? Derived rules are fine...
Jun
26
comment Type theory: can multiple elimination rules be defined, in principle?
The elimination rule for nat in dependent type theory has C being a type family over nat and both your elimination rules are special cases of that one.
Jun
11
revised methods for situations where well-posedness criteria hold but global solutions do not exist
edited tags
Jun
10
comment “Family Tree” of Theorems
@YoavKallus Sorry, I misread your description of the arrows. I guess you mean the equivalences rather than the strict implications.
Jun
9
comment “Family Tree” of Theorems
@YoavKallus: Double arrows usually mean that the converse implication is known to be false. Dependency is very hard to define rigorously. The connection is that if $A$ really depends on $B$ then it must be that $B$ implies $A$. Otherwise, we could use something strictly weaker than $A$ to prove $B$. (For example, $A \lor B$ could be used instead of $A$.) There doesn't seem to be any other purely mathematical ways of defining "dependency". There are, of course, historical and sociological ways to define dependency that behave differently.
Jun
9
answered “Family Tree” of Theorems
Jun
9
comment Who needs Replacement anyway?
For every standard $n$ there is a proof that $\mathcal{P}^n(\omega)$ exists. The compactness argument is as follows. Add a fresh constant $a$ and consider the theory BZC + $\{\forall y \phi(a,y) \to |y| > |\mathcal{P}^n(a \cup \omega)| : n = 0,1,2,\ldots\}$. In a model of this theory, there can be no standard $n$ such that $\exists y(\phi(a,y) \land |y| \leq |\mathcal{P}^n(a \cup \omega)|)$ holds. Therefore the theory is inconsistent, which gives the required $n$.
Jun
9
comment Who needs Replacement anyway?
@MonroeEskew BZC doesn't prove that this is a total function.
Jun
9
comment Who needs Replacement anyway?
@David Yes, I was trying to cook up the right factoid for you all day. This is as close as I got with a short proof. Anyway, the bottom line is that you might as well assume that the colimit you want exists since the assumption you need to make for the workaround to work isn't much less.
Jun
8
comment Who needs Replacement anyway?
@Todd: Your conclusion is spot on for me! On the other hand, if you remove AC and wellpointedness from ETCS, you get a really nice theory of universal constructions, which turns out to be rather well studied and very fruitful...
Jun
8
comment Who needs Replacement anyway?
@Todd: It's all about the generative process and not about materialism. For a concrete example of a structural theory, Coquand's Calculus of Inductive Constructions is a really nice constructive theory of existence.
Jun
8
revised Who needs Replacement anyway?
correction
Jun
8
revised Who needs Replacement anyway?
addendum
Jun
8
awarded  Nice Answer