Subsection 8.1.1 What Are Proofs For?
Recall that the job of proof is to lead us to truth and insight. Let’s watch this video again.
So far, in this course, we’ve focused on guaranteeing that our proofs:
Preserve truth. We have laid out a set of inference rules that is both sound and complete. These rules allow us to derive all and only those statements that follow from our premises.
Of course, if we want to derive conclusions that are true, we must also:
Begin with truth. This means that we must choose premises (axioms) that are true in the world we’re working with. We have chosen to say very little about this because choosing premises is a very different sort of activity than proof construction is. It typically requires substantial domain expertise. And it may be controversial.
In fact, one of the beauties of the theory that we’ve been presenting is that we’ve been able to separate the noncontroversial, reasoning piece from the (very often) controversial premise-selection piece. So, while our goal continues to be the construction of sound arguments (i.e., ones that start with true premises and apply sound inference rules) that lead to conclusions that are true, we’ll continue to focus on the argument construction part.
So far, nothing new. But, up until now, our proofs have been small and not very likely to tell us something we didn’t already know. We need to change that.
We need to:
Discuss strategies for finding nontrivial proofs in nontrivial problem domains.
Describe a way to write such nontrivial proofs. We want to avoid getting so bogged down in the details that we miss the main reason(s) why our conclusion must be true.
In this chapter, we’ll do both of those things.