Inquiry about calculational math

191 views
Skip to first unread message

Florin Vasiliu

unread,
Aug 24, 2020, 4:00:04 AM8/24/20
to Calculational Mathematics
Dear all,

I return with a few questions concerning the calculational style; they've been occurring to me —an independent learner— for a while now, so I thought they could also be of interest to other visitors of this forum. (I apologize to Mr. Weissmann for not pursuing my previous thread further, as my elementary geometry texts were not written in English and I had wanted to study his JAW17 more carefully before replying.)

Could you please expound on the difference between a logic and an algebra? Especially with regard to the clash of perspectives expressed in EWD1227: for instance, how come the need for inference rules was rejected by Prof. Dijkstra, while Prof. Gries kept employing them (e.g., in his paper "Foundations for Calculational Logic"), even after circulation of the open letter? I can't grasp EWD's view here, since, in my current understanding, inference rules are the only syntactic means of deriving one theorem from another; are they somehow implicit in the algebra? Take a look as well at the third paragraph from:
cs.cornell.edu/gries/Logic/Calculationalhistory.html
I find it unsettling, since Dijkstra insisted on absolute (uninterpreted) formality.

Another issue of high interest to me would be a potential (brief) response to Egon Börger's critique of [DS90], also mentioned in EWD1227. Link:
pages.di.unipi.it/boerger/Papers/Miscellaneous/dijkstrareview.pdf
(As an aside, did the Eindhoven group really have no source of inspiration when developing the predicate calculus —some reference text on logic maybe? I couldn't find any.)

In connection with the above, although I understand and agree with Dijkstra's comment that axioms don't have to be "self-evident", I'd like to know what prompted the introduction of some of the laws in his predicate calculus. In particular, when quantification is involved, and truth tables provide no assurance, how can we be certain that the formal rules properly reflect our informal understanding and are hence fit for "applying to the real world"? (With apologies for bordering here on the philosophical facette.)

Thank you in advance for any help!
Regards,
Florin Vasiliu

Kevin

unread,
Aug 25, 2020, 7:00:48 AM8/25/20
to Calculational Mathematics
Hi Florin,

The paper 

' "Everywhere" in predicate algebra and modal logic '

by Rutger M. Dijkstra (Information Processing Letters 58 (1996) 237–243) may answer your questions about predicate algebra versus predicate logic (especially sections 1, 2, and 5). It certainly clarified things for me.

Though it has been many years since I read Borger's review, I can still recall my amazement at how spectacularly he seemed to have missed the point. (I can also recall Dijkstra's compact dismissal in EWD1227 of that review and agreeing with him.)

However, I think D&S confused matters by using the word "logic" in that book when they should not have done so. In that respect, I think G&S (ALATDM) have confused things even more...

The choice of postulates is D&S is, to a certain extent, arbitrary. EWD1123 gives a somewhat different set.

Regards,
Kevin

Kevin

unread,
Aug 25, 2020, 7:02:39 AM8/25/20
to Calculational Mathematics
Sorry, "The choice of postulates *in* D&S..."

Jeremy Weissmann

unread,
Aug 25, 2020, 10:58:12 AM8/25/20
to mathmeth
Hi Florin and everybody,

