|This is a tough project! I will be the first to admit it. Hopefully, you have started on it. There's not much time left... it's due sooner than I thought it was! But let's get to it. Hopefully, this page will help elucidate the project description and maybe give you some tips on implementation. Also I think I'm going to be having some extra office hours for project questions. I'll send out an email when I figure out what time. Are you sitting comfortably? Then we'll begin.||
1: Knowing how to Program (skip this if you know how to program)
First thing's first: if you don't know how to program, that is,
you don't know what a for loop is, you don't know what a class is (Java/C++),
or don't know Matlab, this is a problem. You need to learn something (I'd say
Java), really, really quickly. Try the first Five Chapters of
this or read
or pretty much any other "intro to
Java" website out there, they're all pretty much the same. You need to at
least know program flow, types, objects, and functions/methods, basic
programming stuff, to do this assignment. Perhaps most importantly, you HAVE
to know what a tree is, and how to implement one in the programming language
of your choice. (There's actually NO tree implementation in java.util, so
you're going to have to make your own tree class.
It's not hard, probably about 50 lines or so of code.)
Have you gone and done it? GO GO GO.
2: The Project Description. OK, so basically, the problem is this: we want to give a bunch of input propositions, and have a machine tell us if those propositions are always valid ("true") or have some assignment to their variables that makes them invalid (a "falsifying truth assignment"). Sounds so simple! But how are we going to do it?
|3: The Gentzen Proof System Remember when we wear learning those proof rules back in the good old days of September, and there were those weirdly formatted rules that we pretty much ignored? Yeah, we've got to go back and revisit them now. The Gentzen proof system is nice in that it reformulates the rules to match the form dictated by the lambda calculus (if you don't know what this is, don't worry about it). In other words, it's a lot more "function"-y and this will help us know how to apply the rules in the world of a programming language, where functions (methods, for you Java-people) are like our bread and butter.||
|3a: Sequents A sequent is just a pair of sets; specifically, sets containing propositions. Each node in the tree is going to contain a sequent; each sequent contains two sets of propositions. Got that? For each sequent, one of the sets contains the "inputs" (Ps) and the other, the "outputs" (Qs). If you look at the project description, these are written: P1, ..., Pm → Q1, ..., Qn, where m and n are greater than or equal to 0. Now, most everyone else I've ever seen uses a turnstile (⊢) instead of an arrow. But really that character doesn't matter, choose whatever you want, as long as it's not something we're already using: it just serves to devide the Ps from the Qs. Semicolon is nice and easy to type, so I don't have to keep looking up the wacky code for →. Remember way back when when we were talking about propositions? Propositions contain "propositional letters" (the basic building blocks, we called them Ps and Qs way back when), and these basic blocks can be either true or false. If there are a lot of blocks, there are lots of different combinations of trues and falses we can choose. One such combination is called a truth assignment. In the document, he names a truth assignment as v. You can apply a truth assignment to a proposition, and that assignment will either make the proposition valid, or it will falsify it. Take a simple example: let's make our proposition "Alex put on his hat and put on his scarf. There are two propositional letters: "Alex put on his hat" (which can either be true or false), and "Alex put on his scarf" (again, true or false). There are four truth assignments possible here. Only one of them validates the proposition (no hat today, just a scarf). 3b: The Process The keen insight we need here (found on page 2 of the project description) is that a truth assignment v satisfies the sequent if it makes ALL of the "input" propositions true while, at the same time, making AT LEAST one of the "output" propositions true. If you think of your inputs as your preconditions, and your outputs as possible goals, you want to come up with a truth assignment that satisfies all the preconditions, and satisfies one of the goals at the same time. That's the meaning of v((P1 ∧ ... ∧ Pm) ⇒ (Q1 ∨ ... ∨ Qn)) = true.|
|We want v to light up all the Ps at the same time as it lights up one of the Qs. If we find a v that does NOT do this; that is, we find a v that lights up all the Ps, but doesn't light up any of the Qs, we've found a falsifying assignment: in some sense, it's your "counter example." A sequent is valid if, and only if, it is satisfied by ALL truth assignments; that is, you can't find an assignment that falsifies it. (It should be evident that this is pretty hard to show!) Note there are a bunch of degenerate (but interesting) cases on page 2 of the description: you should now understand why these are true! For example, if there's a common proposition between the Ps and the Qs (an identical thing shows up on both sides: one of the Ps is also a Q!), then clearly, the sequent is valid. (Why? Well, no matter what, if all of the Ps are made true by some assignment, in particular, the P that is also a Q will be made true. Then you have a true Q, and you're done.) Make sure you read all of these cases and understand them! (Your little theorem prover could do checks for these cases and give really fast answers for them, if you wanted!) In light of this insight, the main idea is that we're going to try to go through a bunch of possible truth assignments (the vs!), and if we can't find any that falsify the sequent, then the statement is valid, and the process will produce a proof tree. Otherwise, we can return the falsifying truth statements. Yay!||
|3c: The Rules The rules of the Genzten Calculus are designed specifically so that the conclusion of the rule is falsified by a truth assignment v if any of its two presmises is falsified by v. The rules all work in both directions (which is why there's a left and right version of each rule), and they all basically just shift the Ps and Qs around in different ways. That's it! I'm not going to copy all the rules here because they're all on Page 3 of the project description. Remember, the greek letters are just placeholders representing finite sets of propositions we don't care about in that particular rule. Also, it's worth noting: order matters in the Genzten calculus. The scoping we did by discharging statements where they were used is gone in the Gentzen calculus, replaced (in essence, though this is kind of an oversimplification) by the ordering of the propositions.|
4: Putting it all together.
Alright. So. Let's put all the pieces together. We've got
|So it's pretty obvious when we've "won" the game. We apply the rules a few times, and all the leaves of our tree are axioms. Then the statement is valid. But what happens if that's not possible? There's another possibility: the sequents on the leaves of the tree could be made up of atomic propositions, and the intersection of the Ps and the Qs is empty (see Page 4 of the problem description). What happens if that's true? Well, if all the propositions are atomic, we can't apply any more rules: in some sense, everything's as simple as it can be, and if at this point the intersection is empty, none of the P's match with any of the Qs, which means the statement is falsifiable. These leaves are precisely the falsifying assignments: the P's that need to be "lit" which will produce no "lit" Qs. A sequent is "finished" if it's either of these two cases: either it's an axiom, or all the propositions are atomic and there's no overlap.||
|The kind of cool thing about the Gentzen proof system is that no matter what the sequent is, the process of building a deduction tree from that sequent will always terminate with a tree where all the leaves are finished. The order the rules are applied in doesn't matter! This also tells us that if we're just trying to find out of a proposition (or sequent) is valid, we can just stop as soon as one of the sequents we produce is "finished" and not an axiom, because we've just found a falsifying assignment.|
|5: The Answers "Alright, Alex, that's all well and good, but it's 1 AM and I really just want to know what the heck I have to do to finish this project so I can catch Carmen and go back to watching Glee." I'm sure that's what you're saying. Well, crankypants, here's some advice, because I've got more cheerful tooltips than an anthropomorphic paperclip. First, you need to do two proofs. Proof (1) is basically to prove the statement I just mentioned: that by applying these rules, we'll eventually end up with a deduction tree whose leaves are "finished." The hint should spoonfeed this to you. You just have to show that every time you apply a rule, your number of connectives STRICTLY decreases, which means that in a finite number of rule applications, you have to reach 0, which is "finished" (no more connectives).||
The second proof, (2), basically says that if a truth assignment
satisfies every leaf of a Tree generated from some sequent, it satisfies
that sequent, AND it says that if a truth assignment satisfies the sequent,
it must satisfy every leaf of the Tree.
The key here is to think about what the leaves of the tree
could possibly look like. They MUST consist of a subset of the propositions
from the original sequent, or some broken down version of them (depending on
how the rules were applied). You just have to show that if you set all the Ps
to be "on", and a Q is lit in the original sequent, then a Q is lit in all of
the leaves. Likewise, if a Q is lit in all of the leaves when all the Ps in the
leaves are lit, show that one of the Qs has to be lit in the original sequent.
The third part is the actual dreaded programming. On page 5,
Gallier does a nice job of setting out what exactly you have to do. He
suggests depth-first expansion, which means given a non-finished sequent,
you pull the leftmost non-atomic proposition, and apply the cases he
enumerates (He spells everything out for you on pages 6 and 7!) It's basically just
a big loop. Your terminating condition is set out, too: you stop when all the
leaves are axioms, or when you encounter a leaf in which all of the
propositions are atomic but there's no overlap in the sequent Ps and Qs.
See page 8 for a description of the input format. We'll be
using easier characters (& instead of that wacky wedge thing, | instead of
that wacky v thing, etc) for ease of typing, etc. Propositions are just
a character and then a number. Everything's separated by spaces.
The reason Gallier suggests postfix notation is that reading in
postfix makes parsing stuff a breeze. If you don't know what postfix is, here's
an explanation. Skip this if you know what postfix is.
Unless you're some kind of alien troll from Alternia, when you learned mathematics as a little maggot, you were taught INFIX notation: 3 + 4 You put the operator (in this case, '+') INbetween the two things it operates on (in this case, 3 and 4). This is all well and good for humans, but for computers, it kind of stinks. If a computer is reading left to right, it sees the 3, and doesn't know what the heck to do with it. It reads the +, and says, "oh, OK, I need to add the 3 to something. But what do I add it to? Luckily, in this case, it's just a 4. But what if it were (5 * 6)? It couldn't complete the addition until it had read more stuff. It's just kind of a mess. But if, instead, you write the operator AFTER the things it operates on 3 4 + There's a nifty thing you can do: as you read left to right, you can push each object onto a stack! (I hope you know what a stack is. If not, read the first paragraph here while I weep gently in a corner.) Then, when you start popping things off the stack, notice the first thing to come out is an operand! The computer says, "plus! OK, I know I'm going to get two more numbers off the top of the stack, and add them! So it pops the 4 and the 3 off, adds them, and pushes the reuslt, 7, back on the stack. DONE. For something more complicated... Let's write (5 * 6) + (2 / 1) in postfix: 5 6 * 2 1 / + The computer sees the +, and knows it needs to pop two more numbers off and add them together. But the first thing it pops is a /, which is not a number! So it knows it needs to pop two MORE things, divide them, and then push the result onto the stack, and then keep trying to pop two numbers off the stack (to satisfy the original +). So, it does that. It pops the 1 and 2 off, divides 2 by 1, and pushes the result (2) back on the stack. 5 6 * 2 It pops the two off (that's the first operand for the +) and tries to get the second. Oops! It's a *, which is not a number! Etc etc. Pop, pop, 5 * 6 = 30, push that back on, then pops that off, and we get 30 + 2 = 32, it pushes that on the stack, and it's done.
So that's why we're using postfix. It's easy to parse. Just push everything onto a stack. That takes care of input. Now, about output: Gallier is very vague on output. Obviously, each node of the tree is going to be a sequent, which is two lists connected by whatever your delimiter is (we mentioned semicolon earlier, because it's easy to print and it's the lonliest punctuation mark). And, somehow, you need to make the tree structure apparent. How you do that is up to you... but don't stress too much about it. If you've got the tree built in memory, printing it is easy! If you can't get stuff to fit nicely, you can always print a tree using numbers for the nodes: 1 2 3 4 \ / \ / 5 6 \ / 7 And then just have an index of the sequent in each node: 1: P1,P3,P6;Q5,Q8 2: P2,P3,;Q1,Q9,Q19 3: etc. That seems like a pretty simple way to do it. But any legible tree will do! And don't forget to output whether the statement is valid or not, and if not, what the falsifying asignment is!
Thanks for reading! I hope that helps some!