%% LyX 1.3 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[american]{amsbook}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\setcounter{secnumdepth}{4}
\setlength\parskip{\smallskipamount}
\setlength\parindent{0pt}
\usepackage{amssymb}

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 \numberwithin{section}{chapter}
 \theoremstyle{plain}    
 \newtheorem{thm}{Theorem}[section]
 \numberwithin{equation}{section} %% Comment out for sequentially-numbered
 \numberwithin{figure}{section} %% Comment out for sequentially-numbered
 \theoremstyle{definition}
 \newtheorem*{defn*}{Définition}
 \theoremstyle{definition}
  \newtheorem{problem}[thm]{Problem}
 \theoremstyle{plain}    
 \newtheorem*{thm*}{Théorème} 
 \theoremstyle{definition}
  \newtheorem*{example*}{Exemple}
 \theoremstyle{remark}    
 \newtheorem{notation}[thm]{Notation} 
 \theoremstyle{remark}
 \newtheorem*{rem*}{Remarque}
 \theoremstyle{definition}
  \newtheorem{xca}{Exercice}
 \newenvironment{lyxcode}
   {\begin{list}{}{
     \setlength{\rightmargin}{\leftmargin}
     \setlength{\listparindent}{0pt}% needed for AMS classes
     \raggedright
     \setlength{\itemsep}{0pt}
     \setlength{\parsep}{0pt}
     \normalfont\ttfamily}%
    \item[]}
   {\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathbb{C}}
\usepackage{hyperref}

\usepackage[francais,american]{babel}
\makeatother
\begin{document}

\newcommand{\Imp}{\textrm{ }\rightarrow\textrm{ }}

\newcommand{\Equiv}{\textrm{ }\Leftrightarrow\textrm{ }}
 
\newcommand{\s}{\textrm{ }}



\chapter{Propositional Logic}


\section{Introduction}


\subsection{What is a proof ?}

\begin{defn*}
A \emph{proof} is a piece of text written by a human to convince another
human that some fact is true.
\end{defn*}
\begin{problem}
\cite[p.~2]{Gersting.MSCS}

You have been selected to serve on jury duty for a criminal case.
The attorney for the defense argues as follow:

{}``If my client is guilty, then the knife was in the drawer. Either
the knife was not in the drawer, or Jason Pritchard saw the knife.
If the knife was not there on October 10, it follows that Jason Pritchard
did not see the knife. Furthermore, if the knife was there on October
10, then the knife was in the drawer and also the hammer was in the
barn. But we all know that the hammer was not in the barn. Therefore,
ladies and gentlemen of the jury, my client is innocent.''
\end{problem}
Are you convinced ?

Problems:

\begin{itemize}
\item What is the goal ?
\item What are the hypothesis ?
\item What is the logical link between the statements ?
\item There is plenty of unrelevant information.
\end{itemize}
A good proof consists of:

\begin{itemize}
\item A description of the goal
\item Hypothesis
\item Statements, one after the other. \\
Each one derives logically from the previous ones.
\item Conclusion
\end{itemize}
Let's look at a very simple example:

\begin{thm*}
Let $x$ and $y$ be two integers.

If $x$ is odd and $y$ is odd, then $xy$ is odd.
\end{thm*}
\begin{proof}
Assume $x$ is odd and $y$ is odd.

Let $k$ be an integer such that $x=2k+1$.

Let $l$ be an integer such that $y=2l+1$.

Then, $xy=(2k+1)(2l+1)=2(2kl+k+l)+1$.

Note that $2kl+k+l$ is an integer.

Conclusion: $xy$ is odd.
\end{proof}

\subsection{Formal and Informal proofs}

What do we mean by {}``derives logically from the previous ones''
?

What operations shall we consider as legal ?

To learn more about this, we need a \emph{model} of what we intuitively
consider as true, or \emph{logic}.

This model we are going to construct is called \emph{formal logic}.


\subsubsection{Formal systems}

