How to formally prove a universal implication

discrete mathematicsformal-proofslogicnatural-deductionproof-writing

A textbook I am reading (Discrete Mathematics and its Applications by Rosen) went from introducing formal propositional and predicate logic (including popular rules of inference like Modus Ponens, Modus Tollens, and Universal Generalization) to introducing direct methods of proof for theorems of the form ∀n(P(n)->Q(n)).

Apparently, most mathematical proofs of any kind of theorem are "informal" and omit many logical rules of inference and argumentative steps for the sake of conciseness. However, because the textbook doesn't provide even one example of a detailed "tedious" proof that expresses most or all rules of inference and axioms used in the proof, though I have a general idea of the connection between the two, I have been struggling to fully tie together the ideas of formal logic to the ideas of mathematically proving theorems of the form ∀n(P(n)->Q(n)). Can anyone provide an example of a detailed mathematical proof of a simple theorem that omits few (if any) logical steps in the argument? I have personally struggled with (as a personal exercise) meticulously proving the theorem "for all integers, if n is odd then the square of n is odd", but any logically detailed argument proving a simple theorem similar to that would be very useful.

Best Answer

More a reflection than an answer, but too long for a comment.

Your observation that

Apparently, most mathematical proofs of any kind of theorem are "informal" and omit many logical rules of inference and argumentative steps for the sake of conciseness.

is true. I think it should follow that starting an undergraduate text on discrete mathematics with formal logic - truth tables, rules of inference, quantification - only confuses students when they are then expected to construct convincing proofs using everyday clear thinking. They rightly wonder whether all that formality is necessary and ask questions like this one.

Of course it is necessary in other contexts - when studying logic, when designing programs to prove theorems - but not in introductory courses.

Edit, suggested by @Bram28 's excellent answer. Rosen's Universal Generalization that replaces "for all elements $x$ such that" by "let $x$ be an arbitrary element such that" is close to what is often called "proof by representative special case". Those are not proofs but tell you clearly how a formal (or informal) proof will work.

For (a toy) example, to prove that the square of an odd number is odd, look at what happens when you square $15$. The distributive law tells you $$ 15^2 = (2\times 7 + 1)^2 = 4 \times 49 + 2 \times (2\times 7) + 1 $$ which is the sum of two even numbers and $1$, hence odd. There was nothing special about $15$ in this argument - you can clearly see how it represents all odd numbers.

(Parenthetically, this example/proof suggests the even stronger theorem that the square of an odd number is congruent to $1$ modulo $4$.)

If you search for "representative special case" (with the quotation marks so that you get just links to the whole phrase) you find this from Hilbert:

The art of doing mathematics consists in finding that special case which contains all the germs of generality. (Example for Hilbert quote),

a quote from Polya , and other links worth following.

Related Question