Difference between revisions of "Proofs:Quantifiers"

From Department of Mathematics at UTSA
Jump to navigation Jump to search
(Created page with "==Proving a statement with a universal quantifier== To prove a statement of the form :For all <math>x</math>, <math>P(x)</math> first ask the reader to pick an arbitrary const...")
 
 
Line 13: Line 13:
 
where <math>x</math> is an unbound variable in <math>P(x)</math> and subject to restrictions on where <math>x</math> appears elsewhere in the proof. This may be a valid form of reasoning, but it's not the way a proof is normally written in a mathematical context. For one thing, the expression <math>P(x)</math>, since it has an unbound variable, is really a predicate, not a statement. But proofs in mathematics, aside from the occasional imperative such as "Assume ... ," contain only statements. The rule also requires the distinction between bound and unbound variables. But we're avoiding that distinction and focusing on the difference between statements and predicates instead.)
 
where <math>x</math> is an unbound variable in <math>P(x)</math> and subject to restrictions on where <math>x</math> appears elsewhere in the proof. This may be a valid form of reasoning, but it's not the way a proof is normally written in a mathematical context. For one thing, the expression <math>P(x)</math>, since it has an unbound variable, is really a predicate, not a statement. But proofs in mathematics, aside from the occasional imperative such as "Assume ... ," contain only statements. The rule also requires the distinction between bound and unbound variables. But we're avoiding that distinction and focusing on the difference between statements and predicates instead.)
  
==Example proof==
+
===Example proof===
 
We now have all the rules of inference needed to proof statements involving universal quantifiers, so let's put them to work with another example. The classical syllogism
 
We now have all the rules of inference needed to proof statements involving universal quantifiers, so let's put them to work with another example. The classical syllogism
 
:All people are mortal.
 
:All people are mortal.
Line 88: Line 88:
 
|From 1 and 5
 
|From 1 and 5
 
|}
 
|}
 +
 +
==Proving a a statement with an existential quantifier==
 +
As usual with this type of definition, we get two rules of inference:
 +
:From
 +
::Not (for all <math>x</math>, not <math>P(x)</math>)
 +
:deduce
 +
::For some <math>x</math>, <math>P(x)</math>)
 +
and
 +
:From
 +
::For some <math>x</math>, <math>P(x)</math>
 +
:deduce
 +
::Not (for all <math>x</math>, not <math>P(x)</math>)
 +
 +
These are very practical for doing proofs though so we'll add some others based on these. First, we'll prove, as an example:
 +
 +
:'''Prop. 1:''' <math>P(a)</math> implies for some <math>x</math>, <math>P(x).</math>
 +
 +
Set up the proof of an implication in the usual way to get
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | <math>P(a)</math>
 +
|Hypothesis
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|?
 +
|-
 +
|''n''+1
 +
|<math>P(a)</math> implies for some <math>x</math>, <math>P(x)</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
At this point we don't have anything but the definition to prove
 +
:For some <math>x</math>, <math>P(x)</math>
 +
so use that for the previous line.
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | <math>P(a)</math>
 +
|Hypothesis
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''−1
 +
|style="padding-left: 2em;" | Not (for all <math>x</math>, not <math>P(x)</math>)
 +
|?
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From ''n''−1
 +
|-
 +
|''n''+1
 +
|<math>P(a)</math> implies for some <math>x</math>, <math>P(x)</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
Now we need to prove a negation, so assume the statement is true and derive a contradiction.
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | <math>P(a)</math>
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 4em;" | For all <math>x</math>, not <math>P(x)</math>
 +
|Hypothesis
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''−2
 +
|style="padding-left: 4em;" | <math>False</math>
 +
|?
 +
|-
 +
|''n''−1
 +
|style="padding-left: 2em;" | Not (for all <math>x</math>, not <math>P(x)</math>)
 +
|From 2 and ''n''−2
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From ''n''−1
 +
|-
 +
|''n''+1
 +
