How to start a formal proof in symbolic logic?

[Maggie]

When it comes to formal proofs I have no idea how to even start it. When do I use a subproof and how to use it? Can someone please explain to me when to use a subproof and how to start a formal proof? Please and thank you.

This is what I have so far...and I have no idea what to do next...

 

[John]

I'm not sure what that program is, but I'm assuming

[math]\neg F \implies (G \vee H)[/math],

[math](F \vee G) \implies (I \wedge J)[/math], and

[math] I \iff \neg K[/math]

 

are propositions you can take to be true, and thus your goal is to use these to show that [math]K \implies H[/math]. Is that correct?

Is the problem that you don't see how to work from K to H, or is it that you're not sure how to express the proof using this program?

Edited December 19, 2013 by John

[Maggie]

I'm sorry, the program is called Fitch.

And my problem is I do not know how to start a proof...I don't know what subproof does. If I was asked to write the proof out on a piece of paper I would have no idea how. Using the program helps to check my steps as you can see above. However I just don't understand the proof process. And yes, I don't see how to work from K to H...

[John]

Hm. Well, the way a proof works in general is we start with some assumptions, and using new conclusions we can logically deduce from those assumptions (and further conclusions we can logically deduce from those conclusions, and so on), we work towards some end goal.

So for this proof, our assumption is that [math]K[/math] is true. We also have that [math]I \iff \neg K[/math]. Since [math]K[/math] is true, what do we know about [math]\neg K[/math]? And what does this tell us, given our biconditional?

Edited December 19, 2013 by John

[Maggie]

We know that K and ¬K is a contradiction?

[John]

Well, since [math]K \wedge \neg K[/math] is a contradiction, and [math]K[/math] is true, what do we know about [math]\neg K[/math]?

[Maggie]

¬K is false...?

[John]

Yes, and given that [math]I \iff \neg K[/math], what does this tell us?

[Maggie]

Ohh...if ¬K is false that means I ↔ ¬K is false because I if only if ¬K.

[John]

Almost. The biconditional is true by assumption. Since [math]\neg K[/math] is false, the fact that [math]I \iff \neg K[/math] tells us [math]I[/math] is false.

[Maggie]

Ok...so I need to assume and get a contradiction?

[John]

No. You've got the assumptions listed above, and you're assuming K is true. Starting with the assumption that K is true, you have to reason your way through the other assumptions you have to arrive at the conclusion that H is also true. This will prove that K implies H.

So far, we've seen that since K is true, ~K must be false. And since ~K is false, I must also be false. Now given that I is false, what can we conclude, given the various other statements we assume to be true?

Edited December 19, 2013 by John

[Maggie]

If I is false then the second premise (F ∨ G) → (I ∧ J) must be false because I and J both have to be true for (F ∨ G) to be true?

[John]

Almost again, heh. Remember that [math](F \vee G) \implies (I \wedge J)[/math] is true by assumption. You're on the right track, though.

[Maggie]

Ok...I am not quite sure where I'm going with this...Could you be more specific?