# Formal Proof - premises and conclusions

So I'm learning about formal proof and understand the beginning steps. However, after I'm given an argument and conclusion, I then don't understand how to do the actual formal proving. For example:

Premises: $$P \Rightarrow Q, P \wedge R$$.

Conclusion: $$Q$$.

The first two steps are the two premises. Step three says "$$P$$ (2. Simplification)" and step four says "$$Q$$ (1,3. Modus Ponens)".

What I don't understand is how do you get the correct inference rules and what do the numbers mean?

• The numbers are telling you which steps to look at for the antecedents of the inference rule. How to find a proof is in general something you have to learn by experience. – Rob Arthan Jan 28 at 21:19
• @RobArthan so for this example how do I know that the first is meant to be simplification. And then what does that 2. mean in regards to the simplification inference – JavaScr Jan 28 at 21:26
• The proof tells you that the first step is by simplification. Knowing that that is the right thing to is something you have to learn by experience. The 2 means that you are simplifying the result of the second step in the proof, namely the premise $P \land R$. – Rob Arthan Jan 28 at 21:54
• Ok right thats the answer i seemed to come up with, but then got confused with the 1,3. And with another example the premise didnt match the rule of inference – JavaScr Jan 28 at 22:06
• @JavaScr That the other example didn't match the rule of inference is possibly due to the rule being stated in terms of $P$'s and $Q$'s .... but obviously the $P$'s and $Q$'s could just as well have been $A$'s and $B$'s; as long as the example follows the abstract form of the rule, the rule can be used, which is why this is called formal proof. So, for example, Modus Ponens may be defined by your book as "you can infer $Q$ from $P \rightarrow Q$ together with $P$", but that rule allows you also to infer $C \lor D$ from $(A \land B) \rightarrow (C \lor D)$ together with $A \land B$ – Bram28 Jan 28 at 23:35

The proof contains four lines:

1. $$P ⇒ Q$$ (Premise)
2. $$P ∧ R$$ (Premise)
3. $$P$$ (2. Simplification)
4. $$Q$$ (1,3. Modus Ponens)

The question is:

What I don't understand is how do you get the correct inference rule and what do the numbers mean.

The 2 in the third line means that this third line references the second line containing $$P ∧ R$$. You only need $$P$$ from the second line, but you have to use an inference rule to access it. The rule is called Simplification.

The 1,3 in the fourth line means this line references lines 1 and 3. Line 1 contains a conditional $$P ⇒ Q$$ and line 3 is the line we just derived. It contains the antecedent of the conditional, $$P$$. The Modus Ponens rule says that if we have a conditional and its antecedent we can derive the consequent or $$Q$$. Since this is the goal of the argument, it is finished.

It takes practice to know what the inference rules are and which ones to use to reach a particular goal. It is sometimes useful to have a proof checker to guide one. Here is the argument in the Open Logic Project proof checker:

These proofs are not exactly the same, but they are very similar. They both use rules of classical propositional logic. Instead of Simplication this rule in this proof checker is called conjunction elimination abbreviated by ∧E. The referenced line 2 is the same. Instead of Modus Ponens the rule is called conditional elimination abbreviated by →E. Again the referenced lines, 1 and 3, are the same.

The benefit of using a proof checker is you can get immediate feedback on whether you are using the rules correctly or not as well as confirmation when the proof is complete. Links to the proof checker and the accompanying textbook are below.

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, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf