Programming Languages (CS302 2005S)

Gries, Chapter 2

Gries, David (1998). The Science of Programming. New York, NY: Springer-Verlag. ISBN: 0-387-96480-0. Chapter 2: Reasoning Through Equivalence Transformations (pp. 19-27).



Is it possible to write code similar to the barber paradox that defies standard logic? Or is English not as strict as computer code and allows things code will not?

I really couldn't think of a question about the material. So a question about the class: Will we be dealing with other prepositional calculi (plural of calculus?), potentially one that can handle paradoxes?

In his discussion of the Excluded Middle Law Gries mentions that self-referential statements can possibly create paradoxes which violate the Law of Excluded Middle. He mentions that in the system we are using self-referential statements cannot be introduced. My question is are there situations within the realm of designing a programming language in which we would need to consider such statements and what type of problems can arise?

Formal Systems

The development of any formal system requires the definition of a set of axioms and Gries avoids doing that. 2.3.1 seems to imply that the 12 Laws on pages 20 and 21 are axioms but their interdepence rules that out as well.

Since this formal system for expressing propositions cannot express all our thoughts, what other systems are there?

Laws of Equivalence

Just like the law of contradiction which is proved from others, can we define the law of negation from the other 11 laws?

Gries defines 12 laws of equivalence in this chapter and 1-11 seem to be very useful. How is the 12th law (Law of Identity) useful to us?


Could you clarify what Gries means by inference rules in section 2.3?

In section 2.3, Gries separates the propositional calculus from the notion of a tautology.. "to emphasize the nature of this calculus as a formal system for manipulating propositions." I'm not really clear on the distinction.. it seems like just a different way of stating the Substitution and Transitivity rules.

Why does the proof of exercise 10 require use of conjunctive normal form? Why isn't it sufficient to say that a tautology is true in all states by definition and is therefore can be substituted for the value 'T'? I feel like I am missing some important subtlety.

Is the example, 2.2.3, an actual tautology proof or just an example or how to transform an implication into an easier to read format? It's not an actual tautology, is it?

Concerning the rules about inference, theorems, and axioms. What is the difference between an axiom and a theorem? One is inferred from a theorem, the other is derived from a theorem. Is there any actual difference other than the name (or other semantics)?

A more general question. Is this chapter implying that all our symbol manipulation within programs will be based on the 12 laws?

Regarding exercise 7 and 8, why would one care about disjunctive normal form and conjunctive normal form?

Disclaimer: I usually create these pages on the fly, which means that I rarely proofread them and they may contain bad grammar and incorrect details. It also means that I tend to update them regularly (see the history for more details). Feel free to contact me with any suggestions for changes.

This document was generated by Siteweaver on Wed Mar 2 11:39:32 2005.
The source to the document was last modified on Thu Feb 3 21:47:14 2005.
This document may be found at

You may wish to validate this document's HTML ; Valid CSS! ; Check with Bobby

Samuel A. Rebelsky,