|<math>P(a)</math> implies for some <math>x</math>, <math>P(x)</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
But from 2 we can deduce not <math>P(a)</math>, which leads to the needed contradiction and the proof can be completed.
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | <math>P(a)</math>
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 4em;" | For all <math>x</math>, not <math>P(x)</math>
 +
|Hypothesis
 +
|-
 +
|3
 +
|style="padding-left: 4em;" | not <math>P(a)</math>
 +
|From 2
 +
|-
 +
|4
 +
|style="padding-left: 4em;" | <math>False</math>
 +
|From 1 and 3
 +
|-
 +
|5
 +
|style="padding-left: 2em;" | Not (for all <math>x</math>, not <math>P(x)</math>)
 +
|From 2 and 4
 +
|-
 +
|6
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From 5
 +
|-
 +
|7
 +
|<math>P(a)</math> implies for some <math>x</math>, <math>P(x)</math>
 +
|From 1 and 6
 +
|}
 +
 +
Combining Prop. 1 with the other rules of inference we get
 +
:From <math>P(a)</math> derive
 +
::For some <math>x</math>, <math>P(x).</math>
 +
 +
===Using an existential quantifier===
 +
The rule for using an existential quantifier is relatively complex. It's based on the following proposition which will be our second example proof.
 +
 +
:'''Prop. 2:''' (For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)) implies <math>Q.</math>
 +
 +
First set up the proof of an implication in the normal way, and break up the hypothesis in separate statements.
 +
 +
Set up the proof of an implication in the usual way to get
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | (For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>))
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From 1
 +
|-
 +
|3
 +
|style="padding-left: 2em;" | For all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)
 +
|From 1
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | <math>Q</math>
 +
|?
 +
|-
 +
|''n''+1
 +
|(For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)) implies <math>Q.</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
Use the definition to expand line 2 since that's the only way to use an existential so far.
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | (For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>))
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From 1
 +
|-
 +
|3
 +
|style="padding-left: 2em;" | For all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)
 +
|From 1
 +
|-
 +
|4
 +
|style="padding-left: 2em;" | Not (for all <math>x</math>, not <math>P(x)</math>)
 +
|From 1
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | <math>Q</math>
 +
|?
 +
|-
 +
|''n''+1
 +
|(For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)) implies <math>Q.</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
Now we need to prove <math>Q</math>, and since there doesn't seem to be a direct proof, so set up an indirect proof.
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | (For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>))
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From 1
 +
|-
 +
|3
 +
|style="padding-left: 2em;" | For all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)
 +
|From 1
 +
|-
 +
|4
 +
|style="padding-left: 2em;" | Not (for all <math>x</math>, not <math>P(x)</math>)
 +
|From 1
 +
|-
 +
|5
 +
|style="padding-left: 4em;" | Not <math>Q</math>
 +
|Hypothesis
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''−1
 +
|style="padding-left: 4em;" | <math>False</math>
 +
|?
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | <math>Q</math>
 +
|From 5 and ''n''−1
 +
|-
 +
|''n''+1
 +
|(For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)) implies <math>Q.</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
In order to get to a contradiction, we prove that line 4 is False, in other words
 +
:For all <math>x</math>, not <math>P(x)</math>
 +
is True. This is a universal so introduce an arbitrary constant <math>a</math> and derive not <math>P(a)</math>
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | (For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>))
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From 1
 +
|-
 +
|3
 +
|style="padding-left: 2em;" | For all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)
 +
|From 1
 +
|-
 +
|4
 +
|style="padding-left: 2em;" | Not (for all <math>x</math>, not <math>P(x)</math>)
 +
|From 1
 +
|-
 +
|5
 +
|style="padding-left: 4em;" | Not <math>Q</math>
 +
|Hypothesis
 +
|-
 +
|6
 +
|style="padding-left: 6em;" | Choose <math>a</math>
 +
|Arbitrary constant
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''−3
 +
|style="padding-left: 6em;" | not <math>P(a)</math>
 +
|?
 +
|-
 +
|''n''−2
 +
|style="padding-left: 4em;" | for all <math>x</math>, not <math>P(x)</math>
 +
|From 6 and ''n''−3
 +
|-
 +
|''n''−1
 +
|style="padding-left: 4em;" | <math>False</math>
 +
|From 4 and ''n''−2
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | <math>Q</math>
 +
|From 5 and ''n''−1
 +
|-
 +
|''n''+1
 +
|(For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)) implies <math>Q.</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
At this point <math>a</math> can be plugged into line 3 and the rule of inference for statements can be used to complete the proof.
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | (For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>))
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 2em;" | For some <math>x</math>, <math>P(x)</math>
 +
|From 1
 +
|-
 +
|3
 +
|style="padding-left: 2em;" | For all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)
 +
|From 1
 +
|-
 +
|4
 +
|style="padding-left: 2em;" | Not (for all <math>x</math>, not <math>P(x)</math>)
 +
|From 1
 +
|-
 +
|5
 +
|style="padding-left: 4em;" | Not <math>Q</math>
 +
|Hypothesis
 +
|-
 +
|6
 +
|style="padding-left: 6em;" | Choose <math>a</math>
 +
|Arbitrary constant
 +
|-
 +
|7
 +
|style="padding-left: 6em;" | <math>P(a)</math> implies <math>Q</math>
 +
|From 3
 +
|-
 +
|8
 +
|style="padding-left: 6em;" | Not <math>P(a)</math>
 +
|From 5 and 7
 +
|-
 +
|9
 +
|style="padding-left: 4em;" | For all <math>x</math>, not <math>P(x)</math>
 +
|From 6 and 8
 +
|-
 +
|10
 +
|style="padding-left: 4em;" | <math>False</math>
 +
|From 4 and 9
 +
|-
 +
|11
 +
|style="padding-left: 2em;" | <math>Q</math>
 +
|From 5 and 10
 +
|-
 +
|12
 +
|(For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)) implies <math>Q.</math>
 +
|From 1 and 11
 +
|}
 +
 +
In prose format:
 +
:'''Prop. 2:''' (For some <math>x</math>, <math>P(x)</math>) and (for all <math>x</math>, (<math>P(x)</math> implies <math>Q</math>)) implies <math>Q.</math>
 +
:'''Proof:''' Assume for some <math>x</math>, <math>P(x).</math> Also assume for all <math>x</math>, (<math>P(x)</math> implies <math>Q.</math> We prove <math>Q</math> by contradiction so assume not <math>Q.</math> To get a contradiction, it is enough to prove for all <math>x</math>, not <math>P(x)</math>, since it the negation of the first assumption. Choose <math>a.</math> From the second assumption, <math>P(a)</math> implies <math>Q.</math> But this and not <math>Q</math> imply not <math>P(a).</math> This holds for any <math>a</math>, so for all <math>x</math>, not <math>P(x)</math> and this, with the first assumption, is the required contradiction.
 +
 +
By combining this proposition with the other rules of inference, including the rule for proving a universal, we can recast it as a rule of inference:
 +
 +
:If one has
 +
::For some <math>x</math>, P(x)
 +
:and if by choosing <math>a</math> as an arbitrary constant one can derive
 +
::<math>P(a)</math> implies <math>Q</math>
 +
:then deduce <math>Q</math>.
 +
 +
In order to prove the implication, one would then assume <math>P(a)</math> and derive <math>Q</math>. It's easier to combine the
 +
:Choose <math>a</math>
 +
with the
 +
:Assume <math>P(a)</math>
 +
steps into one to get
 +
:Choose <math>a: P(a).</math>
 +
Read this as:
 +
:Choose <math>a</math> such that <math>P(a).</math>
 +
With this bit of streamlining, the rule of inference becomes
 +
:If one has
 +
::For some <math>x</math>, <math>P(x)</math>
 +
:and if by choosing <math>a: P(a)</math> one can derive <math>Q</math>, then deduce <math>Q</math>.
 +
 +
==For each and for every==
 +
The two quantifiers can be combined it two ways:
 +
:For some <math>x</math>, for all <math>y</math>, <math>P(x, y).</math>
 +
:For all <math>y</math>, for some <math>x</math>, <math>P(x, y)</math>
 +
and
 +
 +
For clarity, it is better to rephrase the first as
 +
:There is some <math>x</math> so that for every  <math>y</math>, <math>P(x, y).</math>
 +
:For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y)</math>
 +
and the second as
 +
 +
Despite just being a change in the order of the quantifiers, these two statements are different. To see this, let the universe of discourse consist of magical rings and let <math>P(x, y)</math> stand for "<math>x</math> rules <math>y</math>". The second statement merely states that every ring is ruled by some ring. One could easily imagine that every ring rules itself, so this wouldn't be saying much. But the first statement says there is a ring, which we might call the One Ring, which rules all the other rings; that's quite a ring. Note that we're using the word 'every' in the first statement to emphasis that the <math>x</math> works for every <math>y</math>, while in the second statement we're using the word 'each' to emphasize that the value of <math>x</math> depends on <math>y.</math>
 +
 +
So the second statement does not imply the first, but we can proof, as our third example, that the first statement implies the second.
 +
 +
:'''Prop. 3:''' There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y)</math> implies for each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
 +
Set up a direct proof in the usual way, then use the existential according to the new rule.
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y).</math>
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 4em;" | Choose <math>a</math>: for all <math>y</math>, <math>P(a, y).</math>
 +
|Constant satisfying condition
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''−1
 +
|style="padding-left: 4em;" | For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|?
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 1, 2 and ''n''−1
 +
|-
 +
|''n''+1
 +
|There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y)</math> implies for each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
We now need to prove
 +
:For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y)</math>
 +
which is a universal, so prove it for an arbitrary <math>b</math>
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y).</math>
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 4em;" | Choose <math>a</math>: for all <math>y</math>, <math>P(a, y).</math>
 +
|Constant satisfying condition
 +
|-
 +
|3
 +
|style="padding-left: 6em;" | Choose <math>b</math>
 +
|Arbitrary constant
 +
|-
 +
| colspan=3 | (''something'')
 +
|-
 +
|''n''−2
 +
|style="padding-left: 6em;" | There is some <math>x</math> so that <math>P(x, b).</math>
 +
|?
 +
|-
 +
|''n''−1
 +
|style="padding-left: 4em;" | For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 3 and ''n''−2
 +
|-
 +
|''n''
 +
|style="padding-left: 2em;" | For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 1, 2 and ''n''−1
 +
|-
 +
|''n''+1
 +
|There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y)</math> implies for each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 1 and ''n''
 +
|}
 +
 +
Now we can plug <math>b</math> into line 2 and the proof is done.
 +
 +
{| class="wikitable" style="text-align: left"
 +
!Line
 +
!Statement
 +
!Justification
 +
|-
 +
|1
 +
|style="padding-left: 2em;" | There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y).</math>
 +
|Hypothesis
 +
|-
 +
|2
 +
|style="padding-left: 4em;" | Choose <math>a</math>: for all <math>y</math>, <math>P(a, y).</math>
 +
|Constant satisfying condition
 +
|-
 +
|3
 +
|style="padding-left: 6em;" | Choose <math>b</math>
 +
|Arbitrary constant
 +
|-
 +
|4
 +
|style="padding-left: 6em;" | <math>P(a, b)</math>
 +
|From 2
 +
|-
 +
|5
 +
|style="padding-left: 6em;" | There is some <math>x</math> so that <math>P(x, b).</math>
 +
|From 4
 +
|-
 +
|6
 +
|style="padding-left: 4em;" | For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 3 and 5
 +
|-
 +
|7
 +
|style="padding-left: 2em;" | For each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 1, 2 and 6
 +
|-
 +
|8
 +
|There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y)</math> implies for each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
|From 1 and 7
 +
|}
 +
 +
In the prose version there's no need to repeat lines 6 and 7, so it becomes:
 +
 +
:'''Prop. 3:''' There is some <math>x</math> so that for every <math>y</math>, <math>P(x, y)</math> implies for each <math>y</math>, there is some <math>x</math> so that <math>P(x, y).</math>
 +
:'''Proof:''' Assume there is some <math>x</math> so that for every <math>y</math>, <math>P(x, y).</math> Choose <math>a</math> so that for every <math>y</math>, <math>P(a, y)</math> and let <math>b</math> be arbitrary. Then <math>P(a, b)</math> and so for some <math>x</math>, <math>P(x, b).</math> This holds for arbitrary <math>b</math>, therefore for each <math>y</math> there is <math>x</math> so that <math>P(x, y).</math>
 +
  
 
==Translating categorical propositions==  
 
==Translating categorical propositions==  

Latest revision as of 15:12, 28 September 2021

Proving a statement with a universal quantifier

To prove a statement of the form

For all ,

first ask the reader to pick an arbitrary constant , then prove the statement . The idea is that, since the constant was chosen at random, with no assumptions other than that it's an object in the universe of discourse, the proof of is valid hold no matter the choice of . Therefore is true for all

Note that for a proof if implication, the reader is asked to make an assumption, then you as the prover must derive a conclusion. Similarly, in the proof of a universal, the reader is asked to do something, namely pick a constant, then you as the prover must derive a conclusion. So we'll state the rule of inference in a way similar to the way the first rule inference for implication is stated.

If by choosing as an arbitrary constant one can derive , then deduce
For all ,

It should be noted here that most books on logic follow a different convention. The rule is often stated as

From deduce
For all , .

where is an unbound variable in and subject to restrictions on where appears elsewhere in the proof. This may be a valid form of reasoning, but it's not the way a proof is normally written in a mathematical context. For one thing, the expression , since it has an unbound variable, is really a predicate, not a statement. But proofs in mathematics, aside from the occasional imperative such as "Assume ... ," contain only statements. The rule also requires the distinction between bound and unbound variables. But we're avoiding that distinction and focusing on the difference between statements and predicates instead.)

Example proof

We now have all the rules of inference needed to proof statements involving universal quantifiers, so let's put them to work with another example. The classical syllogism

All people are mortal.
Socrates is a person.
Therefore Socrates is mortal.

may be restated in our notation as

For all , ( implies ).
Therefore

where is the predicate is a person, is the predicate , and is the constant Socrates. This is supposed to be a syllogism, in other words the conclusion is supposed to be valid for any , and , as long as the first two statements are valid. This amounts to

Proposition: For all , ( implies ) and implies

This is an implication, so start with the standard outline for a direct proof.

It's probably a good idea to break up the 'and' into separate statements.

Line Statement Justification
1 For all , ( implies ) and Hypothesis
2 For all , ( implies ) From 1
3 From 1
(something)
n ?
n+1 For all , ( implies ) and implies From 1 and n

We have and need to derive , so something like implies will do the trick. But we can get that by applying s to the universal quantifier. Filling in the details gives:

Line Statement Justification
1 For all , ( implies ) and Hypothesis
2 For all , ( implies ) From 1
3 From 1
4 implies From 2
5 From 2 and 4
6 For all , ( implies ) and implies From 1 and 5

Proving a a statement with an existential quantifier

As usual with this type of definition, we get two rules of inference:

From
Not (for all , not )
deduce
For some , )

and

From
For some ,
deduce
Not (for all , not )

These are very practical for doing proofs though so we'll add some others based on these. First, we'll prove, as an example:

Prop. 1: implies for some ,

Set up the proof of an implication in the usual way to get

Line Statement Justification
1 Hypothesis
(something)
n For some , ?
n+1 implies for some , From 1 and n

At this point we don't have anything but the definition to prove

For some ,

so use that for the previous line.

Line Statement Justification
1 Hypothesis
(something)
n−1 Not (for all , not ) ?
n For some , From n−1
n+1 implies for some , From 1 and n

Now we need to prove a negation, so assume the statement is true and derive a contradiction.

Line Statement Justification
1 Hypothesis
2 For all , not Hypothesis
(something)
n−2 ?
n−1 Not (for all , not ) From 2 and n−2
n For some , From n−1
n+1 implies for some , From 1 and n

But from 2 we can deduce not , which leads to the needed contradiction and the proof can be completed.

