Time to trot out emakarov's standard question in these sorts of situations: what inference rules are you allowed to use, and what are you calling them?
How do I prove this?
I did the truth table, and I understand it, but I don't understand the proof in Cauman's book First order logic. Actually, I don't see how it makes sense.
Here's what she did:
How do I get just by two premises I introduced and repeated one of them?
If you are assuming p and q in the proof, then you can prove p (because you are assuming it!). So, from p and q you can prove p in particular. Using conditional proof we can discharge one of our assumptions, in this case either p or q. So discharge q. Thus we have a proof of q -> p from p. Then you apply conditional proof again to get a proof of p -> (q -> p) from no assumptions.
Hope this helps.
PREM in proof stands for premise, REPEAT is repeating a premise, CP stands for conditional proof.
There are other rules, but I would really like to understand this proof first and then try to find others.
Do I need to explain any of the rules above?
Thank you very much for your help and sorry for my English.
So, lines 2 and 3 appear to be a "sub-proof", as in the Fitch-style proof. You temporarily assume q. You can inject outside assumptions into a subproof, which gives you line 3. Then, because of the CP schema, you can now conclude q -> p. Line 4 is now back to the same proof-level as line 1. Then you just use CP again to get the conclusion. Does that help?
Repeat isn't an axiom, it's a rule of inference, much like modus ponens. We cannot state modus ponens as an axiom (assuming we have no other rules of inference), because we wouldn't be able to draw any inferences from it. Of course, MP has an associated axiom, i.e. p -> [(p -> q) -> q], but then so does repeat, i.e. p -> p (which is clearly tautologous).
The rule of repeat usually isn't even stated as a rule, it is given as part of the definition of a proof, i.e. a proof from \Gamma to \phi is a finite sequence of formulas such that each member of the sequence is either an axiom, a member of \Gamma (REPEAT), or derived from other previous members of the sequence by means of some rule (which, in hilbert style presentations is simply MP).
Hope this helps.
Correction: MP is an axiom of the proof-theory, but it's not a logical axiom. But in the proof-theory it's also an axiom that \Gamma implies phi for all phi in \Gamma.