Timeline for How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 21, 2020 at 8:35 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 110 characters in body
|
| Aug 14, 2020 at 17:04 | comment | added | Andrej Bauer | Aha, ok. Point taken. I've had rather the opposite experience. Some of my colleagues seem to be more traditional than yours. | |
| Aug 14, 2020 at 16:57 | comment | added | probably_someone | @AndrejBauer I'm saying that they wouldn't object if you did so, unless the idea that the input of an integral is a differential form is relevant to what you're doing. | |
| Aug 14, 2020 at 16:56 | comment | added | Andrej Bauer | @probably_someone: What precisely are you saying? That your mathematician friends habitually write $\int (x \mapsto x^2 + 3 x)$? | |
| Aug 14, 2020 at 16:56 | comment | added | Andrej Bauer | @plop: I readily concur that there are many ways of viewing the integrals, and that $dx$ plays different roles in different situations. However, we are in the teritorry of pedagogy here. I picked a form of integral that is in direct analogy with the universal quantifiers in terms of higher-order functions. For the purposes of this answer it is much better to view it as a variable binder. | |
| Aug 14, 2020 at 15:48 | comment | added | probably_someone | None of the mathematicians I know would react the way you're saying. | |
| Aug 14, 2020 at 14:18 | comment | added | plop | "it[the integral] takes a function f as an argument" Not exactly. The integral takes in differential forms. The adherence to the $dx$ notation is not so much to keep a reminder of the quantified variable, even if it also serves that purpose, but to remind that the integrand pulls back (change of variable) as forms, not as functions. Right end goal in the explanation, but unfortunate example used as analogy. | |
| Aug 14, 2020 at 6:53 | vote | accept | TomR | ||
| Aug 14, 2020 at 6:47 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 433 characters in body
|
| Aug 14, 2020 at 6:41 | history | answered | Andrej Bauer | CC BY-SA 4.0 |