\begin{defn*}
A \emph{formal system} is build by providing:
\begin{itemize}
\item a set of strings: the \emph{axioms}
\item a set of rewriting rules
\end{itemize}
A string that can be obtained from the axioms by applying rewriting
rules is called a \emph{theorem} of the formal system.

The \emph{proof} of a theorem is a description of the axioms and rules
used to get the theorem.

The set of all theorems is called the \emph{language} defined by the
formal system.
\end{defn*}
\begin{example*}
The MIU formal system\cite{Hofstadter.GEB}
\end{example*}
A formal system does not need to have any \emph{meaning} or \emph{semantic}.
It's pure syntax.

We will build formal logic as a formal system, with a meaning!

\begin{itemize}
\item The strings will be logic formulas
\item The axioms will be simple logic formulas that we interpret intuitively
true
\item The rewriting rules will be transformations we interpret intuitively
as valid
\end{itemize}
Then, any theorem of this formal system shall be interpreted as true.

We will have to be very careful with the choice of the axioms and
rules!


\subsubsection{Proofs and programming}

Writing a proof and a writing a program are very similar:

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|}
\hline 
Proofs&
Programming&
Purpose\tabularnewline
\hline
\hline 
Theorem&
Function prototype&
How to use it\tabularnewline
\hline 
Proof&
Function definition&
How it works\tabularnewline
\hline 
Intuitive proof&
Comments&
Explanation for the reader\tabularnewline
\hline 
Informal proof&
Program in a high level language &
Human readable\tabularnewline
\hline
Formal proof&
Program in assembly language&
Machine readable\tabularnewline
\hline
Checking an informal proof&
Compiling&
Human readable -> Machine readable\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

This comparison is not gratuitous. There are deep links between proofs
and programming which have been studied a lot in the last decades.
This is called the Curry-Howard correspondence.


\section{Statements, Symbolic Representation, and Tautologies}

As a first step, let's define logic formulas and their interpretation.


\subsection{Statements and Propositions}

\begin{defn*}
A \emph{statement} (or \emph{proposition}) is a sentence which is
either true or false.
\end{defn*}
\begin{example*}
Which sentences below are statements ?
\begin{itemize}
\item The sky is cloudy
\item It's raining
\item Are you happy ?
\item He is happy
\item Three divides five
\item There are life forms on other planets in the universe
\end{itemize}
\end{example*}
\begin{notation}
$A$, $B$, $C$: symbols representing a statement.

Each of those symbols can be given a truth value, either True (T for
short) or False (F for short).

$1$ is a statement if truth value True.

$0$ is a statement if truth value False.
\end{notation}

\subsection{Connectives}

How can we combine two statements ?


\subsubsection{And (conjunction), or (disjunction)}

\begin{example*}
{}``The sky is cloudy'': $A$. {}``It's raining'': $B$.
\begin{itemize}
\item {}``The sky is cloudy AND it's raining'': $A\wedge B$
\item {}``The sky is cloudy OR it's raining'': $A\vee B$
\end{itemize}
\end{example*}
\begin{defn*}
The \emph{truth table} of a formula describes when it's true or not,
given the truth value of the symbols.

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|c|}
\hline 
$A$&
$B$&
$A\wedge B$&
$A\vee B$\tabularnewline
\hline
\hline 
T&
T&
&
\tabularnewline
\hline 
T&
F&
&
\tabularnewline
\hline 
F&
T&
&
\tabularnewline
\hline 
F&
F&
&
\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

\end{defn*}

\subsubsection{Exclusive or}

\begin{example*}
{}``Cheese or desert''

You get cheese: $A$

You get desert: $B$
\end{example*}
\begin{defn*}
$A$ exclusive or $B$: $A\textrm{ xor }B$.

Truth table:

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|}
\hline 
$A$&
$B$&
$A\textrm{ xor }B$\tabularnewline
\hline
\hline 
T&
T&
\tabularnewline
\hline 
T&
F&
\tabularnewline
\hline 
F&
T&
\tabularnewline
\hline 
F&
F&
\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

\end{defn*}

\subsubsection{Implication}

\begin{example*}
{}``If I get my driver license, I will open a bottle of champagne''.

