Proving a propositional logic formula

[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

<br /> \vdash (A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))<br />

I tried using instanciation second axiom, ie.

<br /> \vdash (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (B \rightarrow C))<br />

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.

 

[AKG]

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

 

[twoflower]

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

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

<br /> 1) A \rightarrow (B \rightarrow A)<br />
<br /> 2) (A \rightarrow (B \rightarrow C)) \rightarrow \left[(A \rightarrow B) \rightarrow (A \rightarrow C)\right]<br />
<br /> 1) (\urcorner B \rightarrow \urcorner A) \rightarrow (A \rightarrow B)<br />

and derivation rule modus ponens

<br /> \underline{A, A \rightarrow B}<br />
<br /> B<br />

 

[twoflower]

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

<br /> \vdash (A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))<br />
<br /> \Leftrightarrow (\mbox{Deduction theorem})<br />
<br /> A \rightarrow (B \rightarrow C) \vdash B \rightarrow (A \rightarrow C)<br />
<br /> \Leftrightarrow (\mbox{Deduction theorem})<br />
<br /> B, A \rightarrow (B \rightarrow C) \vdash A \rightarrow C<br />
<br /> \Leftrightarrow (\mbox{Deduction theorem})<br />
<br /> A, B, A \rightarrow (B \rightarrow C) \vdash C<br />

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.

 

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

 

[twoflower]

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

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.

 

[matt grime]

This kind of proving is not accepted, I think.

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.

 

[twoflower]

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.

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"?

 

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

 

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

 

[AKG]

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.

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.

 

[matt grime]

That's not an axiom he's been given.

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

 

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

 

[twoflower]

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.

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:

<br /> \vdash \urcorner A \rightarrow (\urcorner B \rightarrow \urcorner A)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (a)\ \ \ \ \ instanciation of axiom (A1)}<br />

<br /> \urcorner A \vdash \urcorner B \rightarrow \urcorner A\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (b)\ \ \ \ \ the deduction theorem}<br />

<br /> \vdash (\urcorner B \rightarrow \urcorner A) \rightarrow (A \rightarrow B)\mbox{\ \ \ \ \ \ (c)\ \ \ \ \ axiom (A3)}<br />

<br /> \urcorner A \vdash A \rightarrow B\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (d)\ \ \ \ \ (b), (c) MP}<br />

<br /> \vdash \urcorner A \rightarrow (A \rightarrow B)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (e)\ \ \ \ \ the deduction theorem}<br />

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.

 

[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 <br /> 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}

 

[twoflower]

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 <br /> 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

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.

 

[AKG]

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

 

[twoflower]

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

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

 

[twoflower]

Uhm, I got stuck on another ones :-/

First one:

<br /> \vdash ((A \rightarrow B) \rightarrow (A \rightarrow C)) \rightarrow (A \rightarrow (B \rightarrow C))<br />

So I tried

<br /> \vdash (A \rightarrow B) \rightarrow (A \rightarrow C)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ hypothesis}<br />

<br /> A \rightarrow B \vdash A \rightarrow C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}<br />

<br /> A, A \rightarrow B \vdash C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}<br />

<br /> A \rightarrow B \vdash B\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (modus ponens)}<br />

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

<br /> A, A \rightarrow B \vdash B \rightarrow C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem?)}<br />

<br /> A \rightarrow B \vdash A \rightarrow (B \rightarrow C)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}<br />

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

And the second one follows:

<br /> \vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))<br />

I tried:

<br /> \vdash (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (axiom (A2))}<br />

<br /> A \rightarrow (B \rightarrow C) \vdash (A \rightarrow B) \rightarrow (A \rightarrow C)\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}<br />

<br /> A \rightarrow B, A \rightarrow (B \rightarrow C) \vdash A \rightarrow C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}<br />

<br /> A, A \rightarrow B, A \rightarrow (B \rightarrow C) \vdash C\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ (the deduction theorem)}<br />

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

Could someone show me the way?

Thank you very much.

 

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