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