Mathematical Proof and the Principles of Mathematics/Logic/The existential quantifier

If the universal quantifier is an extended version of conjunction, then what about an extended version of disjunction? This is the only other connective for which this type of extension makes sense, as you should be able to convince yourself.

The existential quantifier

edit

We define the existential quantifier in terms of the universal quantifier by taking

For some  ,  

to mean

Not (for all  , not  ).

The second statement is a bit complicated so lit's unpack it to see if the definition makes sense. For the statement

For all  ,  

to be False there would be need to a value of   for which   is False. Applying this when   is not  , this says that For the statement

For all  , not  

to be False there would be need to a value of   for which   is True. In other words

Not (for all  , not  )

is the same as saying there is a value of   for which   is True, or more briefly

For some  ,  

There is another thing to notice about the statement

Not (for all  , not  )

namely that it depends on the order of the quantifier and the two negations. More specifically,

Not not (for all  ,  )

and

For all  , not not  

are both equivalent to

For all  ,  

which is not what we want.

One way to interpret the existential quantifier logically is to say that For all x, P(x) is the same as the disjunction of all the statements P(a), where a takes on every value in the universe of discourse. If the universe is discourse is finite then this can be written out explicitly. So if the universe of discourse consists of two objects 'a' and 'b', then

For some  ,  

is the same as

  or  

This makes sense in terms of our definition since

  or  

is equivalent to

not (not   and not  )

If our universe of discourse has no objects, then the definition says that

For some  ,  

is False no matter what   is. This may seem a bit odd, but it does make sense since if you rephrase the statement as

There is some   for which  

then it would have to be False if the

There is some  

part were False.

If our universe of discourse has one object,   then the definition says that

For some  ,  

is the same as

Not (for all  , not  )

or

Not not  

or

 

Coincidentally, it turns out that

For some  ,  

is equivalent to

For all  ,  

in a universe with one object.

Proving an existential quantifier

edit

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

edit

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

edit

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