Could you please expound on the difference between a logic and an algebra? [...] for instance, how come the need for inference rules was rejected by Prof. Dijkstra, while Prof. Gries kept employing them (e.g., in his paper "Foundations for Calculational Logic"), even after circulation of the open letter? [...]

   What follows is a very unstructured, but hopefully understandable summary of my thoughts on the matter.  I apologize in advance for the lack of organization.

   There's no question that algebraic logic is correct, just as there's no question that traditional approaches to logic are correct.  In my opinion, they reflect totally different use cases.  I say this as someone who used to study mathematical logic, even as I used the  "algebraic"  approach in my writings — sometimes even in my writings about mathematical logic!

   When in logic we create something called an  "inference system" ,  we are creating a model of human reasoning which is fit for mathematical study.  Thus we specify certain  "axioms"  and  "inference rules" ,  define  "proof"  in terms of these, and then proceed to reason about what can be  "proved"  in this  "system" ,  or even about what cannot be  "proved" !   Logical systems are mathematical objects used to study (that is, 'abstractions of') axiomatic reasoning.

   Note that in the last sentences I used the words  'reason'  and  'reasoning' .   I didn't use the word  'proof'  because I didn't want to confuse semantic levels, but  'reasoning'  is what we mean by  'proof' ,  in a mathematical context.  It is no different from, in abstract algebra, where we might define the  "zero element"  of a ring, which we use to study/generalize the number  0  in the ring of integers.  Similarly,  'inference systems'  are abstractions of human reasoning we can use to study our own reasoning using mathematics.

   So, how do we carry out this reasoning?  We could use inference systems, but this is a Bad Idea.  Inference systems are intentionally defined in a minimalistic way, because they are not meant to be used — they are meant to be studied.  Gries and Scholten attempted to  "soup up"  their inference system to make it more  "user-friendly" ,  but I would still maintain that they used the wrong tool for the job.  (You can make the bottom of a screwdriver heavy and metallic and use it to drive nails into wood, but a hammer will be a better tool for the job because of how it enables the use of rotational force.)

   Mostly we carry out reasoning in natural language.  Natural language can be an incredibly powerful communication tool, but often it is simply not up to the task of dealing with highly abstract concepts related in highly specific, precise ways.  Thus, over the millenia, we invented symbolic representations of mathematical concepts, and over the last few centuries we developed algebraic systems: calculations with uninterpreted formulae.  All professional mathematicians (including logicians) use algebraic calculation to some extent in their proofs.  The algebraic approach was so powerful and wide-ranging that it even enabled us to mathematicize mathematical reasoning itself!  Mathematical logic simply could not have existed until we had already seen how mathematical reasoning could be synthesized into a symbolic form.

   What Dijkstra, Feijen, et al did was to apply calculation more broadly; to make calculational tools more streamlined, flexible, and powerful; and to show how calculational was not only a useful shorthand, but could also drive proof construction.  In this sense, though, they were just expanding on a very mathematical tradition.

   Make no mistake about it: symbolic reasoning still comprises only a small portion of human mathematical reasoning.  Dijkstra's writings are full of English words and explanations.  Gries and Scholten's inference system is defined using the English language.  Sure: within a particular framework, it's possible to state a theorem and prove it without any natural language reasoning, but in order to string those frameworks together to develop a theory, one needs natural language.  I would bet that the extinction of the human race would come way before any significant progress in turning all of human reasoning into symbols.  The reason is that symbolic reasoning reflects a deep understanding and great synthesis of ideas, understanding that takes centuries if not millennia to reach.  Humans did arithmetic for millennia before number systems were developed, and then even longer before algebra could be developed.  These early mathematicians were not dummies; they were great geniuses with an exceptional command of mathematical concepts.  They never could have imagined that these esoteric concepts could be so systematized that someday they could be taught to five-year-olds.

   But I digress.  So, it is not the case that Gries and Schneider's inference system is any more correct than the traditional mathematician's (or Dijkstra's) algebraic approach.  It is a human system designed in terms of human concepts, which makes it as susceptible to error as any other human-designed system.  And yet it is also exceptionally cumbersome and limited.  So, I see no real benefits to their system.

   I think there was a real misunderstanding between Dijkstra and Gries.  When Dijkstra mathematicized logic, it was because he felt  —as someone steeped in a great tradition of mathematics—  that it wasn't beneficial to merely algebraically manipulate  x  and  y  and integrals and so forth, but also to manipulate the structure of the arguments themselves, using predicate calculus.  As far as I can tell, Dijkstra had no interest in  "mathematical logic"  per se;  that is, he had no interest in designing systems to study reasoning and the limitations of reasoning.  Nevertheless, if he had, he surely would have used algebraic calculation to structure and streamline his arguments about mathematical logic — because that is what any professional mathematician would do.  And then, indeed, he would need to introduce more symbols and make more distinctions, because the study of mathematical logic would require it.  The *use* of mathematical logic, however, does not.

   A final point.  There is no human reasoning without  "postulates"  and  "inference rules" .   But by these terms I don't mean the mathematical ones; I mean the human concepts which the mathematical ones model.  A good example is the Law of Modus Ponens:  From  X  and  X => Y  we can conclude  Y .   On page  10  in  EWD1123 ,  Dijkstra proves a symbolic version of Modus Ponens, and even remarks that it no longer requires a special name.  Well, that may be true, but Dijkstra has already used the natural language version of Modus Ponens a dozen times by the time he gets to page  10 !     In his first calculation on page  6  there is a three-step calculation, where each step is equality.  He shows  A = B ,  B = C ,  and  C = D ,  and wants us to conclude  A = D .   Well, what is this but the law of Modus Ponens applied to the transitivity of equality, which states that  X = Y  and  Y = Z  implies  X = Z ?   I suppose one could avoid this problem by turning the transitivity of equality into a inference rule, but then we still have an inference rule.  Similar remarks can be made for the Law of Instantiation:  r.x /\ (Ay : r.y : t.y)  =>  t.x .   We can and should prove and use symbolic versions of the Law of Instantiation, but we simply cannot do mathematics without using this as an  "inference rule" .

   Gries and Scholten (and possibly other logicians) get things wrong when they think that their inference system is able to avoid this problem.  For they use Modus Ponens and the Law of Instantiation and other forms of logical reasoning to set up their inference system.

   To sum up:  Human reasoning uses certain agreed-upon principles of logic, and these cannot be dispensed with — they *are* the definition of human reasoning.  Symbols are used to simplify human reasoning to make it more powerful.  Mathematical logic is a system of symbols used to study human reasoning.

+j

 

Alwyn Goodloe

unread,
Aug 25, 2020, 11:59:49 AM8/25/20
to calculationa...@googlegroups.com
Jeremy, 

   Thanks for your explanation. I think you are correct that Dijkstra wasn't really interested in logic as practiced by logicans. I know Boyer and Moore at UT Austin were very interested in what Edsger was doing, even though they were really building theorem provers. 

   When his text was written Gries did explain how the text was basically developed for a particular discrete math course at Cornell. Curricula of such courses usually have to be agreed on by the faculty as a group.  I gather they abandoned teaching much logic in that course sometime ago and basically teach combinatorics, probability, etc as is standard in the US now.   While I agree with many of the critics of the Gries text, unfortunately I don't think anyone really wrote a better book for calculational logic undergraduates at least in English. 

   I agree with the discussion that the Dijkstra/Scholten  text can come off as a bit puzzling if you approach it from the perspective of studying logic. As you point out it is really algebraic logic. Halmos small book on algebraic logic was equally confusing if approached by someone thinking it was focusing on model theory or proof theory. 

   In some sense the Dijkstra/Scholten  book resembles a book on something like laplace transforms written for engineers. There are a lot of formulas to memorize and in doing so gives you tools to reason about a particular model of the physical world. Mathematicians often hate these sort of books  often dismissing them as too much memorization and too much calculation. On the other hand,texts like "little Ruden' and "big Ruden" are beloved by mathematicians, but not really helpful for an engineer trying to build a system. 

   I think the presentations  of calculational math in Ralph Back's recent books that are targeted at teachers is particularly effective.  I would love for him to take a shot at writing a discrete math book, but he seems very busy trying to help educated Finnish teachers and maybe that is really the best way to spread calculational math. 

--
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/CAMdvELf6EzSDR4xy79Rz-7eaVKFKytdwuWordadZdipJi7OYBg%40mail.gmail.com.


--
Alwyn E. Goodloe, Ph.D.
agoo...@gmail.com

Research Computer Engineer
NASA Langley Research Center

Jeremy Weissmann

unread,
Aug 25, 2020, 12:23:20 PM8/25/20
to mathmeth
Thanks, Alwyn.  Your summary of my email is a lot more coherent than my original email.
 
While I agree with many of the critics of the Gries text, unfortunately I don't think anyone really wrote a better book for calculational logic undergraduates at least in English. 

   Yes, unfortunately I never got around to doing a book like that myself.  I still hope to find the time someday.
 
   I agree with the discussion that the Dijkstra/Scholten  text can come off as a bit puzzling if you approach it from the perspective of studying logic. As you point out it is really algebraic logic. Halmos small book on algebraic logic was equally confusing if approached by someone thinking it was focusing on model theory or proof theory. 

   I hate to be pedantic, but since the point of my email is more or less about terminology, I should say that  Dijkstra/Scholten  is not really algebraic logic, either.  It is just algebra — that is, a symbolic-calculational approach to mathematics.  First, it is applied to the structure of mathematical arguments (logic, if you like), and later to predicate transformers.

   I'm being so pedantic because  "algebraic logic"  is part of logic; that is, the study of the power and limitations of reasoning systems.  We all use reasoning systems; we don't all study reasoning systems.  Dijkstra and Scholten were not studying reasoning systems; they were studying predicate transformer semantics.  They merely algebraized their reasoning system so as to use it more efficiently and effectively.

   (Hey, I think that last paragraph was maybe a succinct summary of my original email!)
 
   In some sense the Dijkstra/Scholten  book resembles a book on something like laplace transforms written for engineers. There are a lot of formulas to memorize and in doing so gives you tools to reason about a particular model of the physical world. Mathematicians often hate these sort of books  often dismissing them as too much memorization and too much calculation. On the other hand,texts like "little Ruden' and "big Ruden" are beloved by mathematicians, but not really helpful for an engineer trying to build a system. 

   That's a good analogy.  Although of course one doesn't have to memorize all of Dijkstra/Scholten.  The basic principles reduce quite nicely to a small handful of properties.
 
   I think the presentations  of calculational math in Ralph Back's recent books that are targeted at teachers is particularly effective.  I would love for him to take a shot at writing a discrete math book, but he seems very busy trying to help educated Finnish teachers and maybe that is really the best way to spread calculational math. 

   I haven't read his stuff in decades.  I'd love to have another look at it.

+j 

Florin Vasiliu

unread,
Aug 25, 2020, 12:36:06 PM8/25/20
to Calculational Mathematics
Thank you very much, Mr. Weissmann, for your comprehensive and highly informative answer! I hope as many members as possible see it: I certainly think it contains some crucial details, not easily found elsewhere. My observation for now:

Your remark that Dijkstra used MP informally way before proving its symbolic counterpart went straight to the heart of my problem (and the reason I slightly favour the GS approach); the question remains: why not push informal appeals to the transitivity of equivalence or modus ponens further away from the actual calculation? In the GS framework, everything needed to (also mechanically) check proofs is precisely specified, informality and usage of natural language being confined to the presentation/justification of the system. Isn't this closer to the goal that the —supposedly, strictly— formal artefacts we design involve only "mindless manipulation of symbols"? (I understand this is not always the way to do math; I'm referring to the instances when we choose to apply it.)

