bio | website | dorais.org |
---|---|---|
location | Hanover, NH | |
age | ||
visits | member for | 5 years, 8 months |
seen | 2 hours ago | |
stats | profile views | 14,301 |
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 |