Lesson 06 First order logic.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ This Jupyter notebook<sup>[1]</sup> is part of the Klopper Letures on Discrete Matheamtics and covers *predicate logic*\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": [
    "# Predicate logic"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## In this lesson"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Follow these links\n",
    "- [Introduction](#Introduction)\n",
    "- [The structure of sentences](#The-structure-of-sentences)\n",
    "- [Well formed formulae](#Well-formed-formulae)\n",
    "- [The predicate](#The-predicate)\n",
    "- [The quantifier](#The-quantifier)\n",
    "- [Some more techniques of proof](#Some-more-techniques-of-proof)\n",
    "    - [Proof by example](#Proof-by-example)\n",
    "    - [Proof by exhaustion](#Proof-by-exhaustion)\n",
    "    - [Proof by counterexample](#Proof-by-counterexample)\n",
    "- [Rules of inference for quantified propositions](#Rules-of-inference-for-quantified-propositions)\n",
    "- [Additional rules](#Additional-rules)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Introduction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "We have looked at propositions as declarative sentences and even used logical connectives to construct propositional functions.  We called this framework **propositional logic**.<p/>\n",
    "In this section, we will build up a more generalized framework in order to help us with proofs, called **predicate logic**.  In order to understand predicate logic, we must learn about the deconstruction of sentences."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## The structure of sentences"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We have to make use of our knowledge of the spoken and written word and remember concepts such as *nouns* and *verbs*.  How exciting is this?  A bit of language class is coming our way.  Who knew?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To understand predicate logic we start with short sentences.  We will consider two types.  The first has a *subject* and a *verb*, that's it.  Here are some examples\n",
    "- A heart pumps\n",
    "- Blood flows\n",
    "- Lungs oxygenate\n",
    "\n",
    "Here we have nouns as subjects (heart, blood and lungs) and single verbs (pumps, flows, oxygenate).  We'll call the **Type I sentences**.<p/>\n",
    "Then we have sentences that have a *subject*, a *verb* and an *object*.  From the examples above we have\n",
    "- A heart pumps blood\n",
    "\n",
    "We'll call these **Type II sentences**.<p/>\n",
    "For **Type III sentences** we will connect a *subject* with a *complement* through a *linking verb*.\n",
    "- She has a heart\n",
    "- Blood is red\n",
    "\n",
    "*She* is our subject and the complement is *a heart*, while the linking verb is *has*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "All three type sentences above can be broken down into *subjects* and **predicates**.  The subject bits are *nouns*, the rest are predicates.  It is common to symbolize predicates with uppercase iltalic letters and subjects by italic lowercase letters.  We then symbolize a sentence with the predicate first and the subject last.  So we might symbolize *a heart pumps blood* as $ Bh $, where $ h $ is *a heart* and $ B $ is *pumps blood*.<p/>\n",
    "In our sentences the lowercase subject symbols (so far) are all constants, called **logical constants**.<p/>\n",
    "As opposed to these constant subjects we might have unspecified subjects.  So instead of a logical constant we have a **logical variable**.  In the sentence: \"Someone has a disease.\", we do not have a specific subject.  Rather we have a possibility of subjects.  If the predicate is then *has a disease*, we can write something like $ Dx $, where $ x $ is our logical variable.  As an aside, there is a difference between this sentence as say: \"Someone drives to the clinic.\".  The firts sentence has a passive predicate and is of **Type III** and the second has an active predicate and is of **Type II**."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can have a sentence: \"Everyone can get the flu.\".  It is **Type II** is our scheme, but something has changed.  We still have a **logical variable** for our subject, but now, instead of *someone*, it is *everyone*.  This is called a **universal quantifier** and we will see it again below.  Let's just play with this concept a bit longer and write \"For anything, if that anything is a human, then that thing can get the flu.\".  What a sentence!  In logical variable format we would write: \"For all $ x $, if that $ x $ is a human, then $ x $ can get the flu.\".<p/>\n",
    "We use the mathematical symbols, $ \\forall $, to identify the universal quantifier.  This allows us to write our sentence in the form of propositional logic $$ { \\left( \\forall x \\right) } {H} {x} \\Rightarrow {F} {x} $$\n",
    "Here we have the predicate $ H $ for *is human* and $ F $ for *can get the flu* together with our logical variable (which is a universal quantifier), $ x $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There is also an **existential quantifier**.  It would go something like this: \"There exists a thing such that if that thing is a human then it can get the flu.\" or \"There exists and $ x $ such that if $ x $ is a human then $ x $ can get the flu.\".  You might have guessed it.  In propositional logic form we have\n",
    "$$ { \\left( \\exists {x} \\right) } {H} {x} \\Rightarrow {F} {x} $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can really string these together $$ \\left( \\forall x \\right) \\left( \\exists y \\right) \\left( \\exists z \\right) \\left( Fx\\land Gy\\land Hz \\right)  $$\n",
    "These are called **multiple quantifiers**."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Well formed formulae"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In proposition logic we represented whole *sentences* with single variables such as $ p \\land q $, with either $ p $  and $ q $ being $ \\mathrm{true} $ or $ \\mathrm{false} $.  In predicate logic we deconstruct a sentence, so we have to be circumspect about how we construct their representations.  This is done through certain rules creating **well formed formulae** (wffe, singular wff)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here are the rules\n",
    "- All sentences in propositional logic are wffe\n",
    "- If $ C $ is a predicate and $ c $ is a constant ot variable then $ cC $ is a wff\n",
    "- Predicates can apply to more than one subject so if $ C $ is a predicate and $ {c}_{1}, {c}_{2}, \\dots , {c}_{n} $ are constants or variables then $ {C}{c}_{1}, {c}_{2}, \\dots , {c}_{n} $ (which by the way can be represented by the conjunction $ {C}{c}_{1} \\land {C}{c}_{2} \\land \\dots \\land {C}{c}_{n} $) is a wff\n",
    "    - An example would be: \"Red blood cells are round and transport oxygen.\"\n",
    "- Conjunctions, disjunctions, negations, implications and biconditionals can be placed between wffe and the results will also be wffe\n",
    "- Quantifiers can be represented by wildcards (usually a $ \\# $), so if we have a wff (say we call it $ W $) containing variable $ {w}_{1}, {w}_{2}, \\dots , {w}_{n} $ then $ { \\left( \\# {w}_{1} \\right) } { \\left( \\# {w}_{2} \\right) } \\dots { \\left( \\# {w}_{n} \\right) } {W} $ is a wff\n",
    "- Wffe do not have to be true to be a wff, so \"Humans get the flu.\" and \"The flu gets humans.\" are both wffe\n",
    "- If we have more than one constant or variable, $ {c}_{1}, {c}_{2} $ and the predicate $ C $, then both $ {C}{c}_{1}{c}_{2} $ and $ {C}{c}_{2}{c}_{1} $ are wffe."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Example of predicate logic sentences that are not wffe are\n",
    "- $ CC{c} $\n",
    "- $ cC $\n",
    "- $ C {c}_{1} C $"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "## The predicate"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We started building our understanding of predicate logic around the concept of a sentence.  We saw that the type of sentences we are considering have a subject and some description, either active of passive, of the subject.  This description is the **predicate**, also called an **open sentence**.  Let's bring some mathematics into our sentences.<p/>\n",
    "Here is an example sentence: \"$ \\sqrt{2} $ is an irrational number.\".  Here, $ \\sqrt{2} $ is the object and the predicate is:  \"...is an irrational number.\".<p/>\n",
    "The predicate is not a proposition.  We could have had the sentence: \" $ x $ is an irrational number.\".  We could summarize this sentence as: $ {f} {\\left( x \\right)} $.  Now, if we subsituted certain numbers for $ x $, we have a proposition that can have a truth value."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can constrain the values of $ x $.  This is known as the **universe of discourse**, $ \\mathbb{U} $.  If we make the universe of discourse $ \\mathbb{U} = \\mathbb{R} \\times \\mathbb{R} $ we could have $ {f} {\\left( x,y \\right)}: x + y = 5 $.  Given $ \\mathbb{U} $ this function maps to the set $ \\left\\{ \\mathrm{true}, \\mathrm{false} \\right\\} $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We could define a predicate properly as a function $ f $ in $ n $ variables from a set $ \\mathbb{U} $ in the form $ f:{\\mathbb{U}^{n}} {\\rightarrow} {\\left\\{ \\mathrm{true} , \\mathrm{false} \\right\\}} $, where $ \\mathbb{U}^{n} $ is the Cartesian product of $ n $ copies of $ \\mathbb{U} $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's look at some example of predicates\n",
    "- $ {R}{\\left( x \\right)} : x $ is a rational number\n",
    "- $ {G}{\\left( y \\right)} : y > 5 $\n",
    "- $ {S}{\\left( x, y \\right)} : x + y = 5 $\n",
    "- $ {Y}{\\left( x \\right)} : x $ is an inflamed organ (we don't need the notion of numbers)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## The quantifier"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Abobe and in **Lesson 04 Introduction to statements of logic** we looked at *propositional functions and quantifiers*.  We revisit this concept now, in view of a predicate."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Declarative senctences can use words to indicate quantity such as *all*, *some*, *none*, *one*, *multiple* and so on.  These are called **quantifiers**."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There are two quantifiers.  The first is the **universal quantifier** and refers to the description, *all*.  We use the mathematical symbol, $ \\forall $, as in $ {\\forall}{x} \\in \\mathbb{U} $.<p/>\n",
    "We can use this in a proposition in as much as if we had a universe of discourse and all the values in that universe satifies the sentence, then the proposition is *true* else it is *false*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Consider two predicates.  We'll name them $ A $ and $ B $ and imagine them as sets with elements.  If we let $ A = B $ or $ A\\subset B $ then we could have the following\n",
    "$$ { \\left( \\forall x \\right) } \\left( A x \\Rightarrow B x \\right) $$\n",
    "This states that for every (all) $ x $, if $ x $ is belongs to predicate A, then $ x $ belongs to the predicate $ B $.  I use the term *belongs* only insofar as describing what we write down, i.e. $ Ax $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now, suppose $ A $ is a predicate, then we can construct a proposition $ {\\exists} {x} \\in \\mathbb{U} $ (which is read: \"There exists $ x $ in $ \\mathbb{U} $.\").  This $ \\exists $ is called the **existential quantifier**, the second of our quantifiers."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we consider the same scenario as above, but instead, we note that there is an $ x $ such that $ x $ belongs to predicate $ A $ and predicate $ B $\n",
    "$$ { \\left( \\exists x \\right) } \\left( A x \\land B x \\right) $$\n",
    "This can happen under four circumstances (think of Venn diagrams)\n",
    "- $ A $ and $ B $ have an intersection\n",
    "- $ A \\subset B $\n",
    "- $ B \\subset A $\n",
    "- $ A = B $"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "We can combine these and note\n",
    "$$ \\left[ \\left( \\exists x \\right) \\left( Ax\\land Bx \\right)  \\right] \\land \\left\\{ \\neg \\left[ \\left( \\forall x \\right) \\left( Ax\\land Bx \\right)  \\right]  \\right\\}  $$\n",
    "This states that there exists at leats one $ x $, such that $ x $ belongs to $ A $ and $ x $ belongs to $ B $ and it is not true that for all $ x $, that $ x $ belongs to $ A $ and $ x $ belongs to $ B $ (or simply not all $ x $ belongs to $ A $ and $ B $).<p/>\n",
    "This is either true if $ A $ and $ B $ have an intersection or if $ B \\subset A $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If $ x $ does not belong with either, we would write\n",
    "$$ \\neg  \\left[ { \\left( \\exists x \\right) } {Ax \\land Bx} \\right]  $$\n",
    "We can use the universal quantifier, because then there might be some that are, unless $ A $ and $ B $ are disjoint in which case we can write\n",
    "$$ { \\left( \\forall x \\right) } \\neg { \\left( Ax \\land Bx \\right) } $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Having run ahead of ourselves a little, here is a brief summary of where we stand\n",
    "- All *true* $ \\equiv $ none *false*\n",
    "    - $ \\forall x A x $ means all *true*\n",
    "    - $ \\neg \\left[ \\exists x \\left( \\neg A x  \\right) \\right] $ means none *false*\n",
    "- All *false* $ \\equiv $ none *true*\n",
    "    - $ \\left[ \\forall x \\left( \\neg Ax \\right) \\right] $ means all *false*\n",
    "    - $ \\neg \\left( \\exists x A x \\right) $ means none *true*\n",
    "- Not all *true* $ \\equiv $ at least one *false*\n",
    "    - $ \\neg \\left( \\forall x A x \\right) $ means not all *true*\n",
    "    -  $ \\left[ \\exists x \\left( \\neg A x \\right) \\right] $ means at least one *false*\n",
    "- Not all *false* $ \\equiv $ at least one *true*\n",
    "    - $ \\neg \\left[ \\forall x \\left( \\neg A x \\right) \\right] $ means not all *false*\n",
    "    - $ \\exists x A x $ means at least one *true*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Stating all these equivalences, we must be able to prove them.  For this, we can use DeMorgan's laws\n",
    "$$ \\neg \\left( p \\land q \\right) \\equiv \\left( \\neg p \\right) \\lor \\left( \\neg q \\right) \\\\ \\neg \\left( p \\lor q \\right) \\equiv \\left( \\neg p \\right) \\land \\left( \\neg q \\right) $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For all *true*, $ \\forall x A  x $ in the same universe of discourse we have $ Aa \\land Ab \\land Ac \\land Ad $.  None *false* on the other had was $ \\neg \\left[ \\exists x \\left( \\neg A x  \\right) \\right] $, which we can write as $ \\neg \\left[ \\left( \\neg Aa \\right) \\lor \\left( \\neg Ab \\right) \\lor \\left( \\neg Ac \\right) \\lor \\left( \\neg Ad \\right)  \\right]  $.  By DeMorgan's law we get $ \\left[ \\neg \\left( \\neg Aa \\right)  \\right] \\land \\left[ \\neg \\left( \\neg Ab \\right)  \\right] \\land \\left[ \\neg \\left( \\neg Ac \\right)  \\right] \\land \\left[ \\neg \\left( \\neg Ad \\right)  \\right] $.  Since we have double negations, we can *cancel* them and we have proven equivalence, $ Aa \\land Ab \\land Ac \\land Ad $. -Q.E.D."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's go for at least one *true*, $ \\exists x A x $ (the last one above).  If we have the universe of discourse $ \\mathbb{U} = \\left\\{ a, b, c, d \\right\\} $ then $ \\left\\{ \\exists x A x \\right\\} = \\left\\{ Aa \\lor Ab \\lor Ac \\lor Ad \\right\\} $, which means that not all are *false*, which is $ \\neg \\left[ \\forall x \\left( \\neg A x \\right) \\right] $, since $ \\neg \\left[ \\forall x \\left( \\neg A x \\right) \\right] = \\neg \\left[ \\left( \\neg Aa \\right) \\land \\left( \\neg Ab \\right) \\land \\left( \\neg Ac \\right) \\land \\left( \\neg Ad \\right)  \\right]  $.  By DeMorgan's law this is $ \\left[ \\neg \\left( \\neg Aa \\right) \\right] \\lor \\left[ \\neg \\left( \\neg Ab \\right) \\right] \\lor \\left[ \\neg \\left( \\neg Ac \\right) \\right] \\lor \\left[ \\neg \\left( \\neg Ad \\right) \\right] $, which is $ Aa \\lor Ab \\lor Ac \\lor Ad $.  -Q.E.D."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now that we see how these proofs are constructed, let's do the other (middle) two, also making use of DeMorgan's laws."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "$ \\left[ \\forall x \\left( \\neg Ax \\right) \\right] \\equiv \\neg \\left( \\exists x A x \\right) $\n",
    "$$ \\left[ \\forall x\\left( \\neg Ax \\right)  \\right] \\\\ =\\left( \\neg Aa \\right) \\wedge \\left( \\neg Ab \\right) \\wedge \\left( \\neg Ac \\right) \\wedge \\left( \\neg Ad \\right) \\\\ \\quad \\\\ \\neg \\left[ \\exists xAx \\right] \\\\ =\\neg \\left[ Aa\\vee Ab\\vee Ac\\vee Ad \\right] \\\\ =\\left( \\neg Aa \\right) \\wedge \\left( \\neg Ab \\right) \\wedge \\left( \\neg Ac \\right) \\wedge \\left( \\neg Ad \\right)  $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "$ \\neg \\left( \\forall x A x \\right) \\equiv \\left[ \\exists x \\left( \\neg A x \\right) \\right] $\n",
    "$$ \\neg \\left( \\forall xAx \\right) \\\\ =\\neg \\left( Aa\\wedge Ab\\wedge Ac\\wedge Ad \\right) \\\\ =\\left( \\neg Aa \\right) \\vee \\left( \\neg Ab \\right) \\vee \\left( \\neg Ac \\right) \\vee \\left( \\neg Ad \\right) \\\\ \\quad \\\\ \\left[ \\exists x\\left( \\neg Ax \\right)  \\right] \\\\ =\\left( \\neg Aa \\right) \\vee \\left( \\neg Ab \\right) \\vee \\left( \\neg Ac \\right) \\vee \\left( \\neg Ad \\right)  $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Some more techniques of proof"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We are in the swing of things, so let's look at more techniques of proofs."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Proof by example"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To show that $ \\exists x Ax $ is *true* it is sufficent to shows that $ Ac $ is *true* for some $ c $ in the universe of discourse."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Proof by exhaustion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To show that $ \\forall x \\left( \\neg A x \\right) $ is *true* we have to show that all of the subjects in the universe of discourse returns a *false*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For example, if we want to prove that there exists no rational roots to the polynomial $ {P}{\\left( x \\right)} = 2 {x}^{8} - {x}^{7} + 8 {x}^{4} + {x}^{2} - 5 $.  There are too many rational numbers to consider, so we do this by invoking the **Rational Roots Theoreom**: If $ {P}{\\left( x \\right)} = {a}_{0} + {a}_{1} {x} + {a}_{2} {x}^{2}, \\dots , {a}_{n} {x}^{n} $ is a polynomial with integer coefficients then any rational root of $ {P}{\\left( x \\right)} $ has the form $ \\frac{a}{b} $ where $ a,b $ are such that $ a $ divides $ {a}_{0} $ and $ b $ divides $ {a}_{n} $.<p/>\n",
    "Our universe of discourse is now $ \\mathbb{U} = \\left\\{ \\pm 1, \\pm 5, \\pm \\frac{1}{2}, \\pm \\frac{5}{2} \\right\\} $ and we can do the proof for these only, showing that $ {P}{\\left( c \\right)} \\ne 0 $, $ \\forall c \\in \\mathbb{U} $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Proof by counterexample"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To show that $ \\forall x A x $ is not *true*, it is suffiecient to show a specific example, $ c $, in the universe of discourse for which $ Ac $ is *false*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "Example time.  Let $ n $ be a positive integer and define $ {p}{ \\left( n \\right) } $ to be the partition function (the number of ways that $ n $ can be constructed from the sum of positive integers, irrespective of order).  Now we have to prove the propisition that for all psoitive integers $ n $, $ {p}{ \\left( n \\right) } $ is prime."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "- $ {p}{ \\left( 1 \\right) } = 1 $\n",
    "- $ {p}{ \\left( 2 \\right) } = 2 $ since it can be constructed as $ 1, 1 + 1 $ \n",
    "- $ {p}{ \\left( 3 \\right) } = 3 $ since it can be constructed as $ 3, 1 + 1 + 1, 1 + 2 $\n",
    "- $ \\vdots $\n",
    "- $ {p}{ \\left( 5 \\right) } = 7 $  since it can be constructed as $ 5, 4 + 1, 3 + 2, 3 + 1 + 1, 2 + 3, 2 + 1 + 1, 1 + 1 + 1 + 1 + 1  $\n",
    "- $ \\vdots $\n",
    "- $ {p}{ \\left( 7 \\right) } = 15 $, which is not a prime number"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Rules of inference for quantified propositions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We should take the time just to summarize our rules of inference.  Let's have a look at the **fundamental rules**."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Modus Ponens** is our first rule\n",
    "$$ \\left[ p \\land \\left( p \\Rightarrow q \\right) \\right] \\Rightarrow q $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next up we have **Hypothetical Syllogism**\n",
    "$$ \\left[ \\left( p \\Rightarrow q \\right) \\land \\left( q \\Rightarrow r \\right) \\right] \\Rightarrow \\left( p \\Rightarrow r \\right) $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**DeMorgan's Laws** for conjunction and disjunction\n",
    "$$ \\neg \\left( p \\land q \\right) = \\left( \\neg p \\right) \\lor \\left( \\neg q \\right) \\\\ \\neg \\left( p \\lor q \\right) = \\left( \\neg p \\right) \\land \\left( \\neg q \\right) $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The **Contrapositive Law**\n",
    "$$ \\left( p \\Rightarrow q \\right) \\equiv \\left( \\neg p \\right) \\Rightarrow \\left( \\neg q \\right) $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "[Back to the top](#In-this-lesson)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Additional rules"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The propositions are good and well, but we have seen that we need first-order logic as well (predicate logic).  Let's summarize its laws."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Universal Specification** states that if a statement $ \\forall xAx $ is assumed to be *true* then the universal quantifier can be dropped to obtain $ Ac $ is *true* for an object $ c $ in the universe of discourse\n",
    "$$ \\forall xAx \\Rightarrow Ac, \\forall c $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Universal Generalization** states that if a statement $ Ac $ is *true* for each element $ c $ in the universe of discourse then the universal quantifier can be prefixed $ \\forall x A x $\n",
    "$$ Ac, \\forall c \\Rightarrow \\forall x A x $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Existential Specification** state that if $ \\exists x A x $ is assumed to be *true* then there is an element $ c $ in the universe of discourse such that $ Ac $ is *true*.\n",
    "$$ \\exists x A x \\Rightarrow Ac $$ for some $ c $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Existential Generalization** states that if $ Ac $ is *true* for some element $ c $ in the universe of discourse then $ \\exists x A x $\n",
    "$$ Ac \\Rightarrow \\exists x A x $$ "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We have to look at an example or two to make the use of these rules clear."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Example: Represent the following arguments symbolically and decide whether they are valid\n",
    "- All men have an XY chromosome pair\n",
    "- All Kings are men\n",
    "- Therefor all Kings have an XY chromosome pair"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we take that $ Ax $ symbolizes \"$ x $ is a man\", $ Bx $ symbolizes \"$ x $ is a King\" and $ Cx $ symbolizes \"$ x $ is an XY chromosome pair\" then we can symbolize this example as\n",
    "$$ \\left\\{ \\left[ \\forall x\\left( Ax \\Rightarrow Cx \\right) \\right] \\land \\left[  \\forall x\\left( Bx \\Rightarrow Ax \\right)  \\right]  \\right\\} \\rightarrow \\left[  \\forall x\\left( Bx \\Rightarrow Cx \\right)  \\right] $$\n",
    "For conjunction, we can re-write this as\n",
    "$$ \\left\\{ \\left[ \\forall x\\left( Bx \\Rightarrow Ax \\right) \\right] \\land \\left[  \\forall x\\left( Ax \\Rightarrow Cx \\right)  \\right]  \\right\\} \\rightarrow \\left[  \\forall x\\left( Bx \\Rightarrow Cx \\right)  \\right] $$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's prove this.  We start with $ \\forall x \\left( Ax \\Rightarrow Cx \\right) $.  If we apply the rule of **Universal Specification** to this we have $  Ac \\Rightarrow Cc $.  Applying **Universal Specification** on $ \\forall x \\left( Bx \\Rightarrow Ax \\right) $ gives us $ Bc \\Rightarrow Ac $.  Now we apply **Hypothetical Syllogism** and get $ \\forall x\\left( Bx \\Rightarrow Cx \\right) $ and **Universal Specification** again to get $ Bc \\Rightarrow Cc $.  We have proved that all Kings have a pair of XY chromosomes."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Another example\n",
    "- *S aureus* are dangerous bacteria\n",
    "- There are *S aureus*\n",
    "- Therefore there are dangerous bacteria"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we take $ Ax $ to mean \"$ x $ is *S aureus*\" and $ Bx $ to mean \"$ x $ is a dangerous bacteria\" we can symbolize our example as $ \\left\\{ \\left[ \\forall x\\left( Ax \\Rightarrow Bx \\right)  \\right] \\land \\left[ \\exists x Ax \\right]  \\right\\} \\Rightarrow Bx  $."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We start with $ \\exists x Ax $ and apply **Existential Specification** to get $ Ac $.  Now we take $ \\forall x\\left( Ax \\Rightarrow Bx \\right) $ and apply **Universal Specification** and get $ Ac \\rightarrow Bc $.  Using **Modus Ponens**, $ \\left[ p \\land \\left( p \\Rightarrow q \\right) \\right] \\Rightarrow q $, we get $ Ac \\land \\left( Ac \\Rightarrow Bc \\right) \\Rightarrow Bc $.  Lastly, for $ Bc $ we apply **Existential Generalization** and get $ \\exists x Bx $ and indeed, there are dangerous bacteria."
   ]
  },
  {
   "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
}