# Logical Reasoning
(under construction)
## Introduction
We will learn how the formal laws of logic can be helpul for informal reasoning.
We draw the running example from the theoretical part of the course, but the same method applies to any kind of reasoning, for example, to debugging code or finding out why some software fails to install properly on our machines.
Btw, if you remember questions from school about shapes, such as, "is every trapezoid a rectangle?", then what we are doing here is pursuing the same ideas in a more advanced setting.
## Learning Outcomes
...
## Examples
We have learned the following:
terminating implies normalising
An ARS has unique normal forms if (and only if) it is confluent and normalising.
If an ARS is confluent and terminating then all elements reduce to a unique normal form.
Let (𝐴,→) be a finitely branching ARS. The ARS is terminating if and only if there is a measure function 𝜙:𝐴→ℕ .
Let us abbreviate these statement to highlight their logical structure
T => NF
C & NF <=> UN
C & T => UN
FB => (T <=> MFN)
## Learning via Reasoning
We can combine the above ingredients to form many statements. How can we find out which are true and which are wrong?
The logical method is a two pronged approach.
- To use the laws of logic to derive new results from what we already knwo to be true.
- To find counterexamples for what we suspect might be wrong.
Let us take the two in turns.
## The Laws of Thought
This will not be a complete list or formal definition of the logic. Just a few rules that are helpful in everyday practice.
Some rules are best remembered as equations. The first group of equations can be remembered as "pushing negations inside"
$$ \neg(A \wedge B) \ = \ \neg A \vee \neg B
\quad\quad\quad
\neg(A \vee B) \ = \ \neg A \wedge \neg B$$
$$\neg(A\to B) \ = \ A \wedge\neg B
\quad\quad\quad
\quad\quad\quad
\neg\neg A \ = \ A
$$
Both $\wedge$ and $\vee$ satisfy the familiar laws of commutativity and associativity that we met earlier in the course when we discussed arithmetic. Also important are the distributive laws
$$ A\wedge (B\vee C) \ = \ (A\wedge B)\vee (A\wedge C)
\quad\quad\quad
A\vee (B\wedge C) \ = \ (A\vee B)\wedge (A\vee C)
$$
Note how similar these rules are to those of arithmetic when you take "$\wedge$" for "$\ast$" and "$\vee$" for "$+$" and "$\neg$" for unary "$-$".
The next group collects properties of implicaton, which is the most interesting connective.
$$A \to B \ = \ \neg B \to \neg A
\quad\quad\quad
A\to B \ = \ \neg A\vee B
$$
$$A\vee B\Rightarrow C \ \ = \ \ (A\Rightarrow C)\wedge (B\Rightarrow C)$$
$$A\Rightarrow B\wedge C \ \ = \ \ (A\Rightarrow B)\wedge (A\Rightarrow C)$$
With these equations you can calculate with propositions as you are used to calculate with number s from school. This is call Boolean algebra. The two important books by [George Boole](https://en.wikipedia.org/wiki/George_Boole) are [An Investigation of the Laws of Thought](http://www.gutenberg.org/files/15114/15114-pdf.pdf) from 1853 and [The Mathematical Analysis of Logic](http://www.gutenberg.org/files/36884/36884-pdf.pdf) from 1847.
These books are classics and well worth taking a look. For example, it is interesting to know that for Boole the study of logic and the study of probability were the same subject. Furthermore, he developed what is now called Boolean algebra explicitely as a logical simplification of Leibniz's and Newton's calculus. In particular, he makes clear that the difference between analysis and discrete mathematics rests ultimately on the laws
$$ A\wedge A \ = \ A
\quad\quad\quad
A\vee A \ = \ A
$$
which do not have an analogue in numbers.
**Remark:** These equations look quite different from the rules of Natural Deduction of Gentzen. But it can be shown that they are equivalent (ignoring Gentzen's rules for quantifiers which do not have an analouge in Boolean algebra).
## Finding Counter Examples
...
## Quiz
... a list of statements for you to find out which are true and which are false ... if they are true, argue how they follow from what you know ... if they are wrong, give a counterexample ...