Natural Deduction·Intermediate·5 lessons·62 practice activities·~300 min
Natural Deduction: Validity and Formal Proof
Why some conclusions follow necessarily
What you'll learn
By the end of this unit, you can…
- Distinguish validity from truth.
- Symbolize argument.
- Construct short proofs.
- Diagnose invalid step.
Lessons
Lesson sequence
- 1Open →
Validity vs Truth
Introduces the difference between validity, truth, and soundness, and trains students to judge the form of a deductive argument separately from the truth of its claims.
- 2Student Pro
Symbolizing Propositional Arguments
Teaches students how to translate short arguments from ordinary language into propositional notation with a clear sentence-letter key.
- 3Student Pro
Basic Natural Deduction
Introduces core natural deduction inference rules and trains students to build short, fully justified line-by-line proofs.
- 4Student Pro
Diagnosing Invalid Proof Steps
Students inspect flawed derivations and explain exactly why the steps fail, naming the mismatched condition of the rule being misused.
- 5Student Pro
Capstone: Building and Defending a Complete Deductive Argument
An integrative lesson that asks students to move through the full cycle of deductive evaluation: read an argument in ordinary language, symbolize it, classify its validity, either prove it or refute it with a counterexample, and then explain the result in plain English.
How to study
Three moves that work for this unit
Read the explanation
Each lesson opens with a guided walkthrough — read it before the activity.
Study the worked example
Look at why each step follows, not just what the answer is.
Practice with the target in mind
Know which rule applies and what would make the response weak before you start.
Reference materials
Optional context for the unit. Each lesson surfaces the concepts and rules it uses — these are here when you want the bigger picture.
Concept map (6 terms)
Validity
The property of an argument whose conclusion cannot be false while all its premises are true.
Soundness
A deductive argument is sound when it is valid and all of its premises are true.
Entailment
A relation in which the premises, taken together, guarantee the conclusion.
Proof
A rule-governed derivation showing that a conclusion follows from a set of premises.
Subproof
A nested section of a proof used to track assumptions and scope in conditional or indirect derivations.
Counterexample
A situation in which the premises of an argument are all true while the conclusion is false.
Rules and standards (8)
- Modus Ponens. From 'P → Q' and 'P', one may derive 'Q'. Common failures: The student affirms the consequent by deriving 'P' from 'P → Q' and 'Q'.; The student derives 'Q' from 'Q → P' and 'P' after confusing the direction of the conditional..
- Modus Tollens. From 'P → Q' and '¬Q', one may derive '¬P'. Common failures: The student denies the antecedent by deriving '¬Q' from 'P → Q' and '¬P'.; The student ignores the conditional's direction when the negation is placed on the consequent..
- Hypothetical Syllogism. From P -> Q and Q -> R, infer P -> R. Common failures: The chained conditionals do not actually share a middle term.; The derived conditional swaps antecedent and consequent..
- Disjunctive Syllogism. From 'P ∨ Q' and '¬P', one may derive 'Q'; similarly from 'P ∨ Q' and '¬Q', one may derive 'P'. Common failures: The student derives the negated disjunct instead of the remaining disjunct.; The student assumes an exclusive disjunction and draws an unlicensed inference about the second disjunct..
- Conjunction Introduction. From P and Q, infer P & Q. Common failures: One of the conjuncts was not established on a prior line.; The conjunction changes the content of the cited lines..
- Conjunction Elimination. From P & Q, infer either P or Q. Common failures: The cited line is not a conjunction.; The derived statement is not one of the conjuncts..
- Conditional Introduction. If assuming P lets you derive Q within a subproof, you may discharge the assumption and infer P -> Q. Common failures: Discharging the assumption before Q has actually been derived.; Using lines from inside a closed subproof after its assumption has been discharged..
- Necessity Standard. A deductive conclusion must follow necessarily from the premises, not merely appear plausible. Common failures: The student defends a conclusion on the basis of plausibility alone.; The student confuses a likely conclusion with a logically guaranteed one..
Formalization patterns (3)
- Sentence-Letter Translation. From natural_language_argument to symbolic_argument — Identify the atomic statements in the argument.; Assign a sentence letter to each distinct atomic statement.; Identify the logical connectives in each premise and the conclusion.; Translate each premise and the conclusion into symbolic form.; Check that the symbolic form preserves the original logical structure..
- Natural Deduction Proof Format. From symbolic_argument to line_by_line_proof — List the premises as the first numbered lines.; State the target conclusion.; Add justified lines one at a time, citing the rule and the prior lines used.; Open a subproof whenever you need to make an assumption.; Close each subproof by discharging its assumption with the appropriate rule.; Verify that the final line matches the intended conclusion and that every citation is in scope..
- Counterexample Construction. From symbolic_argument to row_of_truth_values — List the atomic letters that appear in the argument.; Search for an assignment of truth values that makes every premise true.; Check whether that same assignment also makes the conclusion false.; If such an assignment exists, present it as the counterexample..
Full mastery and assessment guidance
Mastery requirements
- Distinguish validity from truth. Percent Consistent · 80_percent_consistent
- Symbolize argument. Successful Translations · 6_successful_translations
- Construct short proofs. Successful Proofs · 4_successful_proofs
- Diagnose invalid step. Successful Error Analyses · 3_successful_error_analyses
Assessment advice
- Am I evaluating the structure of the argument or the truth of the claims?
- Would the conclusion have to be true if the premises were true?
- Can I build a scenario that makes the premises true and the conclusion false?
- Letting agreement with the conclusion decide the validity verdict.
- Treating unsoundness as the same thing as invalidity.
- Did I preserve the argument's logical form?
- Did I assign sentence letters consistently?
- When I read the symbolic version back in English, does it match the original argument?
- Letting the surface grammar decide the direction of a conditional.
- Inventing letters that appear only once and add nothing.
- Do the cited lines match the rule pattern exactly?
- Does my derived line contain only what the rule allows?
- Is every assumption I opened eventually discharged?
- Copying the structure of a previous proof without checking citations.
- Treating any plausible-looking line as a legal rule application.
- Can I state which condition of the rule failed?
- Can I identify the exact mismatch between the cited lines and the derived line?
- Have I decided whether a legal repair is actually possible?
- Replacing the bad line with a correct one without explaining the original failure.
- Naming a rule by sound rather than by pattern.
- Did I produce all four outputs for each case?
- Did I decide whether to prove or refute before I started writing the proof?
- Does my plain-English explanation make sense to someone who does not know the notation?
- Burning time on a proof attempt for an invalid argument.
- Forgetting that the output of deductive evaluation is a communicable result, not just a proof.
Historical context (3)
- Aristotle. Systematized formal inference and validity by argument structure rather than by content. Argument-form analysis and structural validity tests.
- Gottlob Frege. Developed modern formal language and quantificational logic, separating grammar from logical form. Symbolic formalization and precise logical notation in proof assistants.
- Gerhard Gentzen. Developed natural deduction systems centered on introduction and elimination rules. Subproof-based proof editors and line-by-line derivation systems.