Discrete Mathematics by Pearson

Introduction

PROOF METHODS AND INDUCTION

FORMAL PROOFS

In a complete formal proof of a theorem, each step follows from the previous steps using formal deduction rules. Ideally, such a process is so systematic that it could be checked mechanically by a program.

Since proofs are supposed to be mechanically checkable, we may think of using a computer to produce proofs of true theorems automatically. Russel and Whitehead, in Principia Mathematica, tried to write down a sufficient set of axioms that would let us prove everything interesting. Then Hilbert posed (as one is his 23 famous problems) the problem of finding such a method. One of the great accomplishments of 20th century mathematics is the proof that no such method exists. In fact, we do ...