Line Statement Justification
1 Hypothesis
2 For all , not Hypothesis
3 not From 2
4 From 1 and 3
5 Not (for all , not ) From 2 and 4
6 For some , From 5
7 implies for some , From 1 and 6

Combining Prop. 1 with the other rules of inference we get

From derive
For some ,

Using an existential quantifier

The rule for using an existential quantifier is relatively complex. It's based on the following proposition which will be our second example proof.

Prop. 2: (For some , ) and (for all , ( implies )) implies

First set up the proof of an implication in the normal way, and break up the hypothesis in separate statements.

Set up the proof of an implication in the usual way to get

Line Statement Justification
1 (For some , ) and (for all , ( implies )) Hypothesis
2 For some , From 1
3 For all , ( implies ) From 1
(something)
n ?
n+1 (For some , ) and (for all , ( implies )) implies From 1 and n

Use the definition to expand line 2 since that's the only way to use an existential so far.

Line Statement Justification
1 (For some , ) and (for all , ( implies )) Hypothesis
2 For some , From 1
3 For all , ( implies ) From 1
4 Not (for all , not ) From 1
(something)
n ?
n+1 (For some , ) and (for all , ( implies )) implies From 1 and n

Now we need to prove , and since there doesn't seem to be a direct proof, so set up an indirect proof.

Line Statement Justification
1 (For some , ) and (for all , ( implies )) Hypothesis
2 For some , From 1
3 For all , ( implies ) From 1
4 Not (for all , not ) From 1
5 Not Hypothesis
(something)
n−1 ?
n From 5 and n−1
n+1 (For some , ) and (for all , ( implies )) implies From 1 and n

In order to get to a contradiction, we prove that line 4 is False, in other words

For all , not

is True. This is a universal so introduce an arbitrary constant and derive not

Line Statement Justification
1 (For some , ) and (for all , ( implies )) Hypothesis
2 For some , From 1
3 For all , ( implies ) From 1
4 Not (for all , not ) From 1
5 Not Hypothesis
6 Choose Arbitrary constant
(something)
n−3 not ?
n−2 for all , not From 6 and n−3
n−1 From 4 and n−2
n From 5 and n−1
n+1 (For some , ) and (for all , ( implies )) implies From 1 and n

At this point can be plugged into line 3 and the rule of inference for statements can be used to complete the proof.

Line Statement Justification
1 (For some , ) and (for all , ( implies )) Hypothesis
2 For some , From 1
3 For all , ( implies ) From 1
4 Not (for all , not ) From 1
5 Not Hypothesis
6 Choose Arbitrary constant
7 implies From 3
8 Not From 5 and 7
9 For all , not From 6 and 8
10 From 4 and 9
11 From 5 and 10
12 (For some , ) and (for all , ( implies )) implies From 1 and 11

In prose format:

