JAW114 preview

[Jeremy Weissmann]

Dear all,

   It would mean a lot to me if you had a look at the following preview of  JAW114 ,  Heuristics for a proof of Cantor's Theorem .   You can find the current version here:

     http://mathmeth.com/jaw/main/jaw1xx/jaw114.pdf     .

This note is based on one by Edsger Dijkstra and Jayadev Misra written in 1999, which you can find here:

     https://www.cs.utexas.edu/users/EWD/ewd12xx/EWD1294a.PDF

Let me know what you think!

   All best,

+j

[Lucas Brunno Luna]

Dear Jeremy,

I was aware of EWD1924a, but had not really read it until now; I liked the derivation presented in that paper, and I regard that your JAW114 as an improvement over it for me at least; I especially liked your introduction.

I think it worthwhile to mention that I find that proof very interesting on account of its use of the identity function to formulate the demonstrandum. In former days, if I would at all think about the introduction of a name such as "id" for said concept, I wouldn't know what relevance I should ascribe to it besides the option to rank it as "a waste of characters", as Dijkstra puts it in a response to possible objections to the introduction of the name "skip" for the empty statement. In connection with the later, he remarked that the decimal system was only possible thanks to the introduction of the character "0" for the concept of zero. I am increasingly coming to realize first-hand the value of such nomenclature for concepts such as an "empty number", an "empty command/function" (i.e. one that "leaves things as they are"), etc. and I believe that the presented proof for Cantor's theorem is a good example of the use of the identity function.

Of course, these concepts boil down to the notion of identities in general.

In connection with your conclusion, I think that the colors were a convenient device to help present your development; I don't object to their use if you feel like employing that device.

PS.: I do read those JAWs that you share through this group. My general opinion is that they are usually worthwhile for me to read, and I know that you would like to receive some feedback on them. The trouble is that I usually don't really have anything special to say, so I think it is perhaps better to just remain silent. =(

[Jeremy Weissmann]

I always appreciate feedback!

--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/f89dc84f-9c33-4e39-a9e1-ad8160dd978e%40googlegroups.com.

[Lucas Brunno Luna]

Haha, that's good to know. Just be aware that I still have a lot to learn, and reading what I could possibly have to say would perhaps not be worth the trouble. As they say: "It is better to remain silent at the risk of being thought a fool, than to talk and remove all doubt of it."

All the best!

Em segunda-feira, 25 de maio de 2020 16:15:05 UTC-3, Jeremy Weissmann escreveu:

I always appreciate feedback!

On Mon, May 25, 2020 at 3:11 PM Lucas Brunno Luna <lucasl...@hotmail.com> wrote:

Dear Jeremy,

I was aware of EWD1924a, but had not really read it until now; I liked the derivation presented in that paper, and I regard that your JAW114 as an improvement over it for me at least; I especially liked your introduction.

I think it worthwhile to mention that I find that proof very interesting on account of its use of the identity function to formulate the demonstrandum. In former days, if I would at all think about the introduction of a name such as "id" for said concept, I wouldn't know what relevance I should ascribe to it besides the option to rank it as "a waste of characters", as Dijkstra puts it in a response to possible objections to the introduction of the name "skip" for the empty statement. In connection with the later, he remarked that the decimal system was only possible thanks to the introduction of the character "0" for the concept of zero. I am increasingly coming to realize first-hand the value of such nomenclature for concepts such as an "empty number", an "empty command/function" (i.e. one that "leaves things as they are"), etc. and I believe that the presented proof for Cantor's theorem is a good example of the use of the identity function.

Of course, these concepts boil down to the notion of identities in general.

In connection with your conclusion, I think that the colors were a convenient device to help present your development; I don't object to their use if you feel like employing that device.

PS.: I do read those JAWs that you share through this group. My general opinion is that they are usually worthwhile for me to read, and I know that you would like to receive some feedback on them. The trouble is that I usually don't really have anything special to say, so I think it is perhaps better to just remain silent. =(

