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) |
— | 13 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) |
— | 3 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 |
| 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 |
| 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 |
| Comment | Post #287849 |
Both here and in your answer you are not explicitly using the fact that $f$ is constant on equivalences classes nor the definition of the quotient topology. You implicitly use the former when saying $g([x]):=f(x)$ is well-defined in the vague sketch of the proof at the beginning, but not in the separ... (more) |
— | about 1 year ago |
| Comment | Post #287625 |
The equation you give in the title doesn't seem to appear in the image (which you should reproduce the relevant part as MathJax and also crop it much more aggressively). The equation you reference is $\int_C f(x,y)ds = \int_a^b f(x, 0)dx$ There is no $f(x)$. The domain of integration is critical here... (more) |
— | over 1 year ago |
| Comment | Post #286908 |
@#8056 That's also a common definition according to Wikipedia, though [Wikipedia seems to agree with my experience](https://en.wikipedia.org/wiki/Exponentiation#Real_exponents) that the logarithm-based definition is more common. The logarithm-based definition seems more convenient and easier to work ... (more) |
— | over 1 year ago |
| Comment | Post #286908 |
For $e^x$, given *some other* definition of $e^x$, you can certainly prove that the power series definition I gave is the Taylor series. However, if you take the power series I gave as the definition, then there's no need to talk about the theory of Taylor series. You just have a power series; the fa... (more) |
— | over 1 year ago |
| Comment | Post #286908 |
$\lim_{a\to 0}a$ is just $0$. The limit of an (real) expression is either undefined or it's a real number. It's not some infinitesimal thing. So $\forall x.P(x)\implies P(x\pm\lim_{\epsilon\to 0}\epsilon)$ is just $\forall x.P(x)\implies P(x)$. You could try to do something like $\forall x.\exists\ep... (more) |
— | over 1 year ago |
| Comment | Post #286848 |
This doesn't really make a lot of sense currently. It's also doesn't seem to be about graphs. You don't seem to care about any of the connectivity information, while you do seem to care about geometric information that is usually not considered part of a graph. For example, images $G_2$ and $G_3$ wou... (more) |
— | over 1 year ago |
| Comment | Post #286034 |
If you want to talk about square roots of -1, you need to define what "-1" means and what multiplication means so that you can solve the equation $x \cdot x=-1$. If you want to use the embedding $(x,y)\mapsto(x,y,0)$, that's fine, but you haven't defined a multiplication on triplets nor what -1 means... (more) |
— | almost 2 years ago |
| Comment | Post #286034 |
Your constraints amount to asking for the quaternions whose plane of rotation is represented by a bivector with $0$ $y$-$z$ component. This will restrict to a 2D subspace of bivectors, but there's nothing special about this. The space of rotation operators with $0$ $y$-$z$ component, however, is not ... (more) |
— | about 2 years ago |
| Comment | Post #286034 |
In quaternion algebra, $1$ is not identified with the vector $(1,0,0)$. If we used quaternion terminology for complex numbers, we'd say complex numbers have a scalar part (the real part) and a 1D vector part (the imaginary part). These spaces are (double covers of) spaces of rotation operators that *... (more) |
— | about 2 years ago |
| Comment | Post #286034 |
That part is talking about orthogonal planes. But where are you getting triplets in 2D? For the complex plane, we usually identify $(1,0)$ with 1 and $(0,1)$ with $i$. With complex multiplication, we then get $i^2 = -1$ and, modulo sign (the negation is not orthogonal), that's the only square root of... (more) |
— | about 2 years ago |
| Comment | Post #286034 |
Even in 3D, the notion of axis is problematic. Physicists have a distinction between the notion of an "axial vector" and a "position vector". Reflecting a "position vector" in a plane orthogonal to it negates it, while reflecting an "axial vector" does nothing. When stated as a fact lacking context a... (more) |
— | about 2 years ago |
| Comment | Post #286034 |
Yes, I was implying orthogonal when I said it produces 3 as I said explicitly earlier in the comment. Even if you don't limit to orthogonal, infinitely many is still more than 1. For your latter question, in 4D with an orthogonal basis labelled $x$, $y$, $z$, $w$, what is the "axis" orthogonal to the... (more) |
— | about 2 years ago |
| Comment | Post #286034 |
This answer started off good but stumbled pretty badly near the end. Instead of talking about rotations about an axis, talk about rotations in a plane. In 2D, which we can identify with the complex plane, there is obviously one plane in which to rotate. Going up a dimension to 3D doesn't give us just... (more) |
— | about 2 years ago |
| Comment | Post #285978 |
The same way you'd convert any linear function between finite dimensional spaces to a matrix. Choose a basis for the input, i.e. $\vec x$, and a basis for the output, which will be a basis of bivectors, and evaluate the linear function for each basis vector and expand the result in the output basis.... (more) |
— | about 2 years ago |
| Comment | Post #285978 |
Say $\vec y = \mathbf e_1$ in a set of orthogonal basis vectors $\\{\mathbf e_i\\}_{i=1}^m$. While there are $m \choose 2$ basis bivectors, the only ones we care about are of the form $\mathbf e_1 \wedge \mathbf e_i$ for $i \neq 1$ (as $\mathbf e_1 \wedge \mathbf e_1 = 0$), so there are $m-1$ constra... (more) |
— | about 2 years ago |
| Comment | Post #285436 |
Topologies formulated as sets of open subsets are closed under (arbitrary) unions and *finite* intersections. Requiring countable intersections of open subsets to be open would break many standard examples of topologies. You also do need to explicitly include the total set as well. (If you were talki... (more) |
— | over 2 years ago |
| Comment | Post #285365 |
As has been mentioned to you before, you should inline relevant text rather than or in addition to using an image. Ideally, you should inline it so that there is no benefit to an image, but if you are really concerned about transcription errors or are unable to reproduce some notation, then including... (more) |
— | over 2 years ago |
| Comment | Post #285371 |
As it states and you can derive, $B > C$ is logically equivalent to $C = 2$ in this scenario. Thus the expressions $P(C > D \mid C = 2)$ and $P(C > D \mid C \neq 2)$ are the same as $P(C > D \mid B > C)$ and $P(C > D \mid B \not> C)$ respectively. If $C > D$ was independent of $B > C$, then these exp... (more) |
— | over 2 years ago |
| Comment | Post #284788 |
@#53922 Calling a question a "soft question" doesn't suddenly make it being overly broad, primarily opinion based, and/or lacking context or research okay. (more) |
— | over 2 years ago |
| Comment | Post #284718 |
Finally, there is some context which isn't *technically* required but omitting it sets up confusion down the line. First, most discussions of tensors by physicists are actually discussions of tensor *fields*. A tensor field is a continuous (and usually smooth) assignment of tensors to points on a man... (more) |
— | over 2 years ago |
| Comment | Post #284718 |
Slightly less objectively, your wording and notation compounded by your inconsistent use and unfortunate choices of notation confuse the issue significantly. A key part of this discussion is that all this co-/contra-variant stuff has to do with how we represent vectors (and tensors generally) *with r... (more) |
— | over 2 years ago |
| Comment | Post #284718 |
There are several issues here. First, you call everything a "vector". What the notation refers to are *tensors* and vectors are just the rank-1 case. Anything with other than 1 index is NOT a vector. Your description of the Einstein summation convention is completely wrong. It is not a convention to ... (more) |
— | over 2 years ago |
| Comment | Post #283900 |
I haven't downvoted (or upvoted) this meta answer, but I haven't yet completely decided how I feel. On the one hand, I think *in practice* there are indeed a lot of bad questions of the form discussed. On the other hand, I *am* making the case that there are often better answers than "experience, per... (more) |
— | over 2 years ago |
| Comment | Post #283900 |
It is also the case that the need for insight is often oversold. Many results about sums of binomial coefficients and closely related combinatorial identities have clever proofs involving insights and analogies. However, virtually all "textbook" identities of this form fall within the purview of [a d... (more) |
— | over 2 years ago |
| Comment | Post #283900 |
To give an example of the kind of thing I'm talking about, consider the following more positive rendition of the infinitude of primes: For any finite set of primes, there exists a prime not in that set. I can produce the following proof skeleton completely mechanically from the form of the propositio... (more) |
— | over 2 years ago |
| Comment | Post #283900 |
There is actually quite a bit that can be mechanized in proof finding. Up to and including completely deriving a proof mechanically. And I don't just mean that automatic theorem provers exist. A decent amount of a proof is highly constrained. In my experience, it is not uncommon for people to struggl... (more) |
— | over 2 years ago |
| Comment | Post #282900 |
While it's fine to self-answer a question, why are you answering it as if you weren't the person to ask it, e.g. saying "your answer isn't correct" and "you got it wrong"? There is no need to pretend like you are a third party who just happened upon this question. In fact, it's a bit confusing and bi... (more) |
— | almost 3 years ago |
| Comment | Post #282780 |
I am talking about definite integrals because integration by parts is usually discussed in that context, and the bounds are often important (and sometimes annoying but critical) in applications. Either way, the definite integral formulation is only *more* informative than an indefinite integral. The ... (more) |
— | almost 3 years ago |
| Comment | Post #282657 |
I would not want to be a moderator at this point but likely would be more open to it in the future. My concern is that even rough outlines of the policies we'd want here are not clear. My hope is that next time moderators are needed there's more guidance from the community on what they want out of mo... (more) |
— | almost 3 years ago |
| Comment | Post #282047 |
The bold statement is a sub-clause of a conditional statement that *explicitly assumes* that the players are rational. That real people aren't rational doesn't change what the theory predicts. It just means the theory isn't a particularly accurate model for humans. Either you are wondering, under the... (more) |
— | almost 3 years ago |
| Comment | Post #282046 |
Well, what probability do you assign to getting a red ball from urn B? If that differs from the probability of getting a white ball, why? If it doesn't, then the probabilities are the same in both cases. (more) |
— | almost 3 years ago |
| Comment | Post #281586 |
@Istiak Right now, the only real written thing that gives an *idea* for the scope is the discussion at the [Site Proposal | https://meta.codidact.com/posts/277002] but even this should be taken as a starting place. The policy for homework questions hasn't been set but is likely to be vaguely similar ... (more) |
— | almost 3 years ago |
| Comment | Post #280910 |
Are you right about what? That your expression "approximates" the integral? What criteria are you using to decide that something is an "approximation"? On what domain are you considering? (more) |
— | about 3 years ago |