
\section{Logical Systems}

Now we can say what proofs are\.  
A proof takes {\bf axioms} and {\bf definitions} and
uses {\bf deduction rules}, step by step, to get a desired conclusion.

\subsection{Axioms}

\begin{defin*}
  An {\em axiom} is a proposition that is assumed to be true.
\end{defin*}

Axioms aren't proved---just accepted as reasonable assumptions\.
``Axiom'' is Greek for ``to think worthy,'' not ``to be true''\.
Here are some examples:

\begin{axiom}[Arithmetic]
  If $a = b$ and $b = c$, then $a = c$.
\end{axiom}

This seems very reasonable!\\
But sometimes the right choice of axiom is not clear. 

\begin{axiom}[Euclidean geometry]
  Given a line $l$ and a point $p$ not on $l$, there is exactly one line
  through $p$ parallel to $l$.
\end{axiom}

\begin{axiom}[Spherical geometry]
  Given a line $l$ and a point $p$ not on $l$, there is {\em no} line
  through $p$ parallel to $l$.
\end{axiom}

\begin{axiom}[Hyperbolic geometry]
  Given a line $l$ and a point $p$ not on $l$, there are {\em infinitely
    many} lines through $p$ parallel to $l$.
\end{axiom}
None of the three preceding axioms is better than the others; all
yield equally good proofs\.  Of course, a different choice of axioms
makes different propositions true\.  In fact, the axioms above are
mutually contradictory---they can't all be true\.  

Mathematicians still argue about which axioms are ``right,'' e.g.,
there is a lot of debate about the Axiom of Choice (whose assertion
and denial are equally consistent with other commonly agreed upon
axioms).

Axioms provide us with a place to start in building proofs\.
Every argument has assumptions\.  
To be rigorous, it is important to state those assumptions explicitly as 
axioms. 

In the real world axioms capture our beliefs about what we are
studying (e.g. Newton's mechanics)\. Definitions capture what we think
is important (e.g. force, velocity)\.  If we prove something with
those axioms, we tend to believe it about the real world\.  If the
real world turns out different, we need to change our axioms (Einstein
made us discard Newton's axioms).

\subsection{Definitions}

Definitions are used to agree on what something means.
\begin{itemize}
\item A natural number $\geq 2$ is prime if it has no divisors other than 
  itself and 1.
\item A divisor of an integer $z$ is a nonzero integer $d$
  for which there exists some integer $k$ such that $z = k d$.  We say
  $d \mid z$
\item A triangle is a polygon with 3 sides.
\end{itemize}
Definitions are axiomatic: we can define terms to mean whatever we want, 
so long as we do so unambiguously\. 
Definitions can be built from prior definitions: polygon, integer.

\subsection{Deduction Rules}

These are also called inference rules\.  They are rules for combining
axioms and true propositions to construct more true propositions\.
The most fundamental inference rule is called \emph{modus ponens}
(Latin: method of affirming)\. Another important rule is called
\emph{modus tollens} (Latin: method of denying)\.
\begin{enumerate}
\item Modus ponens: \\
  Given that $P$ and $P \Rightarrow Q$ are both true \\
  Conclude:  $Q$ 

\item Modus tollens (proof by contradiction): \\
  Given:  $P \Rightarrow Q$, $\neg Q$ \\
  Conclude: $\neg P$ 

\item (Special case of Modus Tollens) \\
  Given:  $\neg P \Rightarrow \ms{false}$ \\
  Conclude:  $P$ 

\item (Another special case) \\
  Given: $P$, $\neg P$: \\
  Conclude: $\ms{false}$ 

\item Syllogism: \\
  Given:  $P \Rightarrow Q$, $Q \Rightarrow R$ \\
  Conclude:  $P \Rightarrow R$ 

\item (Cases): \\
  Given: $Q \Rightarrow P$, $\neg Q \Rightarrow P$ \\
  Conclude: $P$
\end{enumerate}

These deduction rules rely only on the truth values of the statements 
$P,Q,R$, and \emph{not} on what the particular statements are\.  So we can 
apply them in many situations.

Truth tables provide a source of deduction rules, all of which are
accepted in mathematics\.
Namely, if $R \Rightarrow S$ is a tautology, then \\
Given: $R$ \\
Conclude: $S$ \\
is an allowable inference rule\.

\noindent
Examples: 
\begin{enumerate}
\item
  $[P \wedge (P \Rightarrow Q)] \Rightarrow Q$ 
  is a tautology (check the truth table), which leads to (Modus Ponens): \\
  Given: $P \wedge (P \Rightarrow Q)$ \\
  Conclude: $Q$ 

\item
  $(P \wedge \neg P) \Rightarrow \ms{false}$ is a tautology, which leads to: \\
  Given: $P$, $\neg P$: \\
  Conclude: $\ms{false}$ 

\item
  $[(P \vee Q) \wedge \neg P] \implies Q$
  is a tautology, which leads to (Disjunctive Syllogism): \\
  Given: $P \vee Q$, $\neg P$ \\ 
  Conclude: $Q$ 
\end{enumerate}

Another way of getting acceptable deduction rules from a truth table,
exemplified using Modus Ponens again: \\
In the truth table, look at the rows where $P$ and $P \Rightarrow Q$ 
are both true\.
$P$ is true in rows 1, 2 \.
$Q$ is true in rows 1, 3, 4 \.
So, both are true exactly in row 1\.
But in that row, $Q$ is also true. 

\subsection{Formal proofs}

In a complete, formal proof of a theorem, each step follows from
previous steps using formal deduction rules\.  There is no room for
debate or misinterpetation\.  Such a process is ideally so systematic
that it could be checked mechanically by a program\.  Modern theorem
proving programs can do this.

Mathematicians generally don't write proofs that formally\.
Rather, they write them in concise prose, but in such a way that others who
are knowledgeable about proof methods can understand how to fill in the
gaps\.  You must develop a sense of the ``right level of detail'' for
proofs in this course.

What about using a computer to {\em produce\/} proofs of true theorems
automatically?  

Russel and Whitehead, in {\em Principia Mathematica}, tried to write
down a sufficient set of axioms that would let us prove everything
interesting\.  Then Hilbert posed (as one is his 23 famous problems)
the problem of finding such a method\.  One of the great
accomplishments of 20th century math is the proof that no such method
exists (G\"odel)\.  In fact, we don't even have a proof that the
axioms of math are consistent!  Maybe they are all
self-contradictory\!  But they have stood up well over time.

Even if we limit ourselves to things that can be proven, computers
won't be much help\.  Finding a proof---even, say, just a proof that a
given propositional logic statement is a tautology---is {\bf
  NP-complete}\.  This means that it is intractable in a certain
formal sense you will learn about in 6.045 or 6.046.

So we will always rely on human intuition to find the proofs, although
we will be using computers more and more to check if they are right.

