Natural Deduction

This is Unit Five of Logic: Natural Deduction. Unit Four gave you a machine that decides validity by exhausting every possibility. It works perfectly and it does not scale — each extra letter doubles the table, and at six letters you are checking sixty-four rows by hand. Proof does something different. Instead of checking every way the world could be, it builds a path from the premises to the conclusion, one guaranteed step at a time. If every step is safe, arriving is safe. Tables confirm; proofs construct. Two families of rule do the work. One family moves forward from whole lines. The other swaps equivalent forms in either direction and reaches inside a line to do it. Then two techniques that let a proof assume something it has not got, use it, and then give it back. Almost every mistake in this unit has the same shape, and the unit names it outright: a perfectly good rule, applied where its conditions do not hold. By the end you will be able to do five things. One: write a proof line with a justification naming the rule and the lines it came from. Two: apply an implication rule only where its conditions actually hold. Three: say how the second family of rules differs in direction and in reach. Four: prove a conditional by assuming its antecedent and discharging. Five: prove a statement by assuming its denial and forcing a contradiction.

Two entries of groundwork. A proof is a sequence where every line is either given or earned, and the earning has to be written down — because a line without a stated reason cannot be checked by anyone, including you.

The object.

Logic 191 What a Proof Is

A run of statements, each one either supplied at the start or produced from earlier ones by a rule known to be safe. Where every step holds, arrival holds — and for arguments with many letters this is far shorter than the table.

The bookkeeping.

Logic 192 Proof Notation

Every line gets a number, and every earned line names both the rule used and the lines it drew on. Without that, a line is not a step in a proof. It is something you would like to be true.

Four of the valid forms from Unit Four now become moves you may write down. Each carries a condition, and the conditions are what the rest of this unit will keep catching people on — the rule has to see a whole line of exactly the right shape.

The first move.

Logic 193 Modus Ponens as a Proof Move

Given a conditional and its condition on separate lines, write the result. The requirement: the conditional must be the entire line. One sitting inside a longer formula is out of reach of this rule.

The second.

Logic 194 Modus Tollens as a Proof Move

The denial has to match the result exactly. A statement and its denial are a pair; a statement and a doubled denial are not — not yet, anyway, and a later rule is what fixes that.

The third.

Logic 195 Hypothetical Syllogism as a Proof Move

The linking piece must match exactly: the result of one and the condition of the other, character for character.

The fourth.

Logic 196 Disjunctive Syllogism as a Proof Move

Rule out one alternative and the other is yours. Only by ruling out — the system will not let you affirm one side and discard the other, which is the twin from Unit Four, refused at the door.

Four moves that have no counterpart in Unit Four's argument forms. Two of them take a line apart and put lines together. One is available whenever you have anything at all, and it looks so generous that people assume it must be illegal.

Taking apart.

Logic 197 Simplification

From a line that joins two statements, write down either one. The condition is about which operator governs the whole line — where a joining sits inside something larger, this rule reaches nothing.

Putting together.

Logic 198 Conjunction

Two statements already established become one joined line. Assembly costs nothing, since both halves were already earned.

The generous one.

Logic 199 Addition

From anything established, write it alongside any statement whatsoever. It is not cheating: an alternative with one true side is true, no matter what rides along beside it.

And the packaged one.

Logic 200 Constructive Dilemma as a Proof Move

Two conditionals and a guarantee that one condition fires, yielding the alternative of the two results. The two conditionals have to arrive already joined into one line — loose, they need assembling first.

A proof is executed forward and planned backward, and those are genuinely different activities. The second entry here is the one that turns proof from guesswork into method — but it comes with a warning about what a plan actually entitles you to write.

Watch one run forward.

Logic 201 First Proof Walkthrough

Each line gets its rule and its sources named as it goes down. The trap arrives immediately: the taking-apart rule works on a line governed by the joining operator and on nothing else, and a conditional is not that.

And watch one get planned.

Logic 202 Proof Strategy: Working Backward

Read the conclusion, ask what single move would produce it, then treat that as the next thing to obtain, working back until the requirements reach the premises. But identifying what you need is not permission to write it — a goal is not yet a line.

Everything so far runs one way and operates on whole lines. The second family does neither, and that difference in reach is precisely why the system needs both — some proofs are unreachable with forward moves alone.

The second family.

Logic 203 Replacement Rules: The Concept

These swap forms known to be interchangeable, running either way, and they apply to a fragment sitting anywhere inside a line. The first family runs forward only and needs the whole line.

Five rules for rearranging material you already have. The first is the one this unit gets wrong most often, and the last is so small that people skip learning it and then find themselves stuck without it constantly.

The rule to watch.

Logic 204 De Morgan's Rules

Denying that both passed says at least one failed. Denying that either passed says both failed. The denial spreads to each part and the operator changes as it does — and leaving the operator alone is this unit's standing mistake.

Order.

Logic 205 Commutativity

