Timeline for answer to What does the word "let" mean in mathematics? by Joe
Current License: CC BY-SA 4.0
Post Revisions
28 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 26 at 13:37 | comment | added | Daniel Schepler | One other use which could be added: Introducing a new notation for an expression to simplify things after that point. Example: "Let $\Delta = b^2 - 4ac$. Then if $\Delta < 0$ we have no real roots, if $\Delta = 0$ we have exactly one real root, and if $\Delta > 0$ we have exactly two real roots." Or, "Let $\Delta := b^2 - 4ac$..." for people like me who like to make the distinction between $=$ as an assertion about two expressions in previously existing variables and $:=$ for a new variable introduction. | |
| Mar 26 at 12:27 | history | edited | Joe | CC BY-SA 4.0 |
added 347 characters in body
|
| Aug 16, 2025 at 8:51 | audit | First answers | |||
| Aug 16, 2025 at 8:59 | |||||
| Jul 21, 2025 at 16:13 | comment | added | Pineapple Fish | Then to prove the $\forall x(\phi(x)\to\psi(x))$ part, you prove the more general statement by saying "Let $\phi(x)$ hold", proceeding to deduce $\psi(x)$, using the deduction theorem to get $\phi(x)\to\psi(x)$, and generalizing it. But notice that the use of the word "let" here is being used in the universal sense, although we seek to use this instance of it to prove a particular statement. So they are really not that different. | |
| Jul 21, 2025 at 16:13 | comment | added | Pineapple Fish | From these rules, we can figure out that if 1) $\exists x\phi(x)$ lies on a previous line in a proof and so does 2) $\forall x(\phi(x)\to\psi(x))$, then we will be able to write $\exists x\psi(x)$. This is how Hilbert systems navigate existential introduction without actually navigating it. Existential introduction requires proving existence. | |
| Jul 21, 2025 at 16:13 | comment | added | Pineapple Fish | @QiaochuYuan We can make a Hilbert system for logic with just 3 rules for quantifiers; if our axioms have only closed formulas, deduce $\forall x\phi(x)$ if $\phi(x)$ was proven at a previous step, the axiom $\forall x\phi(x)\to\phi^x_t$ for a term $t$, and, when $x$ is not free in $\psi$, $\forall x(\psi\vee\phi)\leftrightarrow\psi\vee\forall x(\phi)$. $\exists x\phi$ is an abbreviation of $\neg\forall x\neg\phi$. | |
| Jul 21, 2025 at 16:12 | comment | added | Brian Tung | This is a fantastic answer. I have no idea whether it's comprehensive (as in covering everything), but it's thoughtful and easy to read (at least I found it so), and it covers a lot of ground. Thanks! | |
| Jul 21, 2025 at 15:50 | history | edited | Joe | CC BY-SA 4.0 |
deleted 1 character in body
|
| Jul 21, 2025 at 15:17 | history | edited | Joe | CC BY-SA 4.0 |
deleted 27 characters in body
|
| Jul 21, 2025 at 13:28 | comment | added | Joe | @Stef: Yes, I agree that that usage which you speak of is more likely to fall under (1) or (2). | |
| Jul 21, 2025 at 13:28 | comment | added | Stef | @Joe, yes, but that's only for a proof by contradiction. My comment just stemmed from a momentary confusion on my part, between the three possible uses of Let. The "equation solving" I was thinking of didn't use existential instantiation at all, it was a straightforward "If x is a solution, then f(x) = 0, thus g(x) = 0, thus h(x) = 0, thus x \in (some very small list of solutions, possibly emtpy if there are no solutions)." which never really uses the fact that x "exists" | |
| Jul 21, 2025 at 13:24 | history | edited | Joe | CC BY-SA 4.0 |
deleted 30 characters in body
|
| Jul 21, 2025 at 13:22 | comment | added | Joe | @usul: I think that what you are talking about is related but I'm not sure it's quite the same thing. See my updated answer. (If you are still confused about something, I'd be happy to answer more questions.) | |
| Jul 21, 2025 at 13:14 | comment | added | Joe | @Stef: I think your comment had an element of truth in it: when proving that an equation has no solutions, sometimes we assume for contradiction that $\exists x \, \varphi$ (where $\varphi$ is some formula expressing the assertion that $x$ is a solution to an equation). Then, we are allowed to use $\varphi(c)$ (for some new variable $c$) in the natural deduction proof under the context of the assumption $\exists x \, \varphi$, before eventually showing that it indeed leads to a contradiction. | |
| Jul 21, 2025 at 13:12 | comment | added | Stef | @Joe, oops, indeed, of course | |
| Jul 21, 2025 at 13:08 | history | edited | Joe | CC BY-SA 4.0 |
deleted 5 characters in body
|
| Jul 21, 2025 at 0:33 | history | edited | Joe | CC BY-SA 4.0 |
added 248 characters in body
|
| Jul 20, 2025 at 22:51 | history | edited | Joe | CC BY-SA 4.0 |
added 4 characters in body
|
| Jul 20, 2025 at 21:09 | comment | added | Qiaochu Yuan | @Joe: your edited answer is great! That bit about the difference between Hilbert-style and natural deduction feels like a key piece of what I personally felt confused about here, thanks for clarifying it. | |
| Jul 20, 2025 at 21:09 | vote | accept | Qiaochu Yuan | ||
| Jul 20, 2025 at 20:44 | audit | First answers | |||
| Jul 20, 2025 at 20:56 | |||||
| Jul 20, 2025 at 19:20 | comment | added | Joe | @QiaochuYuan: Thanks, I've just updated my answer with some more details about introducing assumptions. I've found a little difficult to organise my thoughts on this matter, but hopefully by looking at how formal systems deal with this issue, this will shed some light on the meaning of "let" in everyday mathematics. | |
| Jul 20, 2025 at 19:15 | history | edited | Joe | CC BY-SA 4.0 |
added 3251 characters in body
|
| Jul 20, 2025 at 11:45 | comment | added | John Hughes |
I really like this answer. It contains most of what I tried to say, but with better precision because Joe seems to actually know some mathematical logic. :) I also really like the "third use" example. In Isabelle, at least, this is represented by the keyword obtain, as in obtain x where "x \in G /\ (prime x)" by ... which helps distinguish it from the translation of "for all" and "assume" (the first two uses).
|
|
| Jul 20, 2025 at 10:50 | comment | added | usul | @Joe is your comment getting at this? There's a distinction between "We already have a finite group; let us name it G", which happens in case (1), and "We have a thing named G, let it be a finite group (i.e. suppose it is a finite group)", which has to do with case (2). | |
| Jul 20, 2025 at 3:29 | comment | added | Qiaochu Yuan | Thanks for writing this! I like this answer overall and it's close to my own thoughts, and I agree that saying more about this whole "introduction an assumption" thing would be helpful. I don't think this is explained clearly in many places; I certainly never saw a clear explanation of this anywhere in my own mathematical education. | |
| Jul 20, 2025 at 0:40 | comment | added | Joe | Hmmm, I'm now thinking that my explanation in (2) is missing something. The point is that often in natural deduction systems, when we write "$G$ is a finite group", that is often indicated using square brackets to show that it is an assumption (and assumptions are marked as such so they can't be deduced as theorems). So, the usage of the word "let" is not purely expository; it's actually introducing an assumption. It's a bit late where I am now, but I'll see if I can edit this answer tomorrow. | |
| Jul 19, 2025 at 22:45 | history | answered | Joe | CC BY-SA 4.0 |