Questions: Natural Deduction for Propositional Logic

Question 1

To apply →-introduction (the rule for concluding φ → ψ), you must:

• A. Assert both φ and ψ as independent premises
• B. Derive ψ under the temporary assumption of φ, then discharge that assumption
• C. Find a proof of ψ from an empty set of assumptions
• D. Apply modus ponens to an existing conditional statement

Answer: (B)

→-introduction works by opening a subproof: you temporarily assume φ, derive ψ within that scope, then close the subproof and conclude φ → ψ — with the assumption φ discharged (no longer in scope). This mirrors the informal pattern 'Suppose φ. Then ... so ψ. Therefore φ → ψ.' The other options describe different operations that do not produce a conditional.

Question 2

In a Fitch-style natural deduction proof, once an assumption is written on a line it remains available for use anywhere later in the proof.

• T. True
• F. False

Answer: False

Assumptions have scope. When you close a subproof (e.g., to apply →-introduction or proof by contradiction), the assumption that opened that subproof is discharged and is no longer available on subsequent lines. Using a discharged assumption as a justification is a proof error. This scoping is one of the features that makes natural deduction match informal reasoning, where 'suppose' clauses have limited scope.

Question 3

What is the structural difference between an introduction rule and an elimination rule in natural deduction?

Model answer: An introduction rule concludes a formula whose main connective is the connective in question (it builds complexity: e.g., ∧-intro derives φ ∧ ψ from φ and ψ separately). An elimination rule starts from a formula with that connective as its main operator and derives something simpler (it reduces complexity: e.g., ∧-elim derives φ from φ ∧ ψ). Together, each connective's intro and elim rules define what that connective means within the proof system.

This intro/elim pairing is the design principle of natural deduction. Prawitz observed that a 'detour' — introducing a connective only to immediately eliminate it — is always reducible to a shorter proof, which gives natural deduction its normalization theorem. The symmetry between introduction and elimination also corresponds to the Curry-Howard correspondence between proofs and programs.