In many of the more relaxed civilizations on the Outer Eastern Rim of the Galaxy, the Hitch Hiker's Guide has already supplanted the great Encyclopedia Galactica as the standard repository of all knowledge and wisdom, for though it has many omissions and contains much that is apocryphal, or at least wildly inaccurate, it scores over the older, more pedestrian work in two important respects. First, it is slightly cheaper; and secondly it has the words Don't Panic inscribed in large friendly letters on its cover.

So taking advice and reassurance from the cover of the guide, we proceed onward into the brave new world of new stuff we have to deal with.

If the symbols below aren't rendering (you're getting little boxes for ∧, ∨, ⊥, ⇒, ¬, you should check out the alternate version here here.

Alright, so let's get started. If you want to follow along in the slides, it's page 50.

First, we need to define what negation means. We define ¬P as

P ⇒ ⊥

That is, if P is provable, then we get absurdity! This is kind of tricky and weird! But not too weird. If we assume things that are "wrong," or "not provable" (in some sense), we can derive all sorts of wacky useless garbage that is all true, but completely worthless.

For example, if we were to assume that I were a fish, you could then go on to say that if something is a fish it has gills, therefor I have gills, and live in the ocean, and maybe I'm currently trapped in a fishtank in a dentist's office at 42 Wallaby Way in Sydney Australia. Obviously, that's all completely absurd, but it certainly is true. If I were a fish, all of those things would be true.

Don't be too concerned about it yet. Just youth roll with it. We'll talk about it more later.

We all kind of know intuitively what ∧, ∨, and ⊥ mean. So let's talk about what sort of formal rules we can get from them.

We've still got all the rules we already learned about implication, namely ⇒-introduction and ⇒-elimination. So all your work was not for naught!

Our first real new rule: ∧-introduction

If, using a set of premises, we can somehow arrive at a proof for P,
AND using another set of premises, we can arrive at a proof for Q,
then we can say for sure we have a proof of P ∧ Q.

Of course this is valid! If we've got a proof for each of them, we just smoosh the two proofs together and we've got a proof of the conjunction.

If I can prove to you that I bought some apples, and I prove I bought some bananas, well, goshdarnit, I've certainly proven that I bought some apples AND some bananas.


If we've got a deduction tree that goes from some bag of premises and gets P ∧ Q,
then we can say P.

Likewise, if we've got a deduction tree that goes from some bag of premises and gets P ∧ Q,
then we can say Q.

If I prove to you I bought apples AND bananas, I'd hope you'd be convinced I bought apples. Likewise, Bananas. ("Likewise, Bananas" is the name of my Jonathan Coulton cover band.)

Then we've got the ∨-introduction rule INNOVATIVE!

If we have a deduction from some set of premises to P,
then we can say P ∨ Q.

You might think this is a bit silly; after all, we've shown a proof of P that is valid. Why would we then go on to say, "well, we have a proof of P, or we have a proof of Q?" This rule allows us to INTRODUCE new variables into disjunctions. It's a strategic thing; sometimes you've got to lose a little ground to gain more ground. ANYWAY. It's a thing you can do.

∨-elimination (I hope you've picked up the pattern here; every operation can be introduced and eliminated in some way.)

Probably the trickiest rule we're going to encounter, the "Proof by Cases" rule.

If I've demonstrated, from some bag of premises (Gamma), a proof of P ∨ Q (that is, in some sense, either P is true, or Q is true, or both), and then,
Using another set of premises (Delta), which include the premise P, I conclude R, and then
Using another set of premises (Lambda), which include the premise Q, I conclude R,
Then we can definitely say that we have a proof of R, and we can discharge those premises P and Q.

Think about it this way: suppose I tell you that for dinner tonight, we're either having ramen or cereal, and I absolutely certifiably demonstrate that this is so (our fridge is empty, it is Christmas Eve, all the shops are closed, there is two foot of snow outside, that's all that is in the cupboard, we're starving, and we've already eaten Marjorie).

Then, suppose you know for certain that eating ramen will give you an upset stomach.
Suppose you also know for certain that eating cereal will give you an upset stomach.

Then I can guarantee you, tonight you're going to have an upset stomach.

Additionally, you've "used up" the assumptions "Eating ramen tonight," and "eating cereal tonight." You can't really say anything else about them.

Lastly, there is the ⊥-elimination rule.

Starting with some premises, if we arrive at ⊥, absurdity, then we can derive anything we like.

This is actually quite a difficult thing to show! It's somewhat intuitive (if there's a contradiction somewhere in your arguments, all bets are off, and you can come up with wacky things that you can suddenly prove (if we assume 0=1, then computers are made of pudding).

Likewise, the proof-by-contradiction rule:

If we start with a bunch of premises, as well as the premise ¬P,
and we do some deduction and arrive at ⊥, absurdity,
then we can conclude P must be provable.

The major problem with this sort of proof is that it assumes that there is a sort of dichotomy in P; that is, either P is true, or it is not true. Some people find this unsettling.

Also, this sort of proof doesn't actually tell us how to arrive at or construct P. The deduction we did was worthless garbage; it gave us absurdity. So we just jumped back and said there MUST be a proof for P, but we don't actually HAVE it!

Some people don't like this one bit.
Allons-y! Back to CIS160 Page