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.