Joining and alternation do not care which side comes first. The conditional cares enormously — swapping its two sides is Unit Four's invalid twin, dressed up as a rule.

Grouping.

Logic 206 Associativity

Move the brackets freely as long as the operator throughout is the same one. Mixed formulas need the next rule instead.

The error-prone one.

Logic 207 Distribution

The outer operator spreads across both halves of the inner one, the way multiplication spreads across a sum. Write it out on the page. Never attempt it in your head.

And the small one.

Logic 208 Double Negation

It looks trivial and it is needed constantly, because two of the forward rules demand denials that match exactly — and this is the rule that manufactures a match where there was not one.

Five more, all concerned with conditionals, which are the hardest thing to work with directly. One of these is the great unblocker of the whole unit: when a conditional is useless because you cannot get its condition, this rule turns it into something you can attack.

The first.

Logic 209 Transposition

Hired implies vetted becomes not vetted implies not hired. Both moves are required together — negating without swapping, or swapping without negating, produces exactly the invalid twins from Unit Four.

The unblocker.

Logic 210 Material Implication

The equivalence Unit Four found in a table is now a move you may make. Stuck holding a conditional whose condition you cannot obtain, convert it and work the alternation instead.

Unpacking the two-way one.

Logic 211 Material Equivalence

The locking operator opens either into a pair of conditionals or into both-true-or-both-false. Pick whichever the proof can use — conditionals if you want forward moves, the alternation if you want to eliminate.

Unstacking a condition.

Logic 212 Exportation

Storm and outage together forcing closure becomes: storm forces that an outage forces closure. A joined condition unstacks into nested ones, which is useful right before the technique two topics from here.

And the one you will barely notice.

Logic 213 Tautology (Redundancy)

A statement repeated alongside itself collapses to the statement — or gets manufactured into the doubled form. It shows up at the end of dilemma proofs and nowhere else.

One proof, two routes to the same line, and the comparison is the point: the second family does not merely add convenience. It opens routes the forward rules cannot reach at all.

Watch both routes.

Logic 214 Proof Using Replacement Rules

Convert the alternation into a conditional and work forward, or leave it and eliminate. Both arrive. The difference is that the second family works in either direction and on any part of a line, while the first runs one way on whole lines only.

Now a technique that lets a proof help itself to something it has not established. You want a conditional, so you assume its condition, work under that assumption, and then hand it back — and handing it back is what makes it legitimate.

The technique.

Logic 215 Conditional Proof

Assume the condition inside an indented section, reach the result, then close the section and the conditional walks out onto the main line. Once closed, nothing inside may be cited again — the assumption is spent.

Watch it run.

Logic 216 Conditional Proof Walkthrough

Assume the condition, derive through to the result, then close. The lines produced inside were earned under something that is no longer being supposed, so they cannot be reached for afterwards, however true they looked.

The second technique assumes the opposite of what it wants and makes the assumption destroy itself. It is Unit Four's contradiction — false under every arrangement — turned into a tool. And it is what makes a proof from no premises at all possible.

The technique.

Logic 217 Indirect Proof

Assume the denial, reach an outright contradiction, then close — and the statement walks out. Any explicit contradiction will do; it need not involve the statement being proved. Absurdity is the point, not its subject.

Watch it run.

Logic 218 Indirect Proof Walkthrough

Assume the opposite, indent, work until a statement and its denial both stand, then close. The contradiction has to be written down as a line — noticing that two lines conflict is not the same as having derived the conflict.

And from nothing at all.

Logic 219 Proving Tautologies

Statements true under every arrangement need no premises: open with an assumption immediately, negate the target, spread the denial, and let it collapse. It looks impossible for about one entry's worth of time.

Five errors account for most failed proofs, and they share a single diagnosis worth stating plainly, because it changes how you look for your own mistakes. Then the unit's capstone, which uses both assumption techniques with one nested inside the other.

The five.

Logic 220 The Common Proof Errors

Taking apart what is not a joining; reaching into part of a line with a whole-line rule; citing lines from a closed section; affirming instead of denying; and leaving denials that do not match. Every one is a sound rule used where its conditions fail — the rules are never the problem.

The capstone. Planned backward, executed forward.

Logic 221 Capstone: A Mixed-Strategy Proof

Read the goal, work back to a plan, then run it forward with one indented section inside another — and close them in the order they opened. The lecture ends by finding a much shorter route using the second family of rules.

Five things you can now do. You can write a proof line properly: numbered, with the rule and the source lines named — because a line nobody can check is not a step, whatever it says. You can apply the forward rules where their conditions hold, and you know the conditions are the whole difficulty: a whole line of the right shape, denials matching exactly, and the linking piece identical on both sides. You can say what the second family adds — two directions instead of one, and reach into any part of a line instead of the whole of it — and you know the one that unblocks a stuck conditional. You can prove a conditional by assuming its condition and discharging, and you know that closing the section spends everything inside it. And you can prove a statement by denying it and forcing an explicit contradiction onto the page — including from no premises at all.