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 proof contains four lines:
The question is:
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