Thread: Proof of p implies (q implies p)

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?

Please help.
Thank you.

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?

Hey,

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.

How does your conditional proof work? What is its schema?

This is conditional proof:


I will look into it further.
Thank you all.

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?

Originally Posted by harriette

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.

How do we know that REPEAT is a rule??

How do we know that REPEAT is a rule??

The OP has the derivation of p -> (q -> p) where the right column seems to list the rules applied at each step, and REPEAT is one of them. Why are you asking?

Originally Posted by emakarov

The OP has the derivation of p -> (q -> p) where the right column seems to list the rules applied at each step, and REPEAT is one of them. Why are you asking?

I meant to say how do we prove that REPEAT is a rule??

That's usually an axiom schema; that is, it's not usually something you have to prove. It's usually assumed. In this case, it's definitely assumed you can just do that.

Originally Posted by Ackbeet

That's usually an axiom schema; that is, it's not usually something you have to prove. It's usually assumed. In this case, it's definitely assumed you can just do that.

I hardly know of any axiom schema that uses the rule REPEAT as one of its axioms.

Anyway we can prove De Morgans ,can we not??

What kind of truth table will validate REPEAT as a tautology?

Alex,

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.
Sam

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.

Originally Posted by roberts

Alex,

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.
Sam

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.

You mean p->p ,is REPEAT??

No, I mean p -> p is an axiom which stands to the /rule/ of repeat just as p -> [(p -> q) -> q] stands to the /rule/ of modus ponens.

Sam

(In my previous post I stated MP's associated axiom wrongly; that's now been corrected.)