Not even the first step in the first proof of EWD1123 can be formally justified without giving the implication sign in Leibniz's Principle a sort of "meta" status, like that of the horizontal line from inference rules. I may be the exception here, but, as a beginner studying Dijkstra's notes and book, I was very confused by these implicit transitions between the formal, uninterpreted —as advocated— parts, and the intuitive, "extra-mathematical" use of some laws.

Thanks as well to Mr. Hely! I shall look into that article as soon as I get the chance.

Jeremy Weissmann

unread,
Aug 25, 2020, 1:54:27 PM8/25/20
to mathmeth
Dear Florin,

Your remark that Dijkstra used MP informally way before proving its symbolic counterpart went straight to the heart of my problem (and the reason I slightly favour the GS approach); the question remains: why not push informal appeals to the transitivity of equivalence or modus ponens further away from the actual calculation? In the GS framework, everything needed to (also mechanically) check proofs is precisely specified, informality and usage of natural language being confined to the presentation/justification of the system. Isn't this closer to the goal that the —supposedly, strictly— formal artefacts we design involve only "mindless manipulation of symbols"? (I understand this is not always the way to do math; I'm referring to the instances when we choose to apply it.)

   I think you are mistaken if you believe that Gries and Schneider do not also use Modus Ponens and the Law of Instantiation informally, both in setting up and in using their formal framework.  Anywhere in a math text you see the words  "if ... then"  or  "any" ,  these sorts of reasoning will be used.  The same could be said for, say, the symmetry of  'and' ,  which is used everywhere; and especially the weakening rule which from  "X and Y"  allows us to conclude  X .   (Of course, this last rule is essentially instantiation.)

   My point is that all reasoning and argumentation (except in very heavily contextualized situations) use natural language, as well as these days some sort of symbolic calculation.  If you want, you can even use an inference system which restricts your repertoire of moves to the bare minimum, or just beyond.  But to think that the minimalist approach of an inference system is somehow  "more correct"  than other approaches is a mystical belief.  Indeed, one of the first sorts of proofs one does in mathematical logic is to show the equivalence of proving power of a large set of axioms to a smaller (computable) one.

   [And, again, the reason one does this is not to make things more "precise" or "correct", but to simplify reasoning about that system's power and limitations.  It is not very different from the algebraic  "clean up"  we'd perform on an equation like  (x–3)² = 2(x + 4) ,  putting it in the form  x² – 8x + 1 = 0  before using other tools to try to find solutions in  x .]

 
