<?xml version="1.0" encoding="utf-8" standalone="no"?>
<!DOCTYPE document PUBLIC "-//CNX//DTD CNXML 0.5 plus MathML//EN" "http://cnx.rice.edu/technology/cnxml/schema/dtd/0.5/cnxml_mathml.dtd">
<document xmlns="http://cnx.rice.edu/cnxml" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:bib="http://bibtexml.sf.net/" id="m10729"> 

<name xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">First-Order Logic: equivalences</name>
<metadata xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
  <md:version xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">2.26</md:version>
  <md:created xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">2002/07/08 19:00:00 GMT-5</md:created>
  <md:revised xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">2009/01/09 10:41:02.646 US/Central</md:revised>
  <md:authorlist xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
      <md:author xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="ian">
      <md:firstname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Ian</md:firstname>
      
      <md:surname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Barland</md:surname>
      <md:email xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">ibarland@radford.edu</md:email>
    </md:author>
      <md:author xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="greiner">
      <md:firstname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">John</md:firstname>
      
      <md:surname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Greiner</md:surname>
      <md:email xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">greiner@cs.rice.edu</md:email>
    </md:author>
      <md:author xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="phokion">
      <md:firstname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Phokion</md:firstname>
      
      <md:surname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Kolaitis</md:surname>
      <md:email xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">kolaitis@cse.ucsc.edu</md:email>
    </md:author>
      <md:author xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="moshe">
      <md:firstname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Moshe</md:firstname>
      
      <md:surname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Vardi</md:surname>
      <md:email xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">vardi@cs.rice.edu</md:email>
    </md:author>
      <md:author xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="matthias">
      <md:firstname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Matthias</md:firstname>
      
      <md:surname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Felleisen</md:surname>
      <md:email xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">matthias@ccs.neu.edu</md:email>
    </md:author>
  </md:authorlist>

  <md:maintainerlist xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
    <md:maintainer xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="ian">
      <md:firstname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Ian</md:firstname>
      
      <md:surname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Barland</md:surname>
      <md:email xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">ibarland@radford.edu</md:email>
    </md:maintainer>
    <md:maintainer xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="greiner">
      <md:firstname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">John</md:firstname>
      
      <md:surname xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Greiner</md:surname>
      <md:email xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">greiner@cs.rice.edu</md:email>
    </md:maintainer>
  </md:maintainerlist>
  
  <md:keywordlist xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
    <md:keyword xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">boolean algebra</md:keyword>
    <md:keyword xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">boolean identity</md:keyword>
    <md:keyword xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">quantifier</md:keyword>
  </md:keywordlist>

  <md:abstract xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Extend the laws of boolean algebra from propositional logic
to first-order logic.</md:abstract>
</metadata>


<content xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para1">
  Now that we can express interesting concepts using the quantifiers
  “<m:math><m:mo>∃</m:mo></m:math>” (“there exists”) and 
  “<m:math><m:mo>∀</m:mo></m:math>” (“for all”),
  how can we use them for the problem of
  determining whether a formula is true?
  Back in lowly propositional logic, we had three methods:
  <list xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="list1">
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
      truth tables,
    </item>
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
      equivalences, and
    </item>
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
      formal proofs with inference rules.
    </item>
  </list>
  How can we adapt these approaches, for first-order logic?
</para>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para2">
  Well, truth tables have no analog approach.
  With quantifiers, we don't have a finite set of propositions.
  Furthermore, variables can't refer to specific items in the domain
  until we try to interpret them.
  And when we do, the domain may be of any size — possibly
  even infinite.
  Using a truth table on an infinite domain is clearly infeasible,
  but the real problem stems from how we want to be able to discuss reasoning
  without respect to a particular domain.
</para>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para3">
  However, we can add equivalences and inference rules to cope with quantifiers.
  After showing how to work with quantifiers,
  we'll come back to examine our newly-augmented systems
  for those desirable traits, soundness and completeness.