{}``I get my driver license'': $A$.

{}``I open a bottle of champagne'': $B$.
\end{example*}
\begin{defn*}
$A$ \emph{implies} $B$: $A\rightarrow B$.

Truth table:

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|}
\hline 
$A$&
$B$&
$A\rightarrow B$\tabularnewline
\hline
\hline 
T&
T&
\tabularnewline
\hline 
T&
F&
\tabularnewline
\hline 
F&
T&
\tabularnewline
\hline 
F&
F&
\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

\end{defn*}
Why this should be true:

\begin{itemize}
\item no real meaning but we have to pickup one to make it easy
\item Most reasonable is true
\end{itemize}
Why this should be false:

This one can be tricky. To help you make up your mind, here are some
examples:

\begin{itemize}
\item If I don't get my driver license, but still I open a bottle of champagne,
am I a liar?
\item {}``If I open a bottle of champagne, I will get my driver license''
\item {}``When pig flies, I'll give you 2 billions dollars''
\end{itemize}
Well, as strange as it can sound, $F\rightarrow T$ is a true formula.

If you start from an utterly false hypothesis, you can prove anything.

{}``Avec des si, on pourrait mettre Paris en bouteille''

{}``With ifs, Paris could be put in a bottle''

\begin{rem*}
$A\rightarrow B$ and $B\rightarrow A$ are not the same!
\end{rem*}
Sounds stupid ? 

Look carefully around you! This is the most common logic error in
peoples argumentations. 

And it's not always an involuntary error.

\begin{xca}
Give the antecedent and the consequent in the following sentences
\begin{itemize}
\item If the rain continues, then the river will flood
\item A sufficient condition for network failure is that the central switch
goes down
\item It's raining only if there are clouds in the sky
\item It's raining if there are clouds in the sky
\item It's raining if and only if there are clouds in the sky
\item The avocados are ripe only if they are dark and soft
\item A good diet is a necessary condition for a healthy cat
\end{itemize}
\end{xca}

\subsubsection{Equivalence}

\begin{example*}
The knight will win if and only if his armor is strong

The knight will win: $A$.

His armor is strong: $B$.

This sentence contains two informations: 
\begin{itemize}
\item The knight will win if his armor is strong: $A\leftarrow B$.
\item The knight will win only if his armor is strong: $A\rightarrow B$.
\end{itemize}
\end{example*}
\begin{defn*}
$A$ \emph{is equivalent to} $B$: $A\leftrightarrow B$.

Truth table:

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|}
\hline 
$A$&
$B$&
$A\leftrightarrow B$\tabularnewline
\hline
\hline 
T&
T&
\tabularnewline
\hline 
T&
F&
\tabularnewline
\hline 
F&
T&
\tabularnewline
\hline 
F&
F&
\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

\end{defn*}

\subsubsection{Not}

So far we defined binary connectives, that is connectives which took
two arguments.

Here is now a unary connective, taking just one argument.

\begin{example*}
It will not rain tomorrow

The knight will win: $A$.

His armor is strong: $B$.

This sentence contains two informations: 
\begin{itemize}
\item The knight will win if his armor is strong: $A\leftarrow B$.
\item The knight will win only if his armor is strong: $A\rightarrow B$.
\end{itemize}
\end{example*}
\begin{defn*}
not $A$: $A'$ (more usual notation: $\neg A$)

Truth table:

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|}
\hline 
$A$&
$A'$\tabularnewline
\hline
\hline 
T&
\tabularnewline
\hline 
F&
\tabularnewline
\hline
\end{tabular}\end{center}

\end{defn*}

\subsection{Complex Well Formed Formulas}

\begin{defn*}
A \emph{formula} is a string of 
\begin{itemize}
\item symbols: $A$, $B$, \ldots{}
\item connectives: $\vee$, $\wedge$, $\rightarrow$, $\leftarrow$ , $'$
, \ldots{}
\item parenthesis: $($, $)$, $[$, $]$
\end{itemize}
A \emph{well formed formula} (or wff) is a formula which satisfies
certain syntax rules.
\end{defn*}
\begin{notation}
Symbols representing wff: $P$, $Q$, $R$.
\end{notation}