Not even the first step in the first proof of EWD1123 can be formally justified without giving the implication sign in Leibniz's Principle a sort of "meta" status, like that of the horizontal line from inference rules. I may be the exception here, but, as a beginner studying Dijkstra's notes and book, I was very confused by these implicit transitions between the formal, uninterpreted —as advocated— parts, and the intuitive, "extra-mathematical" use of some laws.

   You misunderstand things when you write  "can be formally justified" .   Of course it is justified, and justifiable in many ways.  The step is absolutely correct.  Dijkstra is not trying to teach people reasoning from first principles; he is showing how formal calculi can be developed.

   Dijkstra et al were interested in using calculation wherever it can be beneficial, not only for simplifying equations as above, or solving integrals and what have you, but also (and especially) in clarifying the structure of arguments in any field.  Towards this end it is important to calculate not only with arithmetic concepts like  x  or  2  or  + ,  but also reasoning concepts like  'and'  or  'implies'  or  'for all' .   By translating his reasoning concepts into symbols, he created a system which helps immensely to simplify and even design mathematical arguments.  He also discovered ways of reasoning which would never be possible in natural language — just as it would be nearly unthinkable to do differential calculus in natural language alone, even though some simple principles of calculus were known before Leibniz and Newton.

   But none of this is about  "logic" ,  no more than any professional mathematician's work is about logic.  We all use logic; Dijkstra simply found a way to use it more efficiently.

   Maybe I should finish with an extraordinarily contrived, uncharitable example:  Suppose you are given two lines in the Cartesian plane, and for each you are given their slope (vertical change divided by horizontal change), along with the coordinate of their intersection with the vertical axis.  We would like to know where those lines intersect.  From pseudo-antiquity, there is a method: Take the difference of the slopes and the difference of the intersections with the vertical axis, in the same order.  Divide the latter by the former, and take the opposite sign of the result.  This is the horizontal component of the point of intersection.  We then find the vertical component by multiplying this number by either of the slopes, and then adding the corresponding intersection with the vertical axis.

   For example, suppose one line has slope  2  and intersection with the vertical axis  5 ,  while the other has slope  3  and intersection with the vertical axis  -3 .   The difference of the slope is  2 – 3 = -1  while the difference of the intersection points is  5 – (-3) = 8 .   We divide the latter by the former,  8/(-1) = -8 ,  and take the opposite of this to yield the horizontal coordinate of the point of intersection,  8 .   We then find the vertical coordinate by multiplying  8  by a slope,  2  say, to yield  16 ,  and add the corresponding intersection point,  5 ,  to yield  16 + 5 = 21 .   So the point of intersection is  (8,21) .

   Now, this method is correct.  But because it is carried out in English, there is a lot of room for error.  So what Gries and Scholten advocate is akin to setting up a tableau as follows:

  v_int 1 ___       slope 2 ___
