pull out quantifiers section

Author: oscarlevin

source/ch_intro.ptx

@@ -16,6 +16,6 @@
 
   <xi:include href="./sec_intro-intro.ptx"/>
   <xi:include href="./sec_intro-structures.ptx"/>
-  <xi:include href="./sec_intro-sets.ptx"/>
-  <xi:include href="./sec_intro-functions.ptx"/>
+  <!-- <xi:include href="./sec_intro-sets.ptx"/>
+  <xi:include href="./sec_intro-functions.ptx"/> -->
 </chapter>

source/ch_logic.ptx

@@ -145,6 +145,7 @@
   </introduction>
   <xi:include href="./sec_logic-statements.ptx"/>
   <xi:include href="./sec_logic-prop.ptx"/>
+  <xi:include href="./sec_logic-quant.ptx"/>
   <xi:include href="./sec_logic-proofs.ptx"/>
   <xi:include href="./sec_logic-conc.ptx"/>
 </chapter>

source/sec_logic-prop.ptx

@@ -1275,124 +1275,7 @@
     </example>
   </subsection>
 
-  <subsection>
-    <title>Beyond
-      Propositions</title>
-    <p> As we saw in <xref ref="sec_logic-statements" />, not every statement can
-      be analyzed using logical connectives alone. For example, we might want to work with the
-      statement: </p>
-
-    <blockquote>
-      <p>
-        All primes greater than 2 are odd.
-      </p>
-    </blockquote>
-
-    <p> To write this
-      statement symbolically, we must use quantifiers. We can translate as follows: <me>
-        \forall x ((P(x) \wedge x \gt 2) \imp O(x))
-      </me>. In this case, we are using <m>
-      P(x)</m> to denote <q><m>x</m> is prime</q> and <m>O(x)</m> to denote <q><m>x</m> is odd.</q> These are not
-      propositions, since their truth value depends on the input <m>x</m>. Better to think of <m>P</m> and <m>
-      O</m> as denoting <em>properties</em> of their input. The technical term for these is <term>predicates</term>
-      and when we study them in logic, we need to use <term>predicate logic</term>. </p>
-
-    <p> It is important
-      to stress that predicate logic <em>extends</em> propositional logic (much in the way quantum
-      mechanics extends classical mechanics). You will notice that our statement above still used
-      the (propositional) logical connectives. Everything that we learned about logical equivalence
-      and deductions still applies. However, predicate logic allows us to analyze statements at a
-      higher resolution, digging down into the individual propositions <m>P</m>, <m>Q</m>, etc. </p>
-
-    <p>
-      A full treatment of predicate logic is beyond the scope of this text.
-      One reason is that there is no systematic procedure for deciding whether two statements in
-      predicate logic are logically equivalent (i.e., there is no analogue to truth tables here).
-      Rather, we end with a two examples of logical equivalence and deduction,
-      to pique your interest.
-    </p>
-
-    <example>
-      <statement>
-        <p>
-          Suppose we claim that there is no smallest number. We can translate this into symbols as <me>
-          \neg \exists x \forall y (x \le y)
-          </me> (literally, <q>it is not
-          true that there is a number <m>x</m> such that for all numbers <m>y</m>, <m>x</m> is less than or
-          equal to <m>y</m></q>). </p>
-
-        <p> However, we know how negation interacts with quantifiers: we can
-          pass a negation over a quantifier by switching the quantifier type (between universal and
-          existential). So the statement above should be <em>logically equivalent</em> to <me>
-            \forall x \exists y (y \lt x)
-          </me>. Notice that <m>y \lt x</m> is
-          the negation of <m>x \le y</m>. This literally says, <q>for every number <m>x</m> there is a number <m>
-          y</m> which is smaller than <m>x</m>.</q> We see that this is another way to make our
-          original claim. </p>
-      </statement>
-    </example>
-
-    <example>
-      <statement>
-        <p> Can you switch the order of
-          quantifiers? For example, consider the two statements: <me>
-            \forall x \exists y P(x,y) \qquad \mathrm{ and } \qquad \exists y \forall x P(x,y)
-          </me>.
-          Are these logically equivalent? </p>
-      </statement>
-      <solution>
-        <p> These statements are NOT logically
-          equivalent. To see this, we should provide an interpretation of the predicate <m>P(x,y)</m>
-          which makes one of the statements true and the other false. </p>
-
-        <p> Let <m>P(x,y)</m> be the
-          predicate <m>x \lt y</m>. It is true, in the natural numbers, that for all <m>x</m> there is
-          some <m>y</m> greater than that <m>x</m> (since there are infinitely many numbers). However,
-          there is not a natural number <m>y</m> which is greater than every number <m>x</m>. Thus it is
-          possible for <m>\forall x \exists y P(x,y)</m> to be true while <m>\exists y \forall x P(x,y)</m>
-          is false. </p>
-
-        <p> We cannot do the reverse of this though. If there is some <m>y</m> for which
-          every <m>x</m> satisfies <m>P(x,y)</m>, then certainly for every <m>x</m> there is some <m>y</m> which
-          satisfies <m>P(x,y)</m>. The first is saying we can find one <m>y</m> that works for every <m>x</m>.
-          The second allows different <m>y</m>'s to work for different <m>x</m>'s, but there is nothing
-          preventing us from using the same <m>y</m> that work for every <m>x</m>. In other words, while
-          we don't have logical equivalence between the two statements, we do have a valid deduction
-          rule: </p>
 
-        <sidebyside>
-
-          <tabular halign="center">
-            <row bottom="minor">
-              <cell />
-              <cell><m>\exists y \forall x P(x,y)</m>
-              </cell>
-            </row>
-            <row>
-              <cell><m>
-                  \therefore</m>
-              </cell>
-              <cell><m>\forall x \exists y P(x,y)</m>
-              </cell>
-            </row>
-          </tabular>
-
-        </sidebyside>
-
-        <p>
-          Put yet another way, this says that the single statement <me>
-            \exists y \forall x P(x,y) \imp \forall x \exists y P(x,y)
-          </me>
-          is always true. This is sort of like a tautology, although we reserve that term for
-          necessary truths in propositional logic. A statement in predicate logic that is
-          necessarily true gets the more prestigious designation of a <term>law of logic</term>
-              <idx>law of
-          logic</idx> (or sometimes <term>logically valid</term>, <idx><h>logically valid</h><see>law of logic</see>
-          </idx>
-          but that is less fun). </p>
-      </solution>
-    </example>
-  </subsection>
 
   <reading-questions xml:id="rqs-logic-prop">
     <exercise label="rq-logic-prop-equiv">