# Having trouble starting a proof

I am given the following premise:

( Q --> R )

and the following conclusion

(( ~ Q --> ~ P ) --> ( P --> R ))

I am allowed to use Modus Pollens, Modus Tollens, Hypothetical Syllogism, Simplification, Conjunction, Addition, Disjunctive Syllogism, Constructive Dilemma, and Double Negation rules as well as assuming the antecedant of conclusion is true (CPA), no other rules can be used.

Clearly, the premise doesnt give me enough to work with, so I start with an assumption...

1. ( Q → R ) / (( ~ Q → ~ P ) → ( P → R ))
2. | ( ~ Q → ~ P ) CPA

Problem is, I am completely stumped on where to start from here... Dont need a whole solution, just the next step or two would be helpful...

``` 1. (Q->R) -- Premise
2.  (~Q->~P) -- CPA
3.  P -- CPA
4.  Q -- (2, 3, MT)
5.  R -- (1, 4, MP)
6. (P->R) -- (3-5, CP)

C. (~Q->~P)->(P->R) (1-6, CP)
```

Adding this to present a proof using only the rules the OP can use.

If someone could edit the second 3 to be a 6, that would be greatly appreciated. I'm having trouble doing it myself.

Clearly, the premise doesnt give me enough to work with, so I start with an assumption...

``````|_ ( Q → R )                .: (( ~ Q → ~ P ) → ( P → R ))
|  |_ ( ~Q → ~P ) CPA
``````

Problem is, I am completely stumped on where to start from here... Dont need a whole solution, just the next step or two would be helpful...

As asked the next step is to assume P aiming to derive Q so that and the premise will derive R.

`````` |_ ( Q → R )                .: (( ~ Q → ~ P ) → ( P → R ))
|  |_ ( ~Q → ~P )           CPA   (Conditional Proof Assumption ?)
|  |  |_ P                         Same
:  :  :  :
:  :  :  :
|  |  |  Q
|  |  |  R
|  |  P → R
|  (~Q → ~P) → (P → R)
``````

To fill in the details, I am sure you would be able to work out how to use your first assumption to derive Q from P.

The proof is similar to Another logic proof problem I'm stuck on :( but since there was confusion there, I am proving it using the same Fitch-style proof checker to provide another example: Note that the goal is a conditional. So, I assume the antecedent of the conditional, ¬Q→¬P, as the beginning of a subproof. I did this on line 2. The indent is how the Fitch-style keeps track of subproofs showing where they start and end.

In that subproof I must derive the consequent, P→R. If I can do that, then I can discharge the subproof and place the derived answer outside the indented subproof. The derivation occurred on line 10. Using conditional introduction, I discharged the assumption and closed the subproof on line 11.

But not only is the goal a conditional, the consequent of the goal, P→R, is also a conditional. So I have to derive its consequent, R, within the subproof. So I make another assumption, P, on line 3 and start a sub-subproof. I try to derive R, which I do on line 9. Then I discharge the assumption on line 3 and close this sub-subproof on line 10.

See the links below for the proof checker and a text describing the rules.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018.