Formal Proofs

So for the next section of homework that I am going to be working on, I have to read two chapters on Formal Proofs. I don't know how many of you have been blessed with this requirement in your past (very few of you I expect), as you would not normally need to unless you have taken a logic class, or if you were really unlucky, a geometry class that covered Formal Proofs. Anyway, what I am about to learn is even worse. Not only do we have to learn Formal Proofs, we have to learn how to express them using the Z formal language. To say the least, it is complicated. Fortunately (unfortunately?) I have taken both logic and the bad kind of geometry, so I am fairly familier with Formal Proofs. Fun example Themata Schema(from memory, probably wrong)

If P Then Q, Not Q -> Not P (where -> signifies a sequent)
----------------------------
If P Then Q Therefore If Not Q Then Not P

Looks easy ya? Well how about if you start getting into something past the basics, like:
Iff P ^ Q Then Q U P ^ Not Q, Not Q -> P
-------------------------------------------
Iff P ^ Q Then Q U P ^ Not Q Therefore If Not Q Then P

At least with the first example you can look at it quickly and see that it is a reasonable statement. By the time you get to the second example, there are so many symbols that you can quickly loose track of what you are proving. Oh yes, I forgot to mention, P and Q can stand for a set of equations, which means you potentially have to work through even more.
At this point I will let those of you who are still working on solving the second example know that I just made it up, and it is probably absolutely false. So no, it is not you. Its me. Really.

I really don't like this portion of the class. Fortunately in another month or so we will be moving to the real world applications of Z and Information Security. That will be fun. No data will be safe from me then! MUWAHAHAHA! Oh! I mean... Data, what data? shhhhhh! Don't tell any one.