Rules of Proof for Identity

Press the right key for the next slide (or swipe left)

also ...

Press the left key to go backwards (or swipe right)

Press n to toggle whether notes are shown (no equivalent if you don't have a keyboard)

Press m or double tap to see a menu of slides

Rules of Proof for Identity

Earlier I said to understand identity as logicians think about it, there are just two principles you need.

These principles correspond to the identity and elimitation rules for identity.

The first principle said that if b=c, then whatever is true of b is also true of c.

This principle is the rule =Elim.

Then there was another principle, a=a is never false; this is the rule of proof =Intro.

The first rule of proof is expressed just as you would expect: there are things you have to have already in your proof, and if you have them then you can extend the proof by adding this to it.

But identity intro is a bit different. In this case there are no pre-requisites. You can use the rule regardless of what you have. The rule says that any time you like you can add a sentence of this form, so a=a or b=b or whatever.

Let's see how these rules work with a simple proof.

(Everytime I show you new rules, I'll also show you an example of how they're used.)

First I need some line numbers, and maybe a bit of space.

To apply =Elim I need an identity statement; and that's just what I have at line 2.

To apply =Elim I also need a statement about the thing named on the left hand side of the identity statement, in this case b.

That's just what I have at line 1 of the proof.

So actually I have both of the things I need to apply =Elim.

But now look at the conclusion of this argument.

The conclusion is just what =Elim allows me to conclude.

Have I finished the proof? Not yet. I need to justify the step, which involves two things: I need to cite the rule and to cite the lines I've used in applying it.

Let's look at the same thing a different way.

The first premise is a statement about b (it says a is left of it) whereas the conclusion is the same statement about c (it says that a is left of it).

I take the b from the first premise and put it into the identity statement.

I move accross the identity statement from left to right and find c. And this c I put into the conclusion just where b was earlier.

And this is just the pattern I need to make to use =Elim.

Look at this thing on your right. It looks much like a proof. But actually it's no more a proof than a toddler's scribble. Why not? (I'll return to this question later.)