Lesson 05 Methods of proof.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ This Jupyter notebook<sup>[1]</sup> is part of the Klopper Letures on Discrete Matheamtics and covers * methods of proof*\n",
    "+ Created by me, Dr Juan H Klopper\n",
    "    + Head of Acute Care Surgery\n",
    "    + Groote Schuur Hospital\n",
    "    + University Cape Town\n",
    "    + <a href=\"mailto:juan.klopper@uct.ac.za\">Email me with your thoughts, comments, suggestions and corrections</a> \n",
    "<a rel=\"license\" href=\"http://creativecommons.org/licenses/by-nc/4.0/\"><img alt=\"Creative Commons Licence\" style=\"border-width:0\" src=\"https://i.creativecommons.org/l/by-nc/4.0/88x31.png\" /></a><br /><span xmlns:dct=\"http://purl.org/dc/terms/\" href=\"http://purl.org/dc/dcmitype/InteractiveResource\" property=\"dct:title\" rel=\"dct:type\">The Klopper Lectures on Discrete Mathematics</span> <span xmlns:cc=\"http://creativecommons.org/ns#\" property=\"cc:attributionName\"></span> study notes is licensed under a <a rel=\"license\" href=\"http://creativecommons.org/licenses/by-nc/4.0/\">Creative Commons Attribution-NonCommercial 4.0 International License</a>.\n",
    "\n",
    "+ [1] Fernando Pérez, Brian E. Granger, IPython: A System for Interactive Scientific Computing, Computing in Science and Engineering, vol. 9, no. 3, pp. 21-29, May/June 2007, doi:10.1109/MCSE.2007.53. URL: http://ipython.org"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<link href='http://fonts.googleapis.com/css?family=Alegreya+Sans:100,300,400,500,700,800,900,100italic,300italic,400italic,500italic,700italic,800italic,900italic' rel='stylesheet' type='text/css'>\n",
       "<link href='http://fonts.googleapis.com/css?family=Arvo:400,700,400italic' rel='stylesheet' type='text/css'>\n",
       "<link href='http://fonts.googleapis.com/css?family=PT+Mono' rel='stylesheet' type='text/css'>\n",
       "<link href='http://fonts.googleapis.com/css?family=Shadows+Into+Light' rel='stylesheet' type='text/css'>\n",
       "<link href='http://fonts.googleapis.com/css?family=Philosopher:400,700,400italic,700italic' rel='stylesheet' type='text/css'>\n",
       "\n",
       "<style>\n",
       "\n",
       "@font-face {\n",
       "    font-family: \"Computer Modern\";\n",
       "    src: url('http://mirrors.ctan.org/fonts/cm-unicode/fonts/otf/cmunss.otf');\n",
       "}\n",
       "\n",
       "#notebook_panel { /* main background */\n",
       "    background: #ddd;\n",
       "    color: #000000;\n",
       "}\n",
       "\n",
       "\n",
       "\n",
       "/* Formatting for header cells */\n",
       ".text_cell_render h1 {\n",
       "    font-family: 'Philosopher', sans-serif;\n",
       "    font-weight: 400;\n",
       "    font-size: 2.2em;\n",
       "    line-height: 100%;\n",
       "    color: rgb(0, 80, 120);\n",
       "    margin-bottom: 0.1em;\n",
       "    margin-top: 0.1em;\n",
       "    display: block;\n",
       "}\t\n",
       ".text_cell_render h2 {\n",
       "    font-family: 'Philosopher', serif;\n",
       "    font-weight: 400;\n",
       "    font-size: 1.9em;\n",
       "    line-height: 100%;\n",
       "    color: rgb(200,100,0);\n",
       "    margin-bottom: 0.1em;\n",
       "    margin-top: 0.1em;\n",
       "    display: block;\n",
       "}\t\n",
       "\n",
       ".text_cell_render h3 {\n",
       "    font-family: 'Philosopher', serif;\n",
       "    margin-top:12px;\n",
       "    margin-bottom: 3px;\n",
       "    font-style: italic;\n",
       "    color: rgb(94,127,192);\n",
       "}\n",
       "\n",
       ".text_cell_render h4 {\n",
       "    font-family: 'Philosopher', serif;\n",
       "}\n",
       "\n",
       ".text_cell_render h5 {\n",
       "    font-family: 'Alegreya Sans', sans-serif;\n",
       "    font-weight: 300;\n",
       "    font-size: 16pt;\n",
       "    color: grey;\n",
       "    font-style: italic;\n",
       "    margin-bottom: .1em;\n",
       "    margin-top: 0.1em;\n",
       "    display: block;\n",
       "}\n",
       "\n",
       ".text_cell_render h6 {\n",
       "    font-family: 'PT Mono', sans-serif;\n",
       "    font-weight: 300;\n",
       "    font-size: 10pt;\n",
       "    color: grey;\n",
       "    margin-bottom: 1px;\n",
       "    margin-top: 1px;\n",
       "}\n",
       "\n",
       ".CodeMirror{\n",
       "        font-family: \"PT Mono\";\n",
       "        font-size: 100%;\n",
       "}\n",
       "\n",
       "</style>\n",
       "\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from IPython.core.display import HTML\n",
    "#css_file = 'numericalmoocstyle.css'\n",
    "#css_file = \"custom.css\"\n",
    "css_file = 'style.css'\n",
    "HTML(open(css_file, 'r').read())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "import sympy as sym"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "sym.init_printing(use_latex = \"mathjax\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Methods of proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## In this lesson"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Follow these links\n",
    "- [Introduction](#Introduction)\n",
    "- [Trivial proof](#Trivial-proof)\n",
    "- [Vacuous proof](#Vacuous-proof)\n",
    "- [Direct proof](#Direct-proof)\n",
    "- [Indirect proof](#Indirect-proof)\n",
    "- [Proof by contradiction](#Proof-by-contradiction)\n",
    "- [Proof by cases](#Proof-by-cases)\n",
    "- [Proof by elimination of cases](#Proof-by-elimination-of-cases)\n",
    "- [Conditional proof](#Conditional-proof)\n",
    "- [Proof of equivalence](#Proof-of-equivalence)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Introduction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In the previous lesson, we looked at logical connectives and introduced the concept of a tautology on which valid inferences are based.  In this lesson we will apply inference patterns to validate nine common methods for proving implications."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Trivial proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is the proof of $ p \\Rightarrow q $.  If it can be establised that $ q $ is *true*, regardless of the truth value of $ p $, then $ p \\Rightarrow q $ is *true*.  Let's look at the *sympy* truth table for cases where $ q $ is *true*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "p, q = sym.symbols(\"p q\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\mathrm{True}$$"
      ],
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(p >> q).subs({p:True, q:True})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\mathrm{True}$$"
      ],
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(p >> q).subs({p:False, q:True})"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Vacuous proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If it is possible to establish that $ p $ is *false*, regardless of the truth value of $ q $, then $ p \\Rightarrow q $ is *true*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\mathrm{True}$$"
      ],
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(p >> q).subs({p:False, q:True})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\mathrm{True}$$"
      ],
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(p >> q).subs({p:False, q:False})"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Direct proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The construction of a direct proof of $ p \\Rightarrow q $ begins by assuming that $ p $ is *true* and then from the available information (from the reference frame), the conclusion $ q $ is shown to be true by valid inference."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Indirect proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is the direct proof of the contrapositive.  The contrapositive of $ p \\Rightarrow q $ is $ \\neg q \\Rightarrow \\neg p $ and we write $ p \\Rightarrow q \\equiv  \\neg q \\Rightarrow \\neg p $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We do this in two steps\n",
    "- Assume $ q $ is *false*\n",
    "- Prove on the basis of this assumption and the available information (from the reference frame) that $ p $ is false."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's do an example.  If the prduct of two integers $ a $ and $ b $ is even, then either $ a $ or $ b $ is even."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "So we have the proposition, $ p $ that $ ab $ is even and the consequence, $ q $ that $ a $ is even or $ b $ is even.  The contrapositive of this is $ \\neg q $, which is $ a $ is odd and $ b $ is odd (by DeMorgans' Laws).<p/>\n",
    "So, $ a = 2m + 1 $ and $ b = 2n + 1 $ and $ ab = \\left( 2m + 1 \\right) \\left( 2n + 1 \\right) = 2 \\left( 2mn + m + n \\right) + 1 $.  This is always odd, so $ \\neg p $ is *true*.  This is equivalent to $ p \\Rightarrow q $ is *true*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Proof by contradiction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This method exploits the fact that $ p \\Rightarrow q $ is *true* if and only if $ p \\land \\neg q $ is *false*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The steps involved in this proof are\n",
    "- Assume that $ p \\land \\neg q $ is *true*\n",
    "- Discover on the basis of this assumption, some conclusion that is obviously *false*\n",
    "- This contradiction in the previous steps leads us to the proof that the original assumption was false and hence $ p \\land \\neg q = \\mathrm{false} $"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's consider an example.  Suppose that the integers $ \\left[ 1, 10 \\right] $ are randomly positioned around a circle, show that there will always be a sum of some set of $ 3 $ consecutively positioned integers that is at least $ 17 $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "First we assume that $ p \\land \\neg q $ is *true* (as above).  We can define $ {x}_{i} $ as the integer positioned at the position $ i $.  Now we have $$ {x}_{1} + {x}_{2} + {x}_{3} \\ge 17 \\\\ {x}_{2} + {x}_{3} + {x}_{4} \\ge 17 \\\\ \\vdots \\\\ {x}_{10} + {x}_{1} + {x}_{2} \\ge 17 $$\n",
    "For the $ \\land $ part we have the following\n",
    "$$ {x}_{1} + {x}_{2} + {x}_{3} < 17 \\\\ {x}_{2} + {x}_{3} + {x}_{4} < 17 \\\\ \\vdots \\\\ {x}_{10} + {x}_{1} + {x}_{2} < 17 $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we can shows the latter to be *false*, then by contradiction, $ p \\Rightarrow q $ must be *true*, since it can only be *true* if and only if $ p \\land \\neg q $ is *false*, which we shall prove by some patent example."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now, if you look at this $$ {x}_{1} + {x}_{2} + {x}_{3} < 17 \\\\ {x}_{2} + {x}_{3} + {x}_{4} < 17 \\\\ \\vdots \\\\ {x}_{10} + {x}_{1} + {x}_{2} < 17 $$ carefully, you will note that we can rewrite it as $$ 3 \\left( {x}_{1} + {x}_{2} + \\dots + {x}_{10} \\right) \\le 16 \\times 10 = 160 $$\n",
    "This means that $$ 3 \\frac{10 \\times 11}{2}= 165 \\le 160 $$\n",
    "This is a contradiction and by the proof of contradiction the original proposition must hold and there will always be a sum of $ 3 $ consecutive numbers that will add to more than $ 17 $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Proof by cases"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If $ p $ is in the form $ {p}_{1} \\lor {p}_{2} \\lor \\dots \\lor {p}_{n} $ then $ \\left(  {p}_{1} \\lor {p}_{2} \\lor \\dots \\lor {p}_{n}\\right) \\Rightarrow q $ can be establsihed by proving the different implications $ {p}_{1} \\Rightarrow q $, $ {p}_{2} \\Rightarrow q $, and so on to $ {p}_{n} \\Rightarrow q $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Proof by elimination of cases"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we are confronted with two alternatives $ p $ has to be *true* or $ q $ has to be *true*.  If we are able to verify that $ p $ is *false*, then we must conclude that $ q $ is *true*.  This is disjunctive syllogism from another point of view and we write $ \\left[ \\left( p \\lor q \\right) \\land \\neg q \\right] \\Rightarrow q  $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can extend this to more cases.  If $ {p}_{1}, {p}_{2}, \\dots , {p}_{n} $ are $ n $ propositions, then  $ \\left\\{  \\left[ \\left( {p}_{1} \\lor {p}_{2} \\lor \\dots \\lor {p}_{n} \\right) \\lor q \\right] \\land \\neg {p}_{1} \\land \\neg {p}_{2} \\land \\dots \\land {p}_{n} \\right\\} \\Rightarrow q $ is a tautology."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conditional proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The two propositions $ p \\Rightarrow \\left( q \\Rightarrow r \\right) $ and $ \\left( p \\land q \\right) \\Rightarrow r $ are equivalent.  Therefor, $ p \\Rightarrow \\left( q \\Rightarrow r \\right) $ can be proved as follows\n",
    "- Combine the two antecendents $ p $ and $ q $\n",
    "- Then prove $ r $ on the basis of the assumption"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Proof of equivalence"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we have the biconditional $ p \\Leftrightarrow q $ then it is enough to prove $ p \\Rightarrow q $ and $ p \\Leftarrow q $ separately."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.5.1"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}