5  Natural deduction

Our natural-deduction proof system is a syntactic device governed by a set of rules for transforming formulas, called rules of transformation. These rules are distinguishable into:

• direct rules, which do not require subproofs, and
• indirect rules, which require subproofs.

For the sake of convenience, we can distinguish between:

• one-line direct rules,
• two-line direct rules,
• one-subproof indirect rules, and
• two-subproof indirect rules.

All of the rules are applicable to SL and FOL. The quantifier rules are applicable just to FOL.

For each rule, we will give:

• the proof-formal syntax
• a sample instance
• a summary of:
  • whether and what sort of subproof is needed
  • the number and kinds of line(s) cited in the justification
  • the number and kinds of source(s) necessary to use the rule
  • the kinds of product derivable when using the rule
  • the formal syntax of the rule

5.1 Sample proof

Here is a sample proof with its parts named and described below.

This proof is a demonstration that:

\[\{ (P \wedge Q), (Q \to R)\} \vdash (P \wedge R)\]

• The two formulas above the horizontal line are the premises
• “want \((P \wedge R)\)” is simply a note of the intended target of the proof
  • “Target” in this context means: desired last line
• Lines 1–2 are the setup of the proof
• ‘\(P\)’, ‘\(Q\)’, ‘\(R\)’, and ‘\((P \wedge R)\)’ (i.e., lines 3–6) are derived formulas.
• Each derived line gets a justification. A justification includes:
  • A rule
  • A line number or line numbers
    • E.g., the justification in line 5 (‘\(\to\)E \(2, 4\)’) is comprised of:
      • the \(\to\)E rule, and
      • line numbers \(2\) and \(4\)