[todo: Split the brief and the verbose exposition into two lenses.]

Formal logic makes our reasoning precise by providing formal systems in which to carry out reasoning. These systems are specified by a **proof theory** and often a corresponding **model theory**. Either of these theories will take many different forms and presentations, the important part is that they are rigorous and clearly defined.

Formal systems of logic are not concerned with the content of an argument, but only with the form.

For example, consider the following arguments.

$ \begin{array}{l} \text{If Socrates is a man, then Socrates is mortal.} \ \text{Socrates is a man.} \\hline \text{Therefore, Socrates is mortal.} \end{array} $

$ \begin{array}{l} \text{If the moon is ruled by the Mouse King, then the moon is made of cheese.} \ \text{The moon is ruled by the Mouse King.} \\hline \text{Therefore, the moon is made of cheese.} \end{array} $

Formal logic can not tell you that the latter argument is about non-sense. What it will tell you is about the form of the argument and whether that's valid and it so happens that both of these arguments "look" the same.

Let $~$S$~$ stand for "Socrates is a man", $~$O$~$ stand for "Socrates is mortal", $~$M$~$ stand for "the moon is ruled by the Mouse King", and $~$C$~$ for "the moon is made of cheese".

Then these arguments can be seen as follows.

$ \begin{array}{l} \text{If $~$S$~$ then $~$O$~$.} \ \text{$~$S$~$} \\hline \text{Therefore, $~$O$~$.} \end{array} $

$ \begin{array}{l} \text{If $~$M$~$ then $~$C$~$.} \ \text{$~$M$~$} \\hline \text{Therefore, $~$C$~$.} \end{array} $

This makes it apparent that the arguments proceed in the same way. Then if we introduce the symbol $~$\rightarrow$~$ to mean "If $~$A$~$, then $~$B$~$" in $~$A \rightarrow B$~$, and the symbol $~$\therefore$~$ for "therefore", the form if these arguments is written as

$ \begin{array}{l} A \rightarrow B \ A \\hline \therefore B \end{array} $