# Homework Help: Proving a propositional logic formula

1. May 19, 2006

### twoflower

Hello all,

first I hope there's no problem putting this question here, since I didn't find any special forum dedicated to propositional logic.

I really have very basic question, I'm trying to prove

$$\vdash (A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))$$

I tried using instanciation second axiom, ie.

$$\vdash (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (B \rightarrow C))$$

But it doesn't seem to me very helpful :-/

Could you please give me a hint how to continue or where to start?

Thank you very much.

2. May 19, 2006

### AKG

What rules are you working with, i.e. what is your derivation system? It's a really easy one to prove.

3. May 20, 2006

### twoflower

It's first-order propositional logic, with three axioms

$$1) A \rightarrow (B \rightarrow A)$$
$$2) (A \rightarrow (B \rightarrow C)) \rightarrow \left[(A \rightarrow B) \rightarrow (A \rightarrow C)\right]$$
$$1) (\urcorner B \rightarrow \urcorner A) \rightarrow (A \rightarrow B)$$

and derivation rule modus ponens

$$\underline{A, A \rightarrow B}$$
$$B$$

4. May 20, 2006

### twoflower

Well, I tried it this way, using the deduction theorem.

$$\vdash (A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))$$
$$\Leftrightarrow (\mbox{Deduction theorem})$$
$$A \rightarrow (B \rightarrow C) \vdash B \rightarrow (A \rightarrow C)$$
$$\Leftrightarrow (\mbox{Deduction theorem})$$
$$B, A \rightarrow (B \rightarrow C) \vdash A \rightarrow C$$
$$\Leftrightarrow (\mbox{Deduction theorem})$$
$$A, B, A \rightarrow (B \rightarrow C) \vdash C$$

which is decidable (using modus ponens).

Anyway, expecially the end doesn't seem very fine to me, is this correct?

P.S.: Don't you happen to know about some collection of solved examples from propositional and predicate logic like this? (the examples where I have to prove some formula)

Thank you.

Last edited: May 20, 2006
5. May 20, 2006

### matt grime

You could of course just put the 8 possible T/F combinations of A,B and C in if you felt like it.

Any, way always remember that X => Y is exactly (~X) or Y, which makes the proof quite easy.

Last edited: May 20, 2006
6. May 20, 2006

### twoflower

This kind of proving is not accepted, I think..

Do you think my way is ok?

I'm just afraid I should start from axioms, but the deduction theorem seems to allow the way of proving (or rather showing that the formula is proveable) I used.

7. May 20, 2006

### matt grime

Why not? It is perfectly rigorous, it is just not a particularly useful method since it grows exponentially as an algorithm in the number of inputs. As long as the question does not specify how you should prove it, then any proof should be equally good.

Of course there is another way of doing it: the only thing to check is what happens if B=>(A=>C) is false which is when B is true, A=>C is false, or A is true C is false, but then A=>(B=>C) is also false so the implication is valid.

Last edited: May 20, 2006
8. May 20, 2006

### twoflower

Ok, I accept it's perfectly rigorous proof, but I would rather like to learn prove formulas using the definition of proof or at least using the deduction theorem. I tried it as I wrote and wonder whether it's correct.

And one more question: when proving formula in the first-order (propositional) logic with the three axioms and inference rule (modus ponens), may I use natural deduction rules without justification / proving them? Or is it another "formal system"?

9. May 20, 2006

### matt grime

There are many things you've not tried yet so don't give up. For instance

