Thread: Proof of distributivity theorem in the equational logic

Hi,

I've recently begun studying equational logic E, that outlined in Gries and Schneider's Logical Approach to Discrete math, and I'm working away proving each theorem in turn.

I've stumbled on theorem 3.45 (Distributivity of over ):

and theorem 3.46 (Distributivity of over ):

As usual, they can only be proven with theorems and axioms of a lower number, and truth tables aren't allowed. I keep starting off by going for axiom 3.35 (Golden rule): , to transform (in the case of 3.45 obviously) as my first step. Does anyone have any hints as to where to start? Am I headed in the right direction? How would anyone else prove these?

Thanks in advance!

Originally Posted by Stephen Shaw

I've recently begun studying equational logic E, that outlined in Gries and Schneider's Logical Approach to Discrete math, and I'm working away proving each theorem in turn.

I fear that we may not be able to help you. There may be one of the regulars who may know that particular textbook. The way the question is asked, it is absolutely necessary to have that exact edition of the textbook. I have never even seen a reference to it.

Hmm. I was of the impression that E was quite a well-known logic :-(

Even if people don't know exact theorem numbers, is there any formulaic manipulation that they would do to show that the LHS equals the RHS? I'd quite like to be able to work formally it start-to-finish by myself, but I'm just trying to take some step in the right direction!

Originally Posted by Stephen Shaw

Hmm. I was of the impression that E was quite a well-known logic.

So far as I know, it is not. But I am in the USA.
I will say that I am a bit suspect of a text that does not use truth-tables for these simple properties. They must be developed is a sequence of definitions and axioms. We don’t have them.

Well obviously the fundamental axioms have to be proven by truth tables, and it would be a trivial task to prove the above theorems by truth table. But that's not the point of the exercise. The idea is to formulate theorems from other theorems without explicitly evaluating their truth values, to foster skills in formal symbol manipulation.

I found this book in Google Books. While propositional logic is completely standard, calling it "equational logic" is uncommon. Their axioms are equally eccentric, in particular in treating equivalence as associative. In general, their rewriting approach is a little too algebraic to the detriment of presenting logic as the study of the laws of reasoning. So if I didn't know how to prove some theorem in this particular version of propositional calculus, I wouldn't be too upset.

There is an interesting question why formal logic is taught in discrete mathematics courses at all. I support teaching Boolean logic because, for example, it won't be good if a programmer cannot quickly prove the equivalence of two tests, even though he/she is reasonable smart and understands logical operations in principle. However, it has long been not clear to me how the study of formal proofs, with all those in-house bookworm overly syntactic ways of manipulating strings of characters helps with the development of either mathematical maturity or appreciation of usefulness of logic. Teaching typical Boolean-algebra, rewriting inference rules that are advocated by the book in question may not produce much in this respect. It may not be more effective that teaching any mathematical topic at all. Working through any mathematical subject will implicitly teach students proper laws of reasoning, which is probably the greatest benefit of such courses for future programmers.

However, I believe that teaching formal proofs may have benefit if it is done right. For this, one has to forget about the relation between inference rules and truth tables for a moment. Each of the connectives , , and has to be considered separately, in terms of what it takes to prove a formula with this connective and how such formula can be used to prove others. Under this view, the laws that allow expressing one connective via another, like De Morgan laws, suddenly become non-obvious, and indeed, they cannot be proved without the law of excluded middle, which is a completely different beast by itself. In fact, the first propositional axiom of the book, , is false under this interpretation. Only then can it be seen that there is a clear connection between proofs and programs, in fact, that proofs are programs. Therefore, teaching formal logic is nothing different from teaching programming. I am wondering if students would be more excited about learning formal proofs if they understood this.

This approach to logic (not so much to teaching) is not my own position. It is a well-known and often taught subject (see, e.g., this course and especially this text).