Announcements Last Post
Announcement SoC Curricula 09/30/2017 01:08PM
Announcement Demarcation or scoping of examinations and assessment 02/13/2017 07:59AM
Announcement School of Computing Short Learning Programmes 11/24/2014 08:37AM
Announcement Unisa contact information 07/28/2011 01:28PM
The Gentzen system
March 28, 2008 12:51PM
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.
Anonymous User
Re: The Gentzen system
March 28, 2008 02:43PM
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.
Re: The Gentzen system
March 28, 2008 03:25PM
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?
Anonymous User
Re: The Gentzen system
March 31, 2008 07:47AM
probably very similar lines of study smiling smiley I have been around since 98 confused smiley

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 smiling smiley

I have never been clever enough to do the gentzen without the tableaux - and the ones for cos407 will never be too big. smiling smiley
Re: The Gentzen system
March 31, 2008 10:14AM
avatar Re: The Gentzen system
April 01, 2008 01:58PM
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(\_))
  `-'(. .)`-'
Entia non sunt multiplicanda praeter necessitatem
Sorry, only registered users may post in this forum.

Click here to login