The Gentzen system

I'm struggling a bit with the definition of a Gentzen system presented in the textbook on page 45. Please help.

What do the bits above & below the lines mean after the first paragraph? It looks like division, but can't be (I think). How would one read those formulae/expressions? I did see the bit that says the bit above the line is called a premise and the bit below the line a conclusion but what does it mean? How do I use what is presented there?

The other bit that is confusing is: "The axioms are the sets of formulas containing a complimentary pair of literals". Which formulas? Any formula? Like can I start a proof of P -> Q with a, �a (even though a is not an atom in P or Q)?

I can follow the example proofs but, because of this lack of clarity, cannot see how I would begin one of my own. (Other than maybe to construct the tableaux for the formula's compilment and then write the proof down from that.

Any clarity at all would be most welcome.

have you done any undergrad formal logic? If you haven't , then in my honest opinion you are going to struggle with this course.

premise is what you start off with and conclusion is what you end up with. The gentzen system is most definitely not division

premise (start bit)
_____________________
conclusion (bit you end up with) - its just notation. or maybe thats where I went wrong before....

I think the best way to do the gentzen stuff is to actually do the tableaux and then do the gentzen thing as the negation of your tableaux. If you try to just start the gentzen proof then you are going to take long time to get nowhere and totally frustrate yourself.

Thanks Celene,

Perhaps the bit that's really getting me is what you are allowed to choose as an axiom. Does it really say that you can choose _any_ complimentary pair of literals and not any pair that occurs in the formula or some sub formula? And why do they make the choices they do in the examples?

I can totally see how to create a proof from the tablueax but from the explanation of why the system exists it seems that there will be times that the tablueax is too large to search and that finding a proof in the Gentzen system would be faster.

And besides, I just want to know how it _all_ works...

BTW You seem to have been on every forum I've participated in in the last 10 years of study - do you work there or do we just happen to have very similar lines of study?

probably very similar lines of study I have been around since 98

I guess you can choose any complimentary pair of literals as long as they lead to the thing you want to prove - thats why they say you should use the upside down tableaux - they should not really be all that big?? the biggest ones I have seen in cos405 had 4 closed branches at the bottom - so those 4 pairs of negated literals would be your starting axioms for gentzen, and then you just work backwards to the thing you want to prove

I have never been clever enough to do the gentzen without the tableaux - and the ones for cos407 will never be too big.

thanks

There is no way a Gentzen proof will ever be easier through the thumb-suck approach rather than using a tableaux to determine its steps... unless.....

you are autistic.

If not, don't even try... unless you like hating the course.

 
  ,= ,-_-. =.
 ((_/)o o(\_))
  `-'(. .)`-'
      \_/

http://ilanpillemer.com
Entia non sunt multiplicanda praeter necessitatem