Proving it with math

There are many complicated and sophisticated ways of proving things using mathematics. Unfortunately, I haven't been able to investigate most of them.  But there are a few simple techniques that I've thought about.

Proving it with calculation.  

Okay, so this one isn't what people normally think of as a proof.  But it seems to be one of the easier ones to do.  You just write a program that does the thing.  And then you run it.  It works?  You're done.  It happened, it's proved.  QED.  

So on one hand, you have the curry howard correspondence, which says that programs are proofs.  And on the other hand you have ad hoc constructs, inconsistent compilers, undefined behavior, gamma rays from space flipping bits in your ram, sloppy programmers, and totally ill defined inputs, outputs, or even any idea of what the thing is even supposed to do.  

Personally, I like this one the best.  Probably because it's the one I'm good at.  But there's also something satisfying about it to me.  Not sure I can put my finger on it, but for an arbitrary *thing* I would rather show it with a lambda term than show it with type theory.

Proving it with deduction.

This one is pretty straight forward.  If you have an 'A' and you have a rule which states 'A -> B', then you can conclude 'B'.  

So basically, you gather all of the rules and initial conditions and then you see which way you can point it in.  

This one makes me think about parsing.  You have a language of primitive atoms (or letters) and a set of allowable transform rules.  Then your goal is to search through a very large or infinite tree of possible transformation sequences ... looking for something that is "interesting".  

I'm not exactly sure what to think about this one.  However, it does seem really useful.

Proving it with induction.

That thing from high school or wherever.  You know.  Prove it for 0, then prove it for x (what did that step even mean?), then prove it for x + 1 (why does this help?), and then you're done.   

So basically what's going on is that you're proving the *thing* for a real, specific, base case, then proving it for a general case, and then proving it for a general case modified in such a way that the last step could theoretically be repeated for every item in your set.  ... so with the traditional x + 1 proof, this really only works if your set of possible inputs are natural numbers (ie 0 to infinity).  If you start with zero and an increment function (ie + 1), then you are able to generate every element in the set of natural numbers.  

So again, the theory is more or less that you just proved it for x + 1, so you could theoretically prove it for *every* natural number, therefore you did prove it for every natural number.

This always bothered me as a child because I really didn't understand anything that was going on.  Then I learned set theory and got used to recursion (check out the little schemer and the seasoned schemer for great help getting your mind around recursion).  Now when I think about induction, I just think recursion.

Proving it with contradiction.

So this one is probably the least satisfying proof method.  And at the same time the most satisfying proof method.  With programming you can basically assemble a set of instructions to do a *thing*.  With deduction you have all of the steps to get to the *thing*.  WIth induction you have a recursive sketch of the structure of the *thing*.  With contradiction you just have the *thing* because the alternative is impossible.

So the basic idea is this.  I don't know how to prove the *thing*.  But let's assume the alternative.  IE the *thing* doesn't exist or isn't true.  Now, all we have to do is find a side effect of the *thing* not existing which is totally impossible (the contradiction).  And presto chango *thing* must be true because otherwise *impossible* must be true ... and *impossible* ISNT true (because it can't be ... that would be impossible).

This isn't very satisfying if you are trying to understand why the *thing* is true or isn't true.  If you're trying to understand the structure or form of the problem.

On the other hand.  If you don't care about the structure or form of the problem.  You just need the answer.  Or if someone wants *thing* to be true or wants you to do *thing* (and you don't ... and you want to be a little bit too clever for your own good).  For these types of things I have a hard time thinking of something that's more satisfying than proof by contradiction.  

"Hey, here's a bunch of busy work to do in order to make sure that we are correctly handling situation X."

"Hmm.  If X ever did happen, it would wipe out all of reality.  Past and future.  We're still here, so clearly X is never going to happen ... because then we wouldn't be here.  We're handling situation X appropriately by definition."

ahh