Propositional calculus - Natural Deduction and Formal Proof Systems

Natural Deduction: Rules and Proof Systems Introduction Natural deduction is a proof system designed to mirror the way mathematicians and logicians actually reason. Rather than starting with a set of axioms, natural deduction lets us introduce assumptions and then discharge them when we've established what we need. This system consists of a set of primitive inference rules that allow us to manipulate logical formulas step-by-step until we've proven what we want to show. The Primitive Inference Rules Rule of Assumption The foundation of natural deduction is simple: any formula can be introduced as a premise or assumption at any point in a proof. When we do this, we note that this line depends on this assumption. This is what makes assumptions different from premises—assumptions can later be discharged (removed as requirements for the conclusion). This flexibility is what gives natural deduction its power. It allows us to temporarily assume something, explore its consequences, and then use those consequences to prove what we actually want to show. Conjunction: Introduction and Elimination Conjunction introduction states that if we've established both $P$ and $Q$ separately, then we can conclude $P \land Q$. This is intuitive: having proven two statements, we can assert that both are true. Conjunction elimination works in the opposite direction. If we have a conjunction $P \land Q$, we can derive either conjunct individually: we can extract $P$, or we can extract $Q$. Example: If we've proven "It is raining" and separately proven "It is cold," we can use conjunction introduction to conclude "It is raining AND it is cold." Later, if we need just one of these facts, conjunction elimination lets us extract it from the conjunction. Disjunction: Introduction and Elimination Disjunction introduction lets us derive a disjunction from just one of its disjuncts. If we've proven $P$, we can immediately conclude $P \lor Q$ (for any $Q$). This might seem odd at first—why would we weaken what we know?—but it's useful when we need to work with a disjunction. Disjunction elimination is more complex. To derive a conclusion from a disjunction $P \lor Q$, we must show that the conclusion follows from both $P$ and from $Q$. In other words, we create two separate sub-proofs: one assuming $P$ and deriving our conclusion, and another assuming $Q$ and deriving the same conclusion. Once we've done both, we can conclude our formula without needing the original disjunction. Example: Suppose we know "Either Alice went to the store OR Bob went to the store." We also know that if Alice went, she bought milk, and if Bob went, he bought milk. Using disjunction elimination, we can conclude "Milk was bought" without needing to know which person actually went. Conditional: Introduction and Elimination Conditional introduction is essential for proving implications. To prove $P \to Q$, we assume $P$, derive $Q$, and then discharge the assumption. The key insight is that this shows: "given $P$, we can derive $Q$," which is exactly what the conditional means. Conditional elimination, also called modus ponens, is straightforward: if we have a conditional $P \to Q$ and we have the antecedent $P$, we can directly infer the consequent $Q$. Example: To prove "If it rains, then the game is cancelled," we assume it rains, show that this leads to the game being cancelled, and then discharge the assumption. Later, if someone tells us it actually did rain, we can use modus ponens to conclude the game was cancelled. Negation: Introduction and Elimination Negation introduction proves a negation by assuming the opposite. To prove $\neg P$, we assume $P$, and then derive a contradiction. Once we've shown that $P$ leads to a logical contradiction, we can discharge the assumption and conclude $\neg P$. The reasoning is: if $P$ were true, we'd have an impossible situation, so $P$ must be false. Negation elimination is the straightforward principle of non-contradiction: if we have both a formula $P$ and its negation $\neg P$, this is a contradiction. In formal terms, a contradiction allows us to derive anything (the principle of explosion). Example: To prove "The defendant is not guilty," we might assume the defendant is guilty, then show that this leads to contradictory evidence. Having demonstrated the contradiction, we discharge the assumption and conclude the defendant is not guilty. Reductio ad Absurdum (Proof by Contradiction) Reductio ad absurdum is another proof method that many students find intuitive: to prove a formula $P$, we assume its negation $\neg P$, derive a contradiction, and then discharge the assumption to conclude $P$. The difference between negation introduction and reductio ad absurdum might seem subtle, but it matters. In negation introduction, we assume $P$ to prove $\neg P$. In reductio ad absurdum, we assume $\neg P$ to prove $P$. Both involve contradictions, but they prove different things. How These Rules Connect: An Important Note You might notice that some of these rules seem related. For example, material transposition—the principle that $P \to Q$ is equivalent to $\neg Q \to \neg P$—is not a primitive rule. However, it can be derived from modus ponens and reductio ad absurdum. This shows that the primitive rules are the core toolkit, and many familiar logical principles emerge as derived consequences of these basics. Notation Systems for Natural Deduction Proofs Natural deduction proofs can be written in several different notational styles. Each has strengths and weaknesses, and you may encounter any of them. Gentzen Tree-Shaped Notation Gentzen notation arranges proofs as branching trees, where each node represents the application of a rule. The branches show the premises that feed into that rule application. This notation clearly shows the logical structure and dependencies, but can become visually complex for larger proofs. Jaśkowski Box Notation Jaśkowski notation uses nested boxes to represent sub-proofs and temporary assumptions. When you introduce an assumption, you open a box. Everything inside that box depends on the assumption. When you're ready to discharge the assumption (typically through conditional introduction or negation introduction), the box closes. This notation makes dependencies very explicit but can become difficult to read with many nested assumptions. Fitch Horizontal-Line Notation Fitch notation simplifies Jaśkowski's approach by replacing boxes with horizontal lines. When you introduce an assumption, you draw a line beneath it. All subsequent lines beneath that line are within the scope of that assumption. When you discharge the assumption, you stop the line. This notation is cleaner than nested boxes but still clearly shows which assumptions are active. Suppes–Lemmon Linear Notation Suppes–Lemmon notation writes proofs as simple numbered lists, where each line contains: The formula being derived An annotation explaining which rule was used and which earlier lines justified it An assumption set: the set of line numbers whose assumptions are still active for this line The line number itself This is the most compact notation and works well for linear presentations, though it requires careful attention to the assumption set to understand dependencies. Understanding Proof Structure In any notation system, a natural deduction proof progresses by adding new lines. Each new line must be justified by either: Being an assumption (justified by the rule of assumption) Applying a primitive rule to one or more earlier lines When you apply a rule, you indicate which earlier lines you used and which rule justified the step. The proof is complete when you've derived your target formula, and all assumptions have been discharged (except for the original premises, if any). The crucial point about assumptions is that they must eventually be discharged. A valid proof doesn't end with any active assumptions; everything you concluded must follow from the original premises alone. Axiomatic Proof Systems While natural deduction bases reasoning on inference rules applied to assumptions, axiomatic proof systems take a different approach: they treat certain tautologies as self-evident axioms and derive other formulas using formal rules of inference. Core Idea of Axiomatic Proofs In an axiomatic system, you start with a set of axioms—formulas that are assumed to be true. The two main rules of inference are: Modus ponens: from $P$ and $P \to Q$, infer $Q$ Substitution rule: replace any well-formed formula with any of its substitution instances (replacing a schematic variable with a concrete formula throughout) A proof in an axiomatic system is a sequence of formulas, each either an axiom, an assumption, or derived from earlier lines using modus ponens or substitution. Axiom Schemas and Instantiation Axioms in these systems are typically given as schemas rather than individual formulas. For example, instead of writing out infinitely many axioms like "$P \to (Q \to P)$" for each possible $P$ and $Q$, we write a single schema: "$A \to (B \to A)$" where $A$ and $B$ are schematic variables that can be replaced by any well-formed formula. The substitution rule generates all the concrete axioms we need by substituting specific formulas for the schematic variables. <extrainfo> Key Metatheoretical Properties Two critical results characterize good axiomatic systems: Completeness: Every semantically valid formula (every tautology) is provable in the system. This means the axioms and rules are powerful enough to prove everything that's logically true. Consistency: No contradiction is provable. The system never allows you to prove both $P$ and $\neg P$ for any formula $P$. This ensures the system is sound—it never leads to impossible conclusions. These properties guarantee that an axiomatic system is both powerful enough (completeness) and safe enough (consistency) to rely on. </extrainfo> Summary Natural deduction gives us a flexible toolkit of primitive rules—assumptions, conjunction, disjunction, conditionals, negation, and reductio ad absurdum—that let us build proofs by introducing and discharging assumptions. These rules can be presented in various notational styles depending on what's clearest in context. Axiomatic systems offer an alternative approach based on axiom schemas and rigid rules of inference. Together, these systems provide rigorous methods for establishing logical validity.