\subsubsection{Order of precedence}

The formula $A\wedge B\rightarrow C'$ is ambiguous. It can be read
as:

\begin{itemize}
\item $(A\wedge B)\rightarrow(C')$, 
\item $A\wedge[B\rightarrow(C')]$, 
\item $[(A\wedge B)\rightarrow C]'$ 
\end{itemize}
Solution 1: always put all parenthesis (not very readable).

Solution 2: put an order of precedence between the operators:

\begin{enumerate}
\item Connectives within parentheses, innermost parenthesis first
\item $'$
\item $\wedge$, $\vee$
\item $\rightarrow$, $\leftarrow$
\item $\leftrightarrow$
\end{enumerate}
With this order of preference, $A\wedge B\rightarrow C'$ unambiguously
refer to $(A\wedge B)\rightarrow(C)'$.


\subsubsection{Evaluation of a wff}

From the truth values of the basic statements, and the elementary
truth tables, one can \emph{evaluate} the truth value of a wff.

\begin{example*}
$A\wedge B\rightarrow C'$, with $A$ true, $B$ false and $C$ true:

$A\wedge B$: false

$C'$: false

$A\wedge B\rightarrow C'$: true
\end{example*}
There is a recursive algorithm to compute the evaluation of a wff.


\subsubsection{Truth table of a wff}

This yields an algorithm for computing the truth table of a wff.

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|c|c|c|}
\hline 
$A$&
$B$&
$C$&
$A\wedge B$&
$C'$&
$(A\wedge B)\rightarrow(C')$\tabularnewline
\hline
\hline 
T&
T&
T&
&
&
\tabularnewline
\hline 
T&
T&
F&
&
&
\tabularnewline
\hline 
T&
F&
T&
&
&
\tabularnewline
\hline 
T&
F&
F&
&
&
\tabularnewline
\hline 
F&
T&
T&
&
&
\tabularnewline
\hline 
F&
T&
F&
&
&
\tabularnewline
\hline 
F&
F&
T&
&
&
\tabularnewline
\hline 
F&
F&
F&
&
&
\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

\begin{problem}
What's the size of a truth table?
\end{problem}
%

\begin{problem}
Can any truth table be obtained by a wff?
\end{problem}

\subsection{Tautologies and Contradictions}

\begin{defn*}
A \emph{tautology} is a statement that is always true.

A c\emph{ontradiction} is a statement that is always false.
\end{defn*}
\begin{example*}
$A\vee A'$

{}``Today the sun shine or today the sun does not shine''.
\end{example*}
\begin{xca}
Are the following wff tautologies or contradictions ?
\begin{enumerate}
\item $A\wedge A'$
\item $A\leftrightarrow A$
\item $(A\wedge B)\leftrightarrow(B\wedge A)$
\item $(A\wedge B)\rightarrow A$
\end{enumerate}
\end{xca}
Algorithm to check for a tautology?

Compute the truth table!

It's slow ($2^{n}$, where $n$ is the number of propositions), but
it works.

For certain simple forms of propositions, there is a much faster algorithm
(see \cite[Tautology test, p.~13]{Gersting.MSCS}).

\begin{example*}
Is $[(A\wedge B\rightarrow C')\wedge(E\leftarrow D)]\leftrightarrow[(E\leftarrow D)\wedge(A\wedge B\rightarrow C')]$
a tautology ?

Let $P:=(A\wedge B\rightarrow C')$ and $Q:=(E\leftarrow D)$.

The formula above is $[P\wedge Q]\leftrightarrow[Q\wedge P]$.

Let's prove it's a tautology.

Take some truth values for $A$, $B$, $C$, $D$, $E$. 

$P$ and $Q$ will then have some truth value.

But we know that $(A\wedge B)\leftrightarrow(B\wedge A)$ is a tautology.

So $[P\wedge Q]\leftrightarrow[Q\wedge P]$ will be true!

We don't actually need to compute the truth table of $P$ and $Q$.
\end{example*}
\begin{rem*}
Whenever you have some tautology, if you replace ALL occurrences of
some basic statement (say $A$) by a more complicated wff, you still
get a tautology.
\end{rem*}

\subsection{Equivalence of wff}

Let $P$ and $Q$ be two wff, and suppose $P\leftrightarrow Q$ is
a tautology.

Then $P$ and $Q$ have the same truth table.

\begin{defn*}
$P$ and $Q$ are \emph{equivalent} (noted $P\Equiv Q$) if they have
the same truth table.
\end{defn*}
\begin{rem*}
Writing $P\leftrightarrow Q$ or $P\Equiv Q$ is different.

In the first case, you just represent a formula, which can be true
or false.

In the second case, you claim that the wff $P\leftrightarrow Q$ is
a tautology.
\end{rem*}

\subsubsection{Basic equivalent wff}

What is the negation of {}``Peter is tall and thin'' ?

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|}
\hline 
Identity (id)&
$A\vee0\Equiv A$\tabularnewline
&
$A\wedge1\Equiv A$\tabularnewline
\hline 
Complement (comp)&
$A\vee A'\Equiv1$\tabularnewline
&
$A\wedge A'\Equiv0$\tabularnewline
\hline 
Commutativity (comm)&
$A\vee B\Equiv B\vee A$\tabularnewline
&
$A\wedge B\Equiv B\wedge A$\tabularnewline
\hline 
Associativity (ass)&
$(A\vee B)\vee C\Equiv A\vee(B\vee C)\Equiv A\vee B\vee C$\tabularnewline
&
$(A\wedge B)\wedge C\Equiv A\wedge(B\wedge C)\Equiv A\wedge B\wedge C$\tabularnewline
\hline 
Distributivity (dist)&
$A\vee(B\wedge C)\Equiv(A\vee B)\wedge(A\vee C)$\tabularnewline
&
$A\wedge(B\vee C)\Equiv(A\wedge B)\vee(A\wedge C)$\tabularnewline
\hline 
Double negation (dn)&
$A''\Equiv A$\tabularnewline
\hline 
De Morgan's Law (dm)&
$(A\vee B)'\Equiv A'\wedge B'$\tabularnewline
&
$(A\wedge B)'\Equiv A'\vee B'$\tabularnewline
\hline 
Implication (imp)&
$A'\vee B\Equiv A\rightarrow B$\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

\begin{rem*}
Notice the duality between $\vee$ and $\wedge$. 

Unlike $+$ and $\cdot$ they play a perfectly symmetric role in all
formulas.
\end{rem*}

\subsubsection{More equivalent wff using substitution}

\begin{example*}
$(A\wedge B)\wedge1\Equiv(A\wedge B)$.
\end{example*}
\begin{rem*}
Let $P$ and $Q$ be equivalent wff.

If you replace all occurrences of some basic statement by another
wff, you still get two equivalent wff's.
\end{rem*}
\begin{example*}
$A\wedge(B\vee C)\Equiv A\wedge(C\vee B)$
\end{example*}
\begin{rem*}
Let $P$ and $Q$ be equivalent wff.

If $P$ appears \emph{exactly} as a subformula of a bigger wff, then
you can substitute $P$ by $Q$ and get an equivalent wff.
\end{rem*}

\subsubsection{What's the point ?}

Rewriting a formula to simplify it:

\begin{xca}
\cite[Example 7 p.12]{Gersting.MSCS}
\begin{lyxcode}
If~((outflow~>~inflow)~and~not~((outflow>inflow)~and~(pressure~<~1000)))

~~Do~something;

Else

~~Do~something~else;

EndIf
\end{lyxcode}
Write the wwf corresponding to the test.

Rewrite this wwf using equivalence rules.
\end{xca}
Electronic circuits and logical gates:

\begin{xca}
Build an electronic circuit for $(A\wedge B)\rightarrow C'$.
\begin{itemize}
\item Case 1: you have electronic gates TRUE, FALSE, AND, OR, NAND.
\item Case 2: you only have electronic gates NAND.
\end{itemize}
\end{xca}

\section{Propositional logic}


\subsection{Arguments}

We have seen propositions, well formed formula for formalizing statements.

We now need to formalize arguments.

\begin{example*}
\cite[Example 17 p. 28]{Gersting.MSCS}

Let's formalize the following argument:

{}``If interest rates drop, the housing market will improve. 

Either the federal discount rate will drop, or the housing market
will not improve. 

Interest rates will drop. 

Therefore the federal discount rate will drop.''

Basic statements:
\begin{itemize}
\item I: Interest rates drop
\item H: The housing market will improve
\item F: The federal discount rate will drop
\end{itemize}
Argument: $(I\rightarrow H)\wedge(F\vee H')\wedge I\Imp F$
\end{example*}
\begin{defn*}
An \emph{argument} is a wff of the form $P_{1}\wedge P_{2}\wedge\cdots\wedge P_{n}\Imp Q$.

$P_{1},\cdots,P_{n}$ are the \emph{hypothesis}.

$Q$ is the \emph{conclusion}.

The argument is \emph{valid} iff $P_{1}\wedge P_{2}\wedge\cdots\wedge P_{n}\Imp Q$
is a tautology.
\end{defn*}
\begin{xca}
Prove that the following arguments are valid:
\begin{enumerate}
\item $[A\rightarrow(B\rightarrow C)]\Imp[(A\wedge B)\rightarrow C]$
\item $[(A\wedge B)\rightarrow C]\Imp[A\rightarrow(B\rightarrow C)]$
\end{enumerate}
Why is this reasonable ?

{}``If the sun shine then if you don't put sun cream, you will get
burned'': $A\Imp(B\rightarrow C)$

{}``If the sun shine and you don't put sun cream, then you will get
burned'': $(A\wedge B)\Imp C$
\end{xca}
\begin{example*}
{}``George Washington was the first president of the United States.

Therefore everyday has 24 hours.''
\end{example*}
We put some more restrictions to only keep {}``meaningful'' arguments.

\begin{itemize}
\item $Q$ has some relation with the $P_{i}$.
\item the $P_{i}$ are not in contradiction
\end{itemize}

\subsection{Proof sequences}

So now, how to prove that an argument is a tautology ?

\begin{enumerate}
\item Use the truth table
\item Use formal logic!
\end{enumerate}
\begin{example*}
Let's prove that the argument $A\vee(A\vee B)'\Imp(A\vee B')$ is
valid.

We are lazy to compute the truth table.

Instead, we assume that the hypothesis is valid, and use a series
of equivalences to deduce that the conclusion is valid.

\[
\begin{array}{lll}
1. & A\vee(A\vee B)' & (\textrm{Hypothesis})\\
2. & A\vee(A'\wedge B') & (\textrm{De Morgan}'s,\textrm{ }1)\\
3. & (A\vee A')\wedge(A\vee B') & (\textrm{Distributivity},\textrm{ }2)\\
4. & 1\wedge(A\vee B') & (\textrm{Complement},\textrm{ }3)\\
5. & (A\vee B') & (\textrm{Identity},\textrm{ }4)\end{array}\]

\end{example*}
What we just did is called a \emph{proof sequence}.

This is our first proof using \emph{formal logic}.

\begin{xca}
Prove that the following argument is valid:

$(A\vee B)'\vee(A'\wedge B)\Imp A'$
\end{xca}
\begin{defn*}
\emph{Formal Logic}: wff + set of derivation rules (formal system).
\end{defn*}
What derivation rules shall we accept?

We want our formal logic to be:

\begin{itemize}
\item Correct
\item Complete
\item Minimal
\item Powerful
\end{itemize}

\subsection{Looking for derivation Rules}

\begin{example*}
$A\wedge B\Imp A$
\end{example*}
Equivalences rules are not enough.

We can't prove the previous statement, because $A\wedge B$ is strictly
stronger than $A$.

We have build equivalence rules from equivalences $P\leftrightarrow Q$.

We can build \emph{Inference rules} from any valid argument $P\rightarrow Q$.

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|}
\hline 
Rule name&
From&
Can derive\tabularnewline
\hline
\hline 
modus ponens (mp)&
 $P$, $(P\rightarrow Q)$&
$Q$\tabularnewline
\hline 
modus tollens (mt)&
$(P\rightarrow Q)$, $Q'$&
$P'$\tabularnewline
\hline 
conjunction (con)&
$P$, $Q$&
$P\wedge Q$\tabularnewline
\hline 
simplification (sim)&
$P\wedge Q$&
$P$, $Q$\tabularnewline
\hline 
addition (add)&
$P$&
$P\vee Q$\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

\begin{example*}
$A\wedge(A\rightarrow B)\wedge(B\rightarrow C)\Imp C$

\[
\begin{array}{lll}
1. & A\wedge(A\rightarrow B)\wedge(B\rightarrow C) & (\textrm{Hypothesis})\\
2. & A & (\textrm{Simplification},\textrm{ }1)\\
3. & A\rightarrow B & (\textrm{Simplification},\textrm{ }1)\\
4. & B & (\textrm{Modus ponens},\textrm{ }2,\textrm{ }3)\\
5. & B\rightarrow C & (\textrm{Simplification},\textrm{ }1)\\
6. & C & (\textrm{Modus ponens},\textrm{ }4,\textrm{ }5)\end{array}\]

\end{example*}
%

\begin{example*}
$(A\rightarrow(B\vee C))\wedge B'\wedge C'\Imp A'$

\[
\begin{array}{lll}
1. & (A\rightarrow(B\vee C))\wedge B'\wedge C' & (\textrm{Hypothesis})\\
2. & (A\rightarrow(B\vee C)) & (\textrm{Simplification }1)\\
3. & (B'\wedge C') & (\textrm{Simplification }1)\\
4. & (B\vee C)' & (\textrm{De Morgan}'\textrm{s }3)\\
5. & A' & (\textrm{Modus tollens }4,\textrm{ }5)\end{array}\]

\end{example*}
\begin{xca}
Prove the validity of the following arguments using formal logic:
\begin{enumerate}
\item $A\wedge(B\rightarrow C)\wedge[(A\wedge B)\rightarrow(D\vee C')]\wedge B\rightarrow D$
\item $A'\wedge(A\vee B)\rightarrow B$
\item $A'\wedge B\wedge[B\rightarrow(A\vee C)]\rightarrow C$
\item $A\wedge A'\rightarrow B$
\end{enumerate}
\end{xca}
\begin{thm}
This formal logic is correct and complete.
\end{thm}
The correctness of the formal logic comes from the way we built the
rules from valid arguments.

Proving it's complete is far more difficult.


\subsection{Methods to make it easier}

Our logic is complete, but still not very practical to use. 

Here are some tricks to make it easier.

Most of the time, the proofs start like this:

\[
\begin{array}{lll}
1. & (A\rightarrow(B\vee C))\wedge B'\wedge C' & (\textrm{hyp})\\
2. & (A\rightarrow(B\vee C)) & (\textrm{Simp }1)\\
3. & (B'\wedge C') & (\textrm{Simp }1)\\
\cdots & \cdots & \cdots\end{array}\]


The steps 2 and 3 are pretty trivial, and it's reasonable to start
directly with:

\[
\begin{array}{lll}
1. & (A\rightarrow(B\vee C)) & (\textrm{hyp})\\
2. & (B'\wedge C') & (\textrm{hyp})\\
\cdots & \cdots & \cdots\end{array}\]



\subsubsection{The deduction method}

\begin{example*}
$(A\rightarrow B)\wedge(B\rightarrow C)\Imp(A\rightarrow C)$

The obvious start is:

\[
\begin{array}{lll}
1. & (A\rightarrow B) & (\textrm{hyp})\\
2. & (B\rightarrow C) & (\textrm{hyp})\end{array}\]


But then it's pretty painful:

\[
\begin{array}{lll}
3. & A'\vee B & (\textrm{imp }1)\\
4. & A'\vee(B\rightarrow C) & (\textrm{add }2)\\
5. & (A'\vee B)\wedge(A'\vee(B\rightarrow C)) & (\textrm{con }3,\textrm{ }4)\\
6. & A'\vee(B\wedge(B'\rightarrow C)) & (\textrm{dist }5)\\
7. & A'\vee C & (\textrm{mp }6)\\
8. & A\rightarrow C & (\textrm{imp }7)\end{array}\]


Here it's easier to first rewrite the argument into an equivalent
argument.

We have seen that $P\rightarrow(Q\rightarrow R)$ and $(P\wedge Q)\rightarrow R$
are equivalent. 

So we can prove $A\wedge(A\rightarrow B)\wedge(B\rightarrow C)\Imp C$
instead, which is straightforward:

\[
\begin{array}{lll}
1. & A & (\textrm{hyp})\\
1. & (A\rightarrow B) & (\textrm{hyp})\\
2. & (B\rightarrow C) & (\textrm{hyp})\\
3. & B & (\textrm{mt }1,\textrm{ }3)\\
4. & C & (\textrm{mt }2,\textrm{ }4)\end{array}\]

\end{example*}
This trick is called the \emph{deduction method}.

It's powerful because we have:

\begin{itemize}
\item a simpler goal
\item more hypothesis
\end{itemize}
\begin{xca}
$(A\rightarrow B)\wedge[B\rightarrow(C\rightarrow D)]\wedge[A\rightarrow(B\rightarrow C)]\Imp(A\rightarrow D)$
\end{xca}

\subsubsection{Additional deduction rules}

As we have seen, any valid argument could be transformed into a new
rule.

\begin{example*}
Here are two useful rules.
\end{example*}
\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|}
\hline 
Rule name&
From&
Can derive\tabularnewline
\hline
\hline 
hypothetical syllogism (hs)&
 $P\rightarrow Q$, $Q\rightarrow R$&
$P\rightarrow R$\tabularnewline
\hline 
contraposition&
$P\rightarrow Q$&
$Q'\rightarrow P'$\tabularnewline
\hline
\end{tabular}\end{center}
\vspace{0.3cm}

Adding those new rules won't change the power of the formal logic,
but can make it more convenient. On the other hand, a minimal formal
logic is nice since it's less error prone, and it's easier to remember
all the rules.

It's up to you to choose which rules you want to use (and learn).

\begin{example*}
$(P\rightarrow Q)\wedge(P'\rightarrow Q)\rightarrow Q$.
\end{example*}

\section{Verbal arguments}

We can now start checking verbal arguments.

\begin{example*}
Let's prove the following verbal argument\cite[Example 17 p. 28]{Gersting.MSCS}:

{}``If interest rates drop, the housing market will improve. 

Either the federal discount rate will drop, or the housing market
will not improve. 

Interest rates will drop. 

Therefore the federal discount rate will drop.''
\end{example*}
\begin{xca}
Prove the following verbal argument\cite[Ex.~30 p.~32]{Gersting.MSCS}:

{}``If the program is efficient, it executes quickly. 

Either the program is efficient or it has a bug. 

However, the program does not execute quickly. 

Therefore it has a bug.''
\end{xca}

\section{Summary}


\subsection{Different levels of logic}

Three levels for arguments:

\begin{itemize}
\item formal argument as a string of symbols, proof sequence (syntactic
level).
\item formal argument as a truth table (semantic level).
\item verbal argument (interpretation level).
\end{itemize}
Any verbal argument based on propositions can be translated into a
formal argument.

The propositional logic system is complete and correct:

\begin{itemize}
\item Any formal argument proved syntactically is valid semantically.
\item Any semantically valid formal argument can be proved syntactically\\
(it can be hard, though!).
\end{itemize}

\subsection{Syntactic proof versus semantic proof}

Testing an argument by computing it's truth table is purely mechanical.

So, what's the point of formal logic ?

\begin{itemize}
\item It's often faster and shorter to write
\item You have more chance to grab the meaning of an argument
\item In predicate logic we won't be able to rely on truth tables
\end{itemize}

\end{document}