(A=>(B=>C)) => ( X => (A=>(B=>C))

for any X, so perhaps a well chosen one will help.

10. May 20, 2006

### AKG

I would think that unless it says you may use natural dedution rules, you may not. There are many deductive systems, and one that allows you to use those rules is a different system. Anyways, your proof looks right. I'm not sure if you can just say that the last sentence is satisfiable by modus ponens, but it certainly is. In fact, I'm sure you could easily show it, but it's just not clear as to how you would show such a thing using this deductive system. Doesn't your book have any examples on how proofs are done? It doesn't look like they're asking you to prove hard things, it looks like they're asking you to use a deductive system that is pretty bad for proving things (often, the good thing deductive systems that are bad at proving things is that it's easy to prove things about those deductive systems). Just find some examples (sorry, I don't know of any) to see how they actually expect you to implement modus ponens, and otherwise perform deductions.

11. May 20, 2006

### AKG

That's not an axiom he's been given. Of course, he can derive it easily from the second axiom he was given (assuming that the second axiom works for any sentences A and B, not just atomic sentences) but either way, I don't see how this would be of any use, no matter the choice of X.

12. May 20, 2006

### matt grime

yes it is, it is the first axiom he wrote down, isn't it? Not that I am claiming it to be useful.

13. May 20, 2006

### AKG

Yeah, sorry. When I said, "he can derive it easily from the second axiom," it's because a) I, for no reason I can explain, thought your middle "=>" was a turnstyle, and b) because my memory failed me and I didn't bother to scroll up to his post, so I thought A -> (B -> A) was given as the second axiom.

14. May 20, 2006

### twoflower

Well, there is just one formal proof done from definition and because the length of formal proof grows fast with complexity of formula which is to be proven, next proofs are not proof, but rather demonstration that the proof exists, using the deduction theorem.

Here's an example:

Prove $$\vdash \urcorner A \rightarrow (A \rightarrow B)$$

Demonstration:

$$\vdash \urcorner A \rightarrow (\urcorner B \rightarrow \urcorner A)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (a)\ \ \ \ \ instanciation of axiom (A1)}$$

$$\urcorner A \vdash \urcorner B \rightarrow \urcorner A\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (b)\ \ \ \ \ the deduction theorem}$$

$$\vdash (\urcorner B \rightarrow \urcorner A) \rightarrow (A \rightarrow B)\mbox{\ \ \ \ \ \ (c)\ \ \ \ \ axiom (A3)}$$

$$\urcorner A \vdash A \rightarrow B\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (d)\ \ \ \ \ (b), (c) MP}$$

$$\vdash \urcorner A \rightarrow (A \rightarrow B)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (e)\ \ \ \ \ the deduction theorem}$$

So that's an example how I'm supposed to do the proofs. Of course I could do a direct formal proof, but I think in most cases it's more complicated and lengthy.

Last edited: May 20, 2006
15. May 20, 2006

### AKG

Can you start a proof without instantiation of an axiom? For example, could you start a proof with:

$$A,\, (A \rightarrow B)\vdash B\ \mbox{MP}$$

For then you could just say:

$$A,\, (A\rightarrow (B\rightarrow C)) \vdash (B \rightarrow C)\ (\mbox{MP})$$

$$B,\, A,\, (A\rightarrow (B\rightarrow C)) \vdash C\ (\mbox{Deduction theorem})$$

$$B,\, (A\rightarrow (B\rightarrow C)) \vdash (A\rightarrow C)\ (\mbox{Deduction theorem})$$

$$(A\rightarrow (B\rightarrow C)) \vdash (B\rightarrow (A\rightarrow C))\ (\mbox{Deduction theorem})$$

$$\vdash (A\rightarrow (B\rightarrow C)) \rightarrow (B\rightarrow (A\rightarrow C))\ (\mbox{Deduction theorem})$$

the last few lines being nothing more than what you did in post 4

If not, then you can actually use matt grime's suggestion:

$$\vdash ((A \rightarrow (B\rightarrow C)) \rightarrow (A\rightarrow (A\rightarrow (B\rightarrow C))))\ \ \mbox{(a)}\ \ \ \mbox{A2}$$

$$(A \rightarrow (B\rightarrow C)) \vdash (A\rightarrow (A\rightarrow (B\rightarrow C)))\ \ \mbox{(b)}\ \ \ \mbox{(a)+Deduction theorem}$$

$$A,\, (A \rightarrow (B\rightarrow C)) \vdash (A\rightarrow (B\rightarrow C))\ \ \mbox{(c) }\ \ \ \mbox{(b)+Deduction theorem}$$