Em sábado, 23 de maio de 2020 22:03:59 UTC-3, Jeremy Weissmann escreveu:

Dear all,

   It would mean a lot to me if you had a look at the following preview of  JAW114 ,  Heuristics for a proof of Cantor's Theorem .   You can find the current version here:

     http://mathmeth.com/jaw/main/jaw1xx/jaw114.pdf     .

This note is based on one by Edsger Dijkstra and Jayadev Misra written in 1999, which you can find here:

     https://www.cs.utexas.edu/users/EWD/ewd12xx/EWD1294a.PDF

Let me know what you think!

   All best,

+j

--
You received this message because you are subscribed the mathmeth.com mailing list.

To unsubscribe from this group, send email to Calculational-Mathematics-unsub...@googlegroups.com

For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.

To unsubscribe from this group and stop receiving emails from it, send an email to calculational-mathematics+unsub...@googlegroups.com.

[Jeremy Weissmann]

No not at all.  Ask away and that's how we'll all learn.  In the Tuesday Afternoon Club one should be prepared to answer any question.  (But the asker should be prepared to answer, "Why did you ask that?" .)

+j

On Mon, May 25, 2020 at 3:22 PM Lucas Brunno Luna <lucasl...@hotmail.com> wrote:

Haha, that's good to know. Just be aware that I still have a lot to learn, and reading what I could possibly have to say would perhaps not be worth the trouble. As they say: "It is better to remain silent at the risk of being thought a fool, than to talk and remove all doubt of it."

All the best!

Em segunda-feira, 25 de maio de 2020 16:15:05 UTC-3, Jeremy Weissmann escreveu:

I always appreciate feedback!

On Mon, May 25, 2020 at 3:11 PM Lucas Brunno Luna <lucasl...@hotmail.com> wrote:

Dear Jeremy,

I was aware of EWD1924a, but had not really read it until now; I liked the derivation presented in that paper, and I regard that your JAW114 as an improvement over it for me at least; I especially liked your introduction.

I think it worthwhile to mention that I find that proof very interesting on account of its use of the identity function to formulate the demonstrandum. In former days, if I would at all think about the introduction of a name such as "id" for said concept, I wouldn't know what relevance I should ascribe to it besides the option to rank it as "a waste of characters", as Dijkstra puts it in a response to possible objections to the introduction of the name "skip" for the empty statement. In connection with the later, he remarked that the decimal system was only possible thanks to the introduction of the character "0" for the concept of zero. I am increasingly coming to realize first-hand the value of such nomenclature for concepts such as an "empty number", an "empty command/function" (i.e. one that "leaves things as they are"), etc. and I believe that the presented proof for Cantor's theorem is a good example of the use of the identity function.

Of course, these concepts boil down to the notion of identities in general.

In connection with your conclusion, I think that the colors were a convenient device to help present your development; I don't object to their use if you feel like employing that device.

PS.: I do read those JAWs that you share through this group. My general opinion is that they are usually worthwhile for me to read, and I know that you would like to receive some feedback on them. The trouble is that I usually don't really have anything special to say, so I think it is perhaps better to just remain silent. =(

Em sábado, 23 de maio de 2020 22:03:59 UTC-3, Jeremy Weissmann escreveu:

Dear all,

   It would mean a lot to me if you had a look at the following preview of  JAW114 ,  Heuristics for a proof of Cantor's Theorem .   You can find the current version here:

     http://mathmeth.com/jaw/main/jaw1xx/jaw114.pdf     .

This note is based on one by Edsger Dijkstra and Jayadev Misra written in 1999, which you can find here:

     https://www.cs.utexas.edu/users/EWD/ewd12xx/EWD1294a.PDF

Let me know what you think!

   All best,

+j

--
You received this message because you are subscribed the mathmeth.com mailing list.

To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com

For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.

To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/f89dc84f-9c33-4e39-a9e1-ad8160dd978e%40googlegroups.com.

