Activity for Derek Elkins
| Type | On... | Excerpt | Status | Date |
|---|---|---|---|---|
| Comment | Post #291327 |
The image of "the semantics of Church's type theory" (which you should cite, by the way) is 1) for a logical system, and 2) does not lead to what you wrote. For (1), this isn't a problem, we can just ignore the logical parts, so long as you understand that it is essentially presenting a logic, a form... (more) |
— | 3 days ago |
| Edit | Post #291317 | Initial revision | — | 6 days ago |
| Answer | — |
A: Is there a $\Delta$-complex structure on the sphere with less than three $0$-simplices? If it wasn't for the right to left implication of condition 3, you could do this with a single map out of the 0-simplex. If there are 2 or fewer points in the image of a map from $\Delta^0$, then that means at least two vertices of the image of every map out of the 2-simplex must be the same. Sinc... (more) |
— | 6 days ago |
| Edit | Post #291255 |
Post edited: Had my adjunction backward which made the proof nonsense |
— | 18 days ago |
| Edit | Post #291255 |
Post edited: Nicer proof by being more categorically inspired |
— | 20 days ago |
| Edit | Post #291255 | Post undeleted | — | 20 days ago |
| Edit | Post #291255 |
Post edited: Correct mistake |
— | 20 days ago |
| Edit | Post #291255 | Post deleted | — | 20 days ago |
| Edit | Post #291255 | Initial revision | — | 20 days ago |
| Answer | — |
A: Prove that $\forall x\in\Bbb R:\lfloor x^2\rfloor-\lfloor rx\rfloor\ge-1\iff|r|\le2$. This is definitely more complicated than it needs to be. First, we can rewrite the inequality as $$\lfloor x^2 + 1\rfloor \geq \lfloor rx \rfloor$$ Proof 1 (This is the first proof I wrote, but the second one is nicer and takes a more categorical perspective.) $\lfloor x^2 + 1 \rfloor = 1... (more) |
— | 20 days ago |
| Comment | Post #290803 |
I don't understand many of your questions. They are answered in the article itself. For example, "What are the four axioms regarding equality [... a]nd the fourth?" The answer is the four it lists in the body of the article. The paragraph you quote is a summary of the article and is not meant to be s... (more) |
— | 2 months ago |
| Comment | Post #290727 |
I used "specification language" to emphasize that FOL is a complete system by itself and to emphasize the distinction between the language in which we are specifying something, i.e. FOL, and the thing being specified, in this case ZFC, or, more precisely, the $\in$ predicate. I call it a "specificati... (more) |
— | 3 months ago |
| Comment | Post #290727 |
If you drop the Axiom of Infinity, you're not working in ZFC any longer. The word "rejecting" is a bit ambiguous in this context. It can mean either "not accepting," or it can mean asserting the negation. Not accepting the Axiom of Infinity doesn't mean all sets are finite. It just means can't prove ... (more) |
— | 3 months ago |
| Comment | Post #290727 |
FOL is a specification language and quantifiers and logical connectives, including implication, are what you use to write the specification. You introduce predicate symbols, such as $\in$, to give a name for the things you are describing. Equality is usually taken as part of FOL, but you could also t... (more) |
— | 3 months ago |
| Comment | Post #290637 |
This question has more or less been asked here: https://math.codidact.com/posts/279044 and my answer there captures pretty much what I would say here. Nevertheless, to answer the precise question here, the textbooks are wrong, at least when taken out of context. They are simply doing linguistics but ... (more) |
— | 3 months ago |
| Comment | Post #290538 |
In category theory, where it doesn't make sense to talk about "elements" of objects, as they need not be sets, all concepts must be defined in terms of how arrows relate to each other. In this case, the relevant concept is a [subobject](https://ncatlab.org/nlab/show/subobject) which is an equivalence... (more) |
— | 4 months ago |
| Edit | Post #290515 |
Post edited: |
— | 4 months ago |
| Edit | Post #290515 | Initial revision | — | 4 months ago |
| Answer | — |
A: $\sup(A\cdot B) = (\sup A)(\sup B)$ where $A$ and $B$ bounded sets of positive real numbers To further emphasize the "fake difficulty", we can show that most of this proof is completely "formal", in that it holds for very general reasons that have little to do with real numbers. See the bottom for a detailed, elementary proof that explicitly illustrates that the proof is almost entirely a m... (more) |
— | 4 months ago |
| Comment | Post #290513 |
This is the better proof as what you are proving is that $(\sup A)(\sup B)$ satisfies the universal property of the colimit/coproduct in the partial order category induced by the usual ordering on (positive) reals. (In partial order categories, all colimits are coproducts.) Objects satisfying univers... (more) |
— | 4 months ago |
| Comment | Post #289532 |
Why are you posting questions as multiple accounts? It seems pretty clear that "Ethen" and "Chgg Clou", among others, are the same person. What are the odds that multiple people have independently arrived at a similar time with a heavy interest in basic questions about Canadian lotteries and also sha... (more) |
— | 8 months ago |
| Edit | Post #289507 | Initial revision | — | 8 months ago |
| Answer | — |
A: Picture proof for expansion of $x^n−y^n$ Here's a semi-visual, semi-algebraic approach. A useful alternative perspective on (univariate) polynomials is to think of them as being represented by their sequence of coefficients – filling in zeroes for any missing monomials. With this perspective, multiplying by $z$ simply shifts the se... (more) |
— | 8 months ago |
| Edit | Post #289084 | Initial revision | — | 9 months ago |
| Answer | — |
A: Intuitively, why doesn't picking unpopular integers ($> 31$) lower your probability of winning lotteries? Let's say every lottery you buy exactly one ticket and always use the same numbers. Does that lower your odds of winning versus a strategy where you always pick a random set of numbers? No. Assuming the winning numbers are uniformly distributed, your odds of winning are always directly proportiona... (more) |
— | 9 months ago |
| Edit | Post #288782 | Initial revision | — | 10 months ago |
| Answer | — |
A: Should posting on Meta affect reputation? Just to put out the other option, which is the one I prefer: No, votes on meta posts should not affect main site reputation. (more) |
— | 10 months ago |
| Edit | Post #288411 | Initial revision | — | 11 months ago |
| Answer | — |
A: Average distance from circle's center to a point The problem is indeed that you aren't computing the average distance. What you're computing is a median distance. Essentially, you are equally weighting points that are just slightly outside $C2$ and points that are near the boundary of $C1$, but those contribute different amounts to the average dist... (more) |
— | 11 months ago |
| Edit | Post #288285 |
Post edited: Mention Skolem functions |
— | 11 months ago |
| Edit | Post #288285 | Initial revision | — | 11 months ago |
| Answer | — |
A: how to mathematically express a relationship in which a vector can be any 3D unit vector What makes the most sense to do somewhat depends on the context of this expression. What it seems you are really trying to do is defined $\mathbf e$ as a function of $\mathbf s$. What's making it awkward is that $\mathbf e$ isn't a function of $\mathbf s$ but merely a total (multi-valued) relation... (more) |
— | 11 months ago |
| Edit | Post #288172 | Initial revision | — | 11 months ago |
| Answer | — |
A: Finding a single row of Matrix after exponentiation While there are no doubt even more clever things you can do, the most straightforward approach, which will likely make a significant improvement, is to move from matrix-matrix multiplication to matrix-vector multiplication. Let $ek$ be a (column) vector with all $0$s except the $k$-th entry is $1$... (more) |
— | 11 months ago |
| Comment | Post #288003 |
Sorry, that was just a typo because these examples are using dependent products in a degenerate way that makes them into function types. (I should have just defined $A \to B :\equiv \Pi(A,[x:A]B)$.) It should be $$\lambda(A,[x:A]\Pi(B,[y:B]A),[x:A]\lambda(B,[y:B]A,[y:B]x))$$ And, yes, as mentioned in... (more) |
— | about 1 year ago |
| Comment | Post #288007 |
Yes, this is basically correct. The only caveat is you need to factor in how later defined constants can depend on earlier defined constants. One approach (which I dislike but is technically fine) is to have later constants declared with respect to a context containing all earlier constants, so the c... (more) |
— | about 1 year ago |
| Comment | Post #288005 |
If you treat $\square$ as a term (which is probably not the case), then it is a term that is not classified by a type. If you don't treat it as a term (and in the [original description](https://hal.inria.fr/file/index/docid/76024/filename/RR-0530.pdf) there was no $\square$), then $\*$ is a term that... (more) |
— | about 1 year ago |
| Comment | Post #288007 |
You are correct with that being how you would axiomatize two Tarski-style universes. You do need $T_0$ much as LF needs $El$. Because it gets cluttered, invocations of $El$ are suppresed, but they should actually be all over the place. For example, the type of the identity function would be written l... (more) |
— | about 1 year ago |
| Comment | Post #288007 |
More generally, *by design* the type structure of LF is *not* reflected in the object language. We want to use LF to describe any language we desire which may or may not have pi types or universes or may have pi types/universes that work in a different way than in LF. The reason LF has pi types and a... (more) |
— | about 1 year ago |
| Comment | Post #288007 |
As I explicitly state in the answer you reference, if we're modeling a language with a cumulative hierarchy *within* LF, then the $El$ of LF has no particular relation to the $T_0$ in the object language. As I state there, they aren't even the same *kind* of thing in that context. (more) |
— | about 1 year ago |
| Comment | Post #288005 |
Sure it can be finite. It is for LF. The top-level universe is simply not a term of any other universe. The universe being Tarki-style or Russell-style doesn't change that. (This is why LF doesn't have a code for $\mathsf{Type}$ and a corresponding $El(\mathsf{type})=\mathsf{Type}$ equation. If we di... (more) |
— | about 1 year ago |
| Comment | Post #288003 |
In the informal meta-logic of LF, i.e. the meta-meta-logic relative to our object language, asserting these constants and equations adds them to the signature. From there, you can almost immediately derive those informal rules in the informal meta-meta-logic. But what we care about are the rules of o... (more) |
— | about 1 year ago |
| Edit | Post #288005 | Initial revision | — | about 1 year ago |
| Answer | — |
A: On Tarski-style universes in type theory I'm a bit confused about what you're confused about for the first part. In a Russell-style universe system, we'd have a hierarchy of universes with $\mathcal Ui : \mathcal U{i+1}$, i.e. the $i$th universe is a type in the $(i+1)$th universe. As you state, for a Tarski-style universe system, $\mathcal... (more) |
— | about 1 year ago |
| Edit | Post #288003 | Initial revision | — | about 1 year ago |
| Answer | — |
A: The purpose of logical frameworks in specifying type theories András Kovács answer and comments to your question on Math.SE hit some of the main points. I'll give a bit more detail and context. First, the point of logical frameworks like LF is to be a formal meta-language, and, in particular, a formal specification language. The definitions in the HoTT book ... (more) |
— | about 1 year ago |
| Edit | Post #287980 | Initial revision | — | about 1 year ago |
| Answer | — |
A: The meaning of $\pm$ I think I can explain what's going on by interpreting things more formally, though it could be gotten at informally as well; it's just clearer to see formally. One way to interpret "$y = \pm x$" (and other informal notations like $y = 1,2,3$) is as $y \in \{x, -x\}$ ($y \in \{1,2,3\}$). This is lo... (more) |
— | about 1 year ago |
| Edit | Post #287887 | Initial revision | — | about 1 year ago |
| Answer | — |
A: Unification and generalization of limit and colimit Let $\mathcal I$ be the category with two objects and two parallel arrows between them: $1 \rightrightarrows 2$ and $\mathcal P$ be the cone over $\mathcal I$ with apex labelled $0$. Write $\mathsf f$ and $\mathsf g$ for the two arrows $1 \to 2$. Let $\iota : \mathcal I \hookrightarrow \mathcal P$ be... (more) |
— | about 1 year ago |