$$A,\, A,\, (A \rightarrow (B\rightarrow C)) \vdash (B\rightarrow C)\ \ \mbox{(d)}\ \ \ \mbox{(c)+Deduction theorem}$$

$$A,\, (A \rightarrow (B\rightarrow C)) \vdash (B\rightarrow C)\ \ \mbox{(e)}\ \ \ \mbox{removing repeat A}$$

Last edited: May 20, 2006
16. May 20, 2006

### twoflower

Thank you, I like your way more, because you start with obvious modus ponens and end up with exactly what had been to prove, whereas I wasn't sure how to finish it to be rigorous.

If we don't insist on following the strict schema of formal proof, it would be ok. So...I think it's acceptable way.

17. May 20, 2006

### AKG

I edited that last post - in particular I added some stuff that might satisfy even the strict schema of formal proof.

18. May 20, 2006

### twoflower

Now that's perfect :) Thank you AKG and Matt!

19. May 20, 2006

### twoflower

Uhm, I got stuck on another ones :-/

First one:

$$\vdash ((A \rightarrow B) \rightarrow (A \rightarrow C)) \rightarrow (A \rightarrow (B \rightarrow C))$$

So I tried

$$\vdash (A \rightarrow B) \rightarrow (A \rightarrow C)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ hypothesis}$$

$$A \rightarrow B \vdash A \rightarrow C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}$$

$$A, A \rightarrow B \vdash C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}$$

$$A \rightarrow B \vdash B\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (modus ponens)}$$

Now I made a step I hope is correct but can't see how to justify it formally:

$$A, A \rightarrow B \vdash B \rightarrow C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem?)}$$

$$A \rightarrow B \vdash A \rightarrow (B \rightarrow C)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}$$

That's almost what I got to obtain, but I don't know what to do with it now...

And the second one follows:

$$\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$$

I tried:

$$\vdash (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (axiom (A2))}$$

$$A \rightarrow (B \rightarrow C) \vdash (A \rightarrow B) \rightarrow (A \rightarrow C)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}$$

$$A \rightarrow B, A \rightarrow (B \rightarrow C) \vdash A \rightarrow C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}$$

$$A, A \rightarrow B, A \rightarrow (B \rightarrow C) \vdash C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}$$

But I really don't know if it's the right idea...

Could someone show me the way?

Thank you very much.

20. May 20, 2006

### AKG

I'm not an expert, but I get the impression that deductive systems with few axioms/rules of inference are only useful because it is easiest to prove things about them (e.g. completeness). Systems that are useful for proving things have more axioms/rules of inference. If you can show once that a system with few rules is equivalent to a system with many rules, then all the nice properties that you can prove true for the "lean" system will also hold for the equivalent, heavier system.

In one such "heavy" system, the thing you were originally asked to prove can be proven in about six lines, does not require the deduction theorem, and most importantly, the proof is very easy and intuitive - it would be the first thing you think to do.

Now I don't know how you're using "hypothesis", but strictly speaking, it isn't one of your axioms/rules of inference. In the "heavy" system I was talking about, they make use of something like "hypothesis", but I don't know if you're doing that here. What are you doing, and are you sure it's legal?

On your fourth line, you have $A\rightarrow B \vdash B\ \ \mbox{modus ponens}$. This is wrong - perhaps you meant $A, A\rightarrow B \vdash B$?

Anyways, if you have

$$A, A\rightarrow B \vdash C$$

and all you want is

$$A, A\rightarrow B \vdash B \rightarrow C$$

then I think you can go:

$$A, A\rightarrow B \vdash C$$

$$B, A, A\rightarrow B \vdash C$$

$$A, A\rightarrow B \vdash B \rightarrow C$$

The last line was justified by deduction theorem, the second being justified from the fact that if $\Sigma \vdash \Delta$ and $\Sigma \subseteq \Gamma$ then $\Gamma \vdash \Delta$. I would hope you're allowed to use that kind of justification. You claimed to justify it using deduction theorem, but it doesn't follow. I.e. the step which you hope to have correct doesn't seem formally correct.