--

You received this message because you are subscribed the mathmeth.com mailing list.

To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com

For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.

To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/e22c93d9-4fa2-4123-af81-3c3655ccebcc%40googlegroups.com.

[Musa]

Hello Jeremy,

+ Page 0, section “Nomenclature”, line 3.

  As far as I know, no one does this in practice and the purpose of

  Russell's work is to avoid it and the trouble it leads ---likewise for

  Type Theory and Category Theory, in general.

  I would advise removing that remark; unless you want to include a bit more

  cavets for the Axiom of Comprehension.

+ Page 0, “where ϕ does not depend on S”.

  It seems you're trying to be careful about your definitions and make

  the article accessible.

  Perhaps take care to explain the nature of the ϕ entity ;-)

  ( This is an important concercern, since ϕ is mentioned repeatedly in

  the article, without every being told what kind of thing it is. )

+ Page 1, “Dijkstra and Misra’s entire proof is determined by this

  first design decision, which I adopt here as well, without justification or

  motivation. ”

  This sentence does not instill confidence in the paper.

  There are a number of ways to define surjectivity of a function: Pointwise

  with ∀-∃ or by counting where points are set, or pointfree via cancellation or

  via a pre-inverse.  Indeed, “id = f ∘ g” read left-to-right says

  “every element y of the target is obtainable from f, as witnessed by g(y)”;

  whence “f is surjective”!

  ⇒ This is what you need on page 3: “(⋯S⋯) = g.S” ;-)

  Moreover, the remark on the Axiom of Choice is likely to be unhelpful.

  In Constructive Mathematics, the two formulations of surjectivity

  are equivalent **without** such an axiom ;-)

+ As hinted by the above three points, there seems to be a tendency to

  *both* cover Set Theory comprehensively yet make it accessible.

  Unfortunately, neither goal is met in full.

+ Page 2, “We can easily ∈ bring into the picture via the Axiom of Extensionality

  … Now we’ve bridged the first gap, but in doing so created an existential

  quantification rather than a universal one.”

  The axiom does *not* apply: It speaks of equalities, not discrepancies.

  In ‘applying it’, you actually invoked De Morgan's Law which led to the

  ∃-∀ issue you mention afterwards.

  The Curse of Knowledge …

All the best,

Musa

[Jeremy Weissmann]

Dear Musa,

   Thank you for this wonderful feedback!  It is all very thoughtful and astute, though I do not think I agree with it all.

+ Page 0, section “Nomenclature”, line 3.

  As far as I know, no one does this in practice and the purpose of

  Russell's work is to avoid it and the trouble it leads ---likewise for

  Type Theory and Category Theory, in general.

  I would advise removing that remark; unless you want to include a bit more

  cavets for the Axiom of Comprehension.

   Are you referring to mathematical objects being both sets and elements?  This is absolutely standard.  Perhaps, though, it would be more helpful if I mentioned more explicitly that we try to use lowercase letters for the lefthand argument of  ∈ ,  and uppercase ones for the righthand argument.  But in any case I'm not sure I understand your point.

 

+ Page 0, “where ϕ does not depend on S”.

  It seems you're trying to be careful about your definitions and make

  the article accessible.

  Perhaps take care to explain the nature of the ϕ entity ;-)

  ( This is an important concercern, since ϕ is mentioned repeatedly in

  the article, without every being told what kind of thing it is. )

   Yes, I should probably add that  φ(x)  is meant to represent the property of element  x  being used to define the set.  However, I will not go into detail about substitution, scope of quantifiers, etc.

 