Prop. 2: (For some , ) and (for all , ( implies )) implies
Proof: Assume for some , Also assume for all , ( implies We prove by contradiction so assume not To get a contradiction, it is enough to prove for all , not , since it the negation of the first assumption. Choose From the second assumption, implies But this and not imply not This holds for any , so for all , not and this, with the first assumption, is the required contradiction.

By combining this proposition with the other rules of inference, including the rule for proving a universal, we can recast it as a rule of inference:

If one has
For some , P(x)
and if by choosing as an arbitrary constant one can derive
implies
then deduce .

In order to prove the implication, one would then assume and derive . It's easier to combine the

Choose

with the

Assume

steps into one to get

Choose

Read this as:

Choose such that

With this bit of streamlining, the rule of inference becomes

If one has
For some ,
and if by choosing one can derive , then deduce .

For each and for every

The two quantifiers can be combined it two ways:

For some , for all ,
For all , for some ,

and

For clarity, it is better to rephrase the first as

There is some so that for every ,
For each , there is some so that

and the second as

Despite just being a change in the order of the quantifiers, these two statements are different. To see this, let the universe of discourse consist of magical rings and let stand for " rules ". The second statement merely states that every ring is ruled by some ring. One could easily imagine that every ring rules itself, so this wouldn't be saying much. But the first statement says there is a ring, which we might call the One Ring, which rules all the other rings; that's quite a ring. Note that we're using the word 'every' in the first statement to emphasis that the works for every , while in the second statement we're using the word 'each' to emphasize that the value of depends on

So the second statement does not imply the first, but we can proof, as our third example, that the first statement implies the second.

Prop. 3: There is some so that for every , implies for each , there is some so that

Set up a direct proof in the usual way, then use the existential according to the new rule.

Line Statement Justification
1 There is some so that for every , Hypothesis
2 Choose : for all , Constant satisfying condition
(something)
n−1 For each , there is some so that ?
n For each , there is some so that From 1, 2 and n−1
n+1 There is some so that for every , implies for each , there is some so that From 1 and n

We now need to prove

For each , there is some so that

which is a universal, so prove it for an arbitrary

Line Statement Justification
1 There is some so that for every , Hypothesis
2 Choose : for all , Constant satisfying condition
3 Choose Arbitrary constant
(something)
n−2 There is some so that ?
n−1 For each , there is some so that From 3 and n−2
n For each , there is some so that From 1, 2 and n−1
n+1 There is some so that for every , implies for each , there is some so that From 1 and n

Now we can plug into line 2 and the proof is done.

Line Statement Justification
1 There is some so that for every , Hypothesis
2 Choose : for all , Constant satisfying condition
3 Choose Arbitrary constant
4 From 2
5 There is some so that From 4
6 For each , there is some so that From 3 and 5
7 For each , there is some so that From 1, 2 and 6
8 There is some so that for every , implies for each , there is some so that From 1 and 7

In the prose version there's no need to repeat lines 6 and 7, so it becomes:

Prop. 3: There is some so that for every , implies for each , there is some so that
Proof: Assume there is some so that for every , Choose so that for every , and let be arbitrary. Then and so for some , This holds for arbitrary , therefore for each there is so that


Translating categorical propositions

Historically, logic dealt with categorical propositions; these are statements that relate two predicates in specific ways. There are four types:

All P are Q.
No P are Q.
Some P are Q.
Some P are not Q.

The first type, which we've already seen in the previous section, becomes

For all , ( implies ).

in our notation. The second type may be rephrased as

All P are not Q.

So in our notation it becomes

For all , ( implies not ).

Note that we have from propositional logic

implies not iff implies not .

We leave it as an exercise to prove

No P are Q iff No Q are P.

Now think about what it would mean for the first type

All P are Q.

to be False. There would need to be some object which is a P but not a Q. In other words, the statement of the fourth type

Some P are not Q.

would have to be True. On the other hand, if

Some P are not Q.

is False, then there are no P which are not Q, or put another way,

All P are Q.

So the fourth statement

Some P are not Q.

can be translated as

Not (all P are Q).

or

Not (for all , ( implies )).

Similarly, the third statement

Some P are Q.

Can be translated as

Not (no P are Q).

or

Not (for all , ( implies not )).

We'll introduce another quantifier in the next page which will make these expressions more tractable. In the mean time, we leave it as an exercise to translate two of the categorical syllogisms

All P are Q.
All Q are R.
Therefore all P are R.

and

All P are Q.
No R are Q.
Therefore No P are R.

into our notation and prove them using the rules of inference we've given up to now.

You may have noticed that results our attempts to translate categorical propositions to our notation have been both more verbose and less like natural language than the originals. So you might well wonder what is the advantage of our notation. One advantage is that our notation is expressive enough to include all mathematical statements while categorical propositions alone are too restrictive. Secondly, the categorical syllogisms do not cover all the valid forms of reasoning which are needed to prove theorems. Consider

All triangles and rectangles are rectilinear figures.
All squares are rectangles with all sides equal.
Therefore all squares are rectilinear figures.

This seems to be a valid syllogism, but since the premises both involve three predicates instead of two, it's not one of the categorical syllogisms. In addition, categorical propositions deal only with predicates and not relations, and it would be impossible to do much mathematics with predicates only.