Re: (*) -> 1

[Eduardo Ochs]

On Tue, 17 Jan 2023 at 15:05, Jean Louis <bugs@gnu.support> wrote:
> Ok it has been extended. That is your conclusion. But why? Show me the use.

Hi Jean,

note that we are discussing several different operations called `+'...
and sometimes to understand what a mathematical sentence "really
means" we have to add annotations to these operations with the same
name to distinguish them. The best explanation that I know about this
is in the pages 15-20 of these slides:

http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=15

When I had to explain "neutral elements" to my students a few months
ago I started by the operations "for all" and "exists". They
understood very quickly that for any proposition P(x) we had:

  ∀x∈{2,3,5}.P(x) = P(2)∧P(3)∧P(5)
  ∃x∈{2,3,5}.P(x) = P(2)∨P(3)∨P(5)

where "∧" is "and" and "∨" is "or", and these are the boolean "and"
and "or", that only accept inputs that are truth-values, and the only
truth-values are "true" and "false"... so these "∧" and "∨" are very
different from the "and" and "or" from Lisp.

Then at some point we started to meet expressions like these ones:

  ∀x∈{}.P(x)
  ∃x∈{}.P(x)

In a first moment the students didn't know how to interpret them. I
told them that this is one of the places in which mathematicians
_decide_ to extend a known operation, and in which they _choose_ an
extended definition that may look artificial at first - but they
choose a definition that turns out to be more well-behaved that the
other ones. For the "∀" we had (at least) these three possibilities:

  ∀x∈{}.P(x) = error
  ∀x∈{}.P(x) = false
  ∀x∈{}.P(x) = true

and I showed to them why the mathematicians had decided that this one

  ∀x∈{}.P(x) = true

would be the best choice. In my argument I used the figures that are here,

  http://angg.twu.net/LATEX/2022-2-C2-tudo.pdf#page=87

but these figures are not self-contained - I also talked a lot, wrote
lots of things on the whiteboard, and gesticulated a lot.

By the way, I started by "∀" and "∃" because I saw that it would be
better to start by them and then do "Σ" and "Π" later. See:

  https://en.wikipedia.org/wiki/Summation#Capital-sigma_notation

By the way: my main objective was to show to the students how
definitions work, and how in some cases some definitions can be
extended. "∀" and "∃" were just particular cases of this big idea, and
the big idea itself was more important than its particular cases.

  Cheers,
    Eduardo