+ Page 1, “Dijkstra and Misra’s entire proof is determined by this

  first design decision, which I adopt here as well, without justification or

  motivation. ”

  This sentence does not instill confidence in the paper.

   Why?  Please elaborate.  Every paper has a viewpoint, an approach.  Some things are beyond the scope of the paper, and maybe that's exactly the wording I should use.

 

  There are a number of ways to define surjectivity of a function: Pointwise

  with ∀-∃ or by counting where points are set, or pointfree via cancellation or

  via a pre-inverse.  Indeed, “id = f ∘ g” read left-to-right says

  “every element y of the target is obtainable from f, as witnessed by g(y)”;

  whence “f is surjective”!

  ⇒ This is what you need on page 3: “(⋯S⋯) = g.S” ;-)

   I don't believe that on page 3 I am using the surjectivity of  g ,  but maybe I misunderstand your comment.  Anyway, there are many equivalent formulations of surjectivity, I agree.  Dijkstra and Misra chose one particular formulation, and that is where this proof comes from.

 

  Moreover, the remark on the Axiom of Choice is likely to be unhelpful.

  In Constructive Mathematics, the two formulations of surjectivity

  are equivalent **without** such an axiom ;-)

   You'll have to elaborate on that.  My understanding was that in constructive mathematics, the two formulations are  NOT  equivalent.

+ As hinted by the above three points, there seems to be a tendency to

  *both* cover Set Theory comprehensively yet make it accessible.

  Unfortunately, neither goal is met in full.

   I would disagree with the word  'comprehensively' ,  but I think you are right that I may have not found the right balance.  It is a tightrope I knew I was walking.  The problem is that I really do want to use something like the Axiom of Comprehension as part of my design.  Perhaps I need to reformulate these properties without reference to traditional set-theoretic nomenclature.

+ Page 2, “We can easily ∈ bring into the picture via the Axiom of Extensionality

  … Now we’ve bridged the first gap, but in doing so created an existential

  quantification rather than a universal one.”

  The axiom does *not* apply: It speaks of equalities, not discrepancies.

  In ‘applying it’, you actually invoked De Morgan's Law which led to the

  ∃-∀ issue you mention afterwards.

  The Curse of Knowledge …

   Oh, now I think you are being too naive.  This is not a document on predicate calculus.  It's a document meant for people who have some familiarity with the calculational style, and who feel comfortable using contrapositives without much fuss.  That being said, it would not be any loss to point out that I am using the contrapositive.  (That is indeed what Dijkstra and Misra did in their published paper.)

   And no, I did not invoke De Morgan's Law.  You could use De Morgan's Law to explain how I arrived at my conclusion, but for me this falls under the heading of  "logical reasoning" .   The choice to name and justify logical reasoning is usually going to be outside the scope of any paper which is not specifically about predicate calculus.

* * *

   Looking forward to understanding more!

+j

[Lucas Brunno Luna]

Oh, yes, Musa's answer has reminded me that I found this sentence on page 0, viz. (emphasis mine)

We have the Axiom of Extensionality which states that equality of sets is equivalent to equality of their elements:

somewhat ambiguous, (i.e. initially I thought not that every element in some set X is equal to some element in some set Y and vice-versa, but what amounts to saying that both sets have at most one element because all elements are equal to each other) even though the formula that is introduced just after that makes clear what you mean. In any case, I think it's perhaps better to refrain from using a sentence like that.

[Jeremy Weissmann]

What you say is true except the scope of your quantification is wrong. But I agree that I’m not entirely satisfied with that phrasing so I will try a different one. 

On May 26, 2020, at 12:30, Lucas Brunno Luna <lucasl...@hotmail.com> wrote:



Oh, yes, Musa's answer has reminded me that I found this sentence on page 0, viz. (emphasis mine)

We have the Axiom of Extensionality which states that equality of sets is equivalent to equality of their elements:

somewhat ambiguous, (i.e. initially I thought not that every element in some set X is equal to some element in some set Y and vice-versa, but what amounts to saying that both sets have at most one element because all elements are equal to each other) even though the formula that is introduced just after that makes clear what you mean. In any case, I think it's perhaps better to refrain from using a sentence like that.

--

You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/8fef81d6-92b5-4af7-8a1d-9c219d505fdf%40googlegroups.com.