</para>


<section xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="section1">
<name xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">First-order Equivalences</name>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para4">
  When we upgrade from propositional logic to first-order logic, 
  what changes do we need to make to the laws of boolean algebra?
  Well first off, we can keep all the existing
  <cnxn xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" document="m10540">propositional equivalences</cnxn>.
  For example,
  <m:math><m:apply><m:equivalent/>
    <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
      <m:apply><m:not/> <m:apply><m:and/><m:ci>φ</m:ci> <m:ci>ψ</m:ci></m:apply> </m:apply>
    </m:apply>
    <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
      <m:apply><m:or/>
        <m:apply><m:not/><m:ci>φ</m:ci></m:apply>
        <m:apply><m:not/><m:ci>ψ</m:ci></m:apply>
      </m:apply>
    </m:apply>
  </m:apply></m:math>.
  (Technically, we're even making those equivalences stronger,
   since those meta-variables <m:math><m:ci>φ</m:ci></m:math>, <m:math><m:ci>ψ</m:ci></m:math>, <m:math><m:ci>θ</m:ci></m:math> can now stand for 
   any <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">first-order</emphasis> formula, rather than merely
   propositional formulas.)
</para>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para5">
  But, we also need <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">additional</emphasis> identities
  to deal with our new-fangled quantifiers.
  What should these be?
  The most interesting are those that relate the two kinds of quantifiers.
  Universal quantification (<m:math><m:mo>∀</m:mo></m:math>) says that something holds for
  all members of the domain, and existential quantification (<m:math><m:mo>∃</m:mo></m:math>)
  says that something holds for at least one member.
  Clearly, <m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply></m:math> implies
  <m:math><m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply></m:math>, but the other direction doesn't
  hold, so that is not an equivalence.
  <note xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" type="aside">
    Wait just a minute!  That implication holds only if the domain
    is non-empty, so that there is at least one member in it.
    We'll see this restriction appear a few times.
  </note>
</para>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para6">
  What about
  <m:math><m:apply><m:forall/>
    <m:bvar><m:ci>x</m:ci></m:bvar>
    <m:apply><m:not/><m:ci>φ</m:ci></m:apply>
  </m:apply></m:math>?
  In English,
  “for all items <m:math><m:ci>x</m:ci></m:math>, <m:math><m:ci>φ</m:ci></m:math>(<m:math><m:ci>x</m:ci></m:math>) does not hold”.
  A more natural way to say this is 
  that there is <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">no</emphasis> item <m:math><m:ci>x</m:ci></m:math>
  such that <m:math><m:ci>φ</m:ci></m:math>(<m:math><m:ci>x</m:ci></m:math>) <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">does</emphasis> hold  — that is,
  <m:math><m:apply><m:not/>
    <m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply>
  </m:apply></m:math>.
  Indeed, this will be one of our new boolean algebra rules.
</para>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para7">
  See
  <cnxn xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" document="m11045">a list of equivalences with quantifiers</cnxn>.
  As before, we can use these to show other pairs of formulas equivalent,
  as in the following examples.
</para>

<example xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="example1">
  <para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para8">
    Using these identities, we can simplify formulas such as
    the following:
    <m:math><m:apply><m:and/>
      <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
        <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
          <m:apply><m:and/>
            <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
            <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
          </m:apply>
        </m:apply>
      </m:apply>
      <m:apply><m:not/>
        <m:apply><m:exists/><m:bvar><m:ci>z</m:ci></m:bvar>
          <m:apply><m:not/>
            <m:apply><m:ci type="function">R</m:ci><m:ci>z</m:ci></m:apply>
          </m:apply>
        </m:apply>
      </m:apply>
    </m:apply></m:math>.
  </para>

  <table xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="proof1">

<tgroup xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" cols="3" align="center" colsep="1" rowsep="1">
<colspec xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colwidth="*" colname="c1"/>
<colspec xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colwidth="*" colname="c2"/>
<colspec xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colwidth="*" colname="c3"/>

