184 views

Skip to first unread message

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

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

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

Aug 25, 2020, 7:02:39 AM8/25/20

to Calculational Mathematics

Sorry, "The choice of postulates *in* D&S..."

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

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.

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

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.

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.

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

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

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.

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

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/b47f2396-c2e3-8ec4-c3bf-2c7d725c7abc%40t-online.de.

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

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/CAMdvELdm9hUokMi7gs0or-MeCJExyC6Fxd_Ax3hexK%3DAKk%2ByoA%40mail.gmail.com.

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.

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

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.

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.

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

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,

--

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.

Sep 7, 2020, 3:00:37 PM9/7/20

to calculationa...@googlegroups.com

Yes Henry, that is possible. Mail me your complete postaddress

Wim.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/9E1DCF76-396F-4AB6-8C01-4F9C9021FF77%40ucd.ie.

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

Fax +54 341 4802654

--------------------------------------------------------------------------------------

-------------------------------------------------------------------------------------

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)

Donde con toda seguridad encontrarás una mano que te ayude

será en el extremo de tu propio brazo.

Napoleón (1769 - 1821)

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/CADOuC4dPPZhVQr52t1cuiJ%3D4JUK8t8TT8y4-cGO4yaO2bwtbgw%40mail.gmail.com.

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

--

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/CABbWiraU0YyAMTsJAaEt%3D8Z%3Dtdo_TOrr9FoXf08zsMBSofNxZg%40mail.gmail.com.

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:

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/CADOuC4dPPZhVQr52t1cuiJ%3D4JUK8t8TT8y4-cGO4yaO2bwtbgw%40mail.gmail.com.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu