Wednesday, 8 October 2014

Introductions and Proofs

Just as a little pre-amble, sorry about the changes in notation, I keep trying to find a way to insert the actual symbols but I have yet to figure it out.  I'll try to stick to just the backslashes from now on.

This week was the week of the first midterm.  I actually had a big midterm in biochemistry the day before this one, so my studying may have slipped off the top-priority spot.  Ignoring that fact, I feel like it went really well, I was well prepared despite my lack of thorough preparation, if that makes any sense.  In any case, we continued with proof structure this week, which I find really fun, but I like things that have easy-to-follow steps and procedures.

The biggest thing so far this week has definitely come from tutorial (yet again), notation in proofs and symbol introduction:

Creating a general proof without actually proving anything is an integral part of solving a proof; it helps you to organize your thoughts and find out what you actually have to prove.  Here's an example:

to prove : \forall x \in D, \exists y \in D', P(x, y)
assume x in D     #domain assumption
    find y'
        [proof of y' \in D']
        then y' \in D'
        [proof of P(x, y')]
        then P(x, y')
    then \exists y \in D', P(x, y)    # \exists -intro.
then \forall x \in D, \exists y \in D', P(x, y)     # \forall -intro.

Now this only uses the quantifier introductions; there are also \and -intros, \or -intros, and =>-intros.  They can be used under specific conditions:

\and - intro:
    If you are proving P(x) \and Q(x), ignoring the quantifier, you can introduce an \and symbol if you prove P(x) and Q(x) separately.

\or - intro:
    If you are proving P(x) \or Q(x), again ignoring the quantifier, if you assume P(x) and then prove Q(x), you can introduce the \or symbol, because it is inclusive - of Q(x) is true it doesn't matter if P(x) is or not.

=> -intro:
    If you are proving P(x) => Q(x), ditto with the quantifier, this proof actually follows the same formula as for an \or -intro.  The only way for an implication to be false is for the antecedent to be true and the consequent to be false, so we assume P(x) and prove Q(x), and we can then introduce the => symbol.

No comments:

Post a Comment