<tbody xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">1</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:apply><m:and/>
             <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
               <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
                 <m:apply><m:and/>
                   <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                   <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                 </m:apply>
               </m:apply>
             </m:apply>
             <m:apply><m:not/>
               <m:apply><m:exists/><m:bvar><m:ci>z</m:ci></m:bvar>
                 <m:apply><m:not/>
                   <m:apply><m:ci type="function">R</m:ci><m:ci>z</m:ci></m:apply>
                 </m:apply>
               </m:apply>
             </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"/>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">2</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:and/>
             <m:apply><m:forall/>
               <m:bvar><m:ci>y</m:ci></m:bvar>
               <m:apply><m:forall/>
                 <m:bvar><m:ci>x</m:ci></m:bvar>
                 <m:apply><m:and/>
                   <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                   <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                 </m:apply>
               </m:apply>
             </m:apply>
             <m:apply><m:forall/>
               <m:bvar><m:ci>z</m:ci></m:bvar>
               <m:apply><m:not/>
                 <m:apply><m:not/>
                   <m:apply><m:ci type="function">R</m:ci><m:ci>z</m:ci></m:apply>
                 </m:apply>
               </m:apply>
             </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Complementation of <m:math><m:mo>∃</m:mo></m:math>
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">3</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                    <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
                       <m:apply><m:and/> <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                             <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                       </m:apply>
                    </m:apply>
                 </m:apply>
                 <m:apply><m:forall/><m:bvar><m:ci>z</m:ci></m:bvar>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>z</m:ci></m:apply>
                 </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Double Complementation
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">4</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
                    <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                       <m:apply><m:and/> <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                             <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                       </m:apply>
                    </m:apply>
                 </m:apply>
                 <m:apply><m:forall/><m:bvar><m:ci>z</m:ci></m:bvar>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>z</m:ci></m:apply>
                 </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Reordering <m:math><m:mo>∀</m:mo></m:math>s
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">5</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
                    <m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                             <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                          </m:apply>
                          <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                             <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                          </m:apply>
                    </m:apply>
                 </m:apply>
                 <m:apply><m:forall/><m:bvar><m:ci>z</m:ci></m:bvar>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>z</m:ci></m:apply>
                 </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Distribution of <m:math><m:mo>∀</m:mo></m:math> over <m:math><m:mo>∧</m:mo></m:math>
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">6</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
                    <m:apply><m:and/> <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                          <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                             <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                          </m:apply>
                    </m:apply>
                 </m:apply>
                 <m:apply><m:forall/><m:bvar><m:ci>z</m:ci></m:bvar>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>z</m:ci></m:apply>
                 </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Simplification of <m:math><m:mo>∀</m:mo></m:math> (<m:math><m:ci>y</m:ci></m:math> not free in <m:math><m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply></m:math>)
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">7</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
                    <m:apply><m:and/> <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                          <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                             <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                          </m:apply>
                    </m:apply>
                 </m:apply>
                 <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                 </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> renaming
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">8</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
              <m:apply><m:and/> <m:apply><m:and/> <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                          <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                             <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                          </m:apply>
                    </m:apply>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
              </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Distribution of <m:math><m:mo>∀</m:mo></m:math> over <m:math><m:mo>∧</m:mo></m:math>
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">9</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
              <m:apply><m:and/> <m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                             <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                          </m:apply>
                          <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                    </m:apply>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
              </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Commutativity of <m:math><m:mo>∧</m:mo></m:math>
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">10</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
              <m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                       <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                    </m:apply>
                    <m:apply><m:and/> <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                          <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
                    </m:apply>
              </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Associativity of <m:math><m:mo>∧</m:mo></m:math>
           </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">11</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
              <m:apply><m:and/> <m:apply><m:forall/><m:bvar><m:ci>y</m:ci></m:bvar>
                       <m:apply><m:ci type="function">Q</m:ci><m:ci>x</m:ci><m:ci>y</m:ci></m:apply>
                    </m:apply>
                    <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
              </m:apply>
           </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"> Idempotency of <m:math><m:mo>∧</m:mo></m:math>
           </entry>
</row></tbody>
</tgroup>
</table>

  <para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para9">
    Admittedly, some of these steps are rather small and obvious
    (<foreign xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">e.g.</foreign>, our use of commutativity and associativity);
    we include them to illustrate how the identities of propositional
    logic are also used in first-order logic.
  </para>
</example>




<example xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="example2">
  <para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para10">
    An example of 
    <m:math><m:apply><m:equivalent/>
      <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar><m:ci>ψ</m:ci></m:apply>
      <m:ci>ψ</m:ci>
    </m:apply></m:math>
    where <m:math><m:ci>ψ</m:ci></m:math> doesn't contain <m:math><m:ci>x</m:ci></m:math> occurring free:
    Let <m:math><m:ci>ψ</m:ci></m:math> be
    <cnxn xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" document="m10728" target="exercise-even-and-prime">the formula we've seen before</cnxn>,
    asserting that a positive integer <m:math><m:ci>n</m:ci></m:math> was noncomposite:
    <m:math><m:apply><m:forall/><m:bvar><m:ci>j</m:ci></m:bvar>
      <m:apply><m:forall/><m:bvar><m:ci>k</m:ci></m:bvar>
        <m:apply><m:implies/>
          <m:apply>
            <m:eq/>
            <m:apply><m:times/> <m:ci>j</m:ci> <m:ci>k</m:ci></m:apply>
            <m:ci>n</m:ci>
          </m:apply> 
          <m:apply><m:or/>
            <m:apply><m:eq/> <m:ci>j</m:ci> <m:cn>1</m:cn></m:apply>
            <m:apply><m:eq/> <m:ci>k</m:ci> <m:cn>1</m:cn></m:apply>
          </m:apply>
        </m:apply>
      </m:apply>
    </m:apply></m:math>.
    Since <m:math><m:ci>n</m:ci></m:math> occurs free, the truth of this formula
    depends on the value of <m:math><m:ci>n</m:ci></m:math>.
    The formula
    <m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar><m:ci>ψ</m:ci></m:apply></m:math>
    really is equivalent to <m:math><m:ci>ψ</m:ci></m:math>:
    It's true for exactly the same values of <m:math><m:ci>n</m:ci></m:math>.
    The use of <m:math><m:ci>x</m:ci></m:math> is essentially a bit of a rus, since <m:math><m:ci>x</m:ci></m:math> plays no part
    of the meat of the <m:math><m:ci>ψ</m:ci></m:math>.
  </para>

  <para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para11">
    However, the following formula is certainly <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">not</emphasis>
    equivalent:
    <m:math><m:apply><m:forall/><m:bvar><m:ci>n</m:ci></m:bvar><m:ci>ψ</m:ci></m:apply></m:math>.
    This formula asserts that all elements of the domain are non-composite
    (and it doesn't depend on choosing a particular interpretation for <m:math><m:ci>n</m:ci></m:math>).
    Because <m:math><m:ci>n</m:ci></m:math> occurred free, we can't use the
    “simplification of quantifiers” identity on it.
  </para>

  <para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para12">
    Finally, one more variant:
    <m:math><m:apply><m:forall/><m:bvar><m:ci>j</m:ci></m:bvar><m:ci>ψ</m:ci></m:apply></m:math>.
    This <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">is</emphasis> equivalent to the original, just like 
    <m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar><m:ci>ψ</m:ci></m:apply></m:math> was.
    Why?  The <m:math><m:ci>j</m:ci></m:math> that occurs inside <m:math><m:ci>ψ</m:ci></m:math> is a local variable,
    and is different from any enclosing bindings' <m:math><m:ci>j</m:ci></m:math>.
    As we saw, local variables shadow less-local ones, just as in most
    
    programming languages.
  </para>
</example>




<exercise xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="exercise1">
  <problem xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
    <para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para13">
      The equivalences for distributing implication over equivalences seem
      counterintuitive at first glance.  Show that the following one holds,
      given all the identities which don't involve both implication and
      quantifiers.
    </para>

    <para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para14">
      Assuming that <m:math><m:ci>ψ</m:ci></m:math> does not have any free occurrences of variable <m:math><m:ci>x</m:ci></m:math>,
      <m:math><m:apply><m:equivalent/>
        <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar> <m:apply><m:implies/> <m:ci>φ</m:ci> <m:ci>ψ</m:ci> </m:apply> </m:apply>
        <m:apply><m:implies/> <m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply> <m:ci>ψ</m:ci> </m:apply>
      </m:apply></m:math>.
    </para>
  </problem>

  <solution xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
    <table xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="proof2">

<tgroup xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" cols="3" align="center" colsep="1" rowsep="1">
<colspec xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colwidth="*" colname="c1"/>
<colspec xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colwidth="*" colname="c2"/>
<colspec xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colwidth="*" colname="c3"/>

<tbody xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">1</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar> <m:apply><m:implies/> <m:ci>φ</m:ci> <m:ci>ψ</m:ci> </m:apply> </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3"/>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">2</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar> <m:apply><m:or/> <m:apply><m:not/><m:ci>φ</m:ci></m:apply> <m:ci>ψ</m:ci> </m:apply> </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3">
          Definition of <m:math><m:mo>⇒</m:mo></m:math>
        </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">3</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:or/> <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar> <m:apply><m:not/><m:ci>φ</m:ci></m:apply> </m:apply> <m:ci>ψ</m:ci> </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3">
           Distribution of <m:math><m:mo>∀</m:mo></m:math> over <m:math><m:mo>∨</m:mo></m:math>
        </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">4</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:or/> <m:apply><m:not/><m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply></m:apply> <m:ci>ψ</m:ci> </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3">
          Complementation of <m:math><m:mo>∃</m:mo></m:math>
        </entry>
</row>
<row xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
<entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" align="left">5</entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" namest="c2" nameend="c2"><m:math><m:mo>≡</m:mo><m:apply><m:implies/> <m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply> <m:ci>ψ</m:ci> </m:apply></m:math></entry><entry xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" colname="c3">
          Definition of <m:math><m:mo>⇒</m:mo></m:math>
        </entry>
</row></tbody>
</tgroup>
</table>
  </solution>
</exercise>



<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para15">
  Are the following two sentences true?
  <list xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="list2">
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
      “All flying pigs wear top hats.”
      <m:math><m:apply><m:forall/><m:bvar><m:ci>p</m:ci></m:bvar>
         <m:apply><m:ci type="function">wears_top_hat</m:ci><m:ci>p</m:ci></m:apply>
      </m:apply></m:math>
      (over the domain of flying pigs).
    </item>
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
      “All numbers in the empty set are even.”
      <m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
         <m:apply><m:ci type="function">even</m:ci><m:ci>x</m:ci></m:apply>
      </m:apply></m:math>
      (over the empty domain).
    </item>
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
      “Every Pulitzer prize winner I've met thinks I'm smart,
             and cute, too!”
      <m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
        <m:apply><m:ci type="function">thinksImSmartAndCute</m:ci><m:ci>x</m:ci></m:apply>
      </m:apply></m:math>
      (over the empty, since I haven't met any Pulitzer prize winners).
  </item>
  </list>
  Each sentence states that some property holds for every member
  of some set (flying pigs or the empty set), but there are no 
  such members.
  Such sentences are considered <term xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">vacuously true</term>.
</para>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para16">
  Okay, maybe you believe that the sentences aren't false, but
  you still want some reason to consider them true.
  Well, think of their negations:
  <list xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="list3">
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
       “There exists a flying pig not wearing a top hat.”
       <m:math><m:apply><m:exists/><m:bvar><m:ci>p</m:ci></m:bvar>
          <m:apply><m:not/><m:ci type="function">wears_top_hat</m:ci><m:ci>p</m:ci></m:apply>
       </m:apply></m:math>,
       over the (empty) domain of flying pigs.
       You can't go off and find a flying pig which contradicts this,
       since you can't find any flying pig at all.
       (Note that the negation <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">isn't</emphasis>
        “No flying pigs wear top hats.”)
    </item>
    <item xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">
       “There exists a number in the empty set that is even.”
       <m:math><m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar><m:apply><m:not/><m:ci type="function">even</m:ci><m:ci>x</m:ci></m:apply></m:apply></m:math>,
       over the empty domain.
       (The negation <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">isn't</emphasis>
        “No numbers in the empty set are even.”)
    </item>
  </list>
  Since these negations are false, the original sentences must be true.

  This is also similar to the fact that a simple propositional implication,
  <m:math><m:apply><m:implies/><m:ci>a</m:ci> <m:ci>b</m:ci></m:apply></m:math> is true, if <m:math><m:ci>a</m:ci></m:math> is in fact false, regardless of
  the truth of <m:math><m:ci>b</m:ci></m:math>;
  in this crude analogy, <m:math><m:ci>a</m:ci></m:math> corresponds to “in the domain”.
</para>

<note xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" type="aside">
  
    In boolean algebra, we only allow the values <m:math><m:false/></m:math> and <m:math><m:true/></m:math>,
    with no third option.  This is sometimes called 
    <term xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">the law of the excluded middle</term>.
    Philosophers <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">have</emphasis> developed “trimodal”
    logics which have a third option, but everything in those logics can
    be translated into something in traditional logic; 
    such logics might be more convenient in some cases, but they
    aren't more expressive.
  ¶

  
    <term xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Fuzzy Logic</term>, on the other hand, 
    is a variant where every proposition has
    a <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">degree</emphasis> of truth (from zero to one).
    While this <emphasis xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">is</emphasis> different than propositional logic
    (and, it is the right way to model many real-world problems),
    as a logic it hasn't yielded interesting new mathematical results.
  
</note>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para17">
  Even more silliness can ensue when the domain is empty:
  For example, not only is every member of the empty set even,
  but every member is simultaneously odd!
  That is,
  <m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar>
    <m:apply><m:and/>
      <m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply>
      <m:apply><m:not/><m:apply><m:ci type="function">R</m:ci><m:ci>x</m:ci></m:apply></m:apply>
    </m:apply>
  </m:apply></m:math>
  is true (only) when the domain is the empty set.
  Even more degnerately,
  <m:math><m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar><m:false/></m:apply></m:math>
  is a true (only) on the emtpy domain.
</para>


</section> 


<section xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="section2">
<name xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/">Are we done yet?</name>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para18">
  While equivalences are very useful, we are often interested in
  implications such as the one mentioned previously:
  <m:math><m:apply><m:implies/>
    <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply>
    <m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply>
  </m:apply></m:math>.
  We could rephrase that as an equivalence,
  <m:math><m:apply><m:equivalent/>
    <m:apply><m:implies/>
      <m:apply><m:forall/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply>
      <m:apply><m:exists/><m:bvar><m:ci>x</m:ci></m:bvar> <m:ci>φ</m:ci> </m:apply>
    </m:apply>
    <m:true/>
  </m:apply></m:math>.
  Informally, it should be clear that that is rather awkward, and
  formally it is as well.
</para>

<para xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" id="para19">
  But such implications are exactly what inference rules are good for.
  So, let's continue and consider what
  <cnxn xmlns:md="http://cnx.rice.edu/mdml/0.4" xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:bib="http://bibtexml.sf.net/" document="m10774">first-order inference rules</cnxn>
  should be.
</para>

</section> 



</content>
</document>