– v_int 2 ___     - slope 1 ___
  diff    ___   ÷   diff    ___   =  h-coord ___

With a structure like this, we're much less likely to make mistakes.  It's clean and organized.  It's also highly limited, although one might imagine a whole system of tableaux that could expand this idea to other problems.

   What Dijkstra advocates is to model the lines with the equation  y = (slope)·x + (int) ,  and then solve the simultaneous system of equations.  Yes, it's further from the original method from antiquity, but the result is a flexible system that can be used to solve not only this problem but countless others besides.  And of course, Dijkstra's way is abstract so there are certainly ways to be confused.  But the system makes sense and is powerful and flexible, and that's what we want.

+j

Jeremy Weissmann

unread,
Aug 25, 2020, 4:16:56 PM8/25/20
to mathmeth
Oops.  It has been brought to my attention that I wrote  "Gries and Scholten"  several times when I meant to write  "Gries and Schneider" .  (Not every time, though!)

Sorry, Fred!

+j

Diethard Michaelis

unread,
Aug 25, 2020, 5:23:57 PM8/25/20
to calculationa...@googlegroups.com, Florin Vasiliu
Didn't have the time to read through all the discussion.
[But did see and dislike ugly nonsense like "mathematicians hate".]

Nevertheless felt I should / could add some literature
that was at a time very helpful for me:

(0) "On Calculational Proofs" (2002) by Vladimir Lifschitz
http://www.cs.utexas.edu/users/ai-lab?lif01b

This note is about the "calculational style" of presenting proofs
introduced by Dijkstra and Scholten and adopted in some books on
theoretical computer science. We define the concept of a calculation,
which is a formal counterpart of the idea of a calculational proof. The
definition is in terms of a new formalization DS of predicate logic. Any
proof tree in the system DS can be represented as a sequence of
calculations. This fact shows that any logically valid predicate formula
has a calculational proof.
http://www.cs.utexas.edu/users/vl/papers/calc.ps
or PDF at
https://www.sciencedirect.com/science/article/pii/S0168007201000598/pdf?md5=1b3c99c85a614877b83c1c3e1b47e809&pid=1-s2.0-S0168007201000598-main.pdf

(1) "Algebraic Logic" by Paul R. Halmos,
Chelsea Publishing, NY, 1962
Part One, Monadic Algebras
presents point-free existential (and universal) quantifiers
[the D&S book unfortunately fails to do so,
seems D&S had studied Tarski but never Halmos].

A more light weight version is
(2) "Logic as Algebra" by Paul Halmos and Steven Givant,
The Math. Assoc. of America, 1998

Diethard.


Jeremy Weissmann

unread,
Aug 25, 2020, 8:16:14 PM8/25/20
to mathmeth
Wow!  Reference (0) is very cool.  Thank you, Diethard.

+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.

Jorge Petrucio Viana

unread,
Aug 26, 2020, 11:41:53 AM8/26/20
to calculationa...@googlegroups.com
Hello!

Very good references provided by Diethard, indeed!

Just a small observation: (1) and (2) are about logic of monadic predicates, 
that is, they only encompass quantification in formulas generated from monadic
predicates, those of the form P (x). Thus, the interaction between quantifiers is 
somewhat limited. In order to have a full quantification, Halmos moved to the 
so-called polyadic algebras, but these have become much more complex 
(in a certain sense) than the cylindrical algebras of Tarski (and his collaborators).

best,
Petrucio

Diethard Michaelis

unread,
Aug 26, 2020, 4:30:28 PM8/26/20
to calculationa...@googlegroups.com, Jorge Petrucio Viana
Hi Petrucio

> Just a small observation: (1) and (2) are about logic of monadic
> predicates,
> that is, they only encompass quantification in formulas generated from
> monadic
> predicates, those of the form P (x).

NO! Monadic in Monadic Boolean Algebra has nothing to do
with monadic predicates / functions!
A Monadic Boolean Algebras is an arbitrary Boolean Algebra B
together with a mapping Q: B -> B called "quantifier"
subject to Halmos' quantifier axioms
(see https://en.wikipedia.org/wiki/Monadic_Boolean_algebra
if you don't have (1) or (2) at hand):

Q.true = true
Q.p => p
Q.(p /\ q) = Q.p /\ Q.q
Q.p \/ Q.q = Q.(p \/ Q.q)

This is the universal quantifier variant,
Halmos did it for existential quantifiers.
(All are properties of D&S everywhere / [], too.)

For most (all) calculational purposes we do not need
the polyadic / cylindrical stuff mentioned by Petrucio.
Especially for the D&S book these axioms nearly suffice
in order to replace the quantifiers by dummy-free ones.
And [] then becomes one of these quantifiers!
The only additional postulate we need is that
the quantifiers we will use must commute
and thus their composition is a quantifier, too.
For ordinary quantifiers with dummies this is a theorem.
Abstract monadic quantifiers, however, need not commute.
Plus we must deal with the range separately / differently
-- via trading range and term --
as Halmos quantifiers don't have / know about ranges.

Diethard.

Florin Vasiliu

unread,
Aug 30, 2020, 12:22:10 PM8/30/20
to Calculational Mathematics
My thanks to everyone who contributed to the discussion!
I too appreciate Mr. Michaelis's reading suggestions.
To Mr. Weissmann: I shall further reflect on your reply; it was again illuminating in most respects.

Wim Feijen

unread,
Sep 7, 2020, 2:27:34 PM9/7/20
to calculationa...@googlegroups.com

Dear All,  

   Dick (Netty's husband) is "cleaning" his house.  He asked me whether there would be people interested in some of the following books:

  • On a method of multi-programming (4 items)
  • Beauty is our business (1 item)
  • On the shape of mathematical arguments (Springer: 16 items)
  • On the shape of mathematical arguments (PhD thesis: 29 items).

If some of you are interested in getting one or more of these books, please send me an email mentioning which book(s) you would like to have.  And then I will contact each of you personally.  Best wishes,

Wim Feijen

Henry McLoughlin

unread,
Sep 7, 2020, 2:58:25 PM9/7/20
to calculationa...@googlegroups.com
Dear Wim,

I would love a copy of the PhD thesis “On the shape of mathematical arguments” if that were possible.

Best wishes,

Henry

Sent from my iPad

On 7 Sep 2020, at 19:27, Wim Feijen <w.h.j....@gmail.com> wrote:


--
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.

Wim Feijen

unread,
Sep 7, 2020, 3:00:37 PM9/7/20
to calculationa...@googlegroups.com
Yes Henry, that is possible.  Mail me your complete postaddress

Wim.

Natalia Colussi

unread,
Sep 7, 2020, 3:07:48 PM9/7/20
to calculationa...@googlegroups.com
Dear Wim,

I would like to have a copy of the PhD thesis “On the shape of mathematical arguments”  and  the book "On a method of multi-programming" if that were possible. But, if were not, any of the books will be great! I am so happy to have the opportunity to have a just a  copy of any of them.  Thank a lot! 
Natalia.

--
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/262C4108-2A17-4826-85C4-25C117905904%40gmail.com.


--
-------------------------------------------------------------------------------------
Lic. Natalia Colussi
-------------------------------------------------------------------------------------
Profesora Depto. de Ciencias de la Computación
Facultad de Cs. Exactas, Ingeniería y Agrimensura
Universidad Nacional de Rosario
Av. Pellegrini 250 Planta Baja 
2000SBT, Rosario, Santa Fe, Argentina
Tel +54 341 4802649 --int 141/230
--------------------------------------------------------------------------------------
-------------------------------------------------------------------------------------
Lo importante es no cesar de hacerse preguntas.
Albert Einstein

Donde con toda seguridad encontrarás una mano que te ayude
será en el extremo de tu propio brazo.
Napoleón (1769 - 1821)

Wim Feijen

unread,
Sep 7, 2020, 3:10:34 PM9/7/20
to calculationa...@googlegroups.com
Dear Natalia,

   Your choice can be fullfilled.  Please send me your complete postaddress.

Wim.

Anmol Paralkar

unread,
Sep 7, 2020, 3:19:49 PM9/7/20
to calculationa...@googlegroups.com
Dear Wim,

 If possible, please may I have a copy of her PhD thesis.

Thank you,
Anmol P. Paralkar

--

Wim Feijen

unread,
Sep 7, 2020, 3:21:37 PM9/7/20
to calculationa...@googlegroups.com
Yes Anmol, very well possible.  Please send me your complete postaddress.  Best wishes,

Wim.

Wim Feijen

unread,
Sep 8, 2020, 2:39:23 PM9/8/20
to calculationa...@googlegroups.com
Hi Natalia, both books are (still) available.  Now please send me you complete post address.  Best wishes,

Wim Feijen.

On 7 Sep 2020, at 21:07, Natalia Colussi <natalia...@gmail.com> wrote:

Reply all
Reply to author
Forward
0 new messages