Additional Topics in Logic

Logical reasoning and program correctness form the backbone of our mathematical and programming endeavors. To close this first portion of the course, we look at some final, miscellaneous topics that further tie together these two critical concepts together.

The Spectrum of Formality

What does it mean for a proof to be "formal?" Is it enough for a proof to contain symbols and reference relevant proof rules? In today's class we will answer these important questions!

Formal Proof Revisited

Previously we discussed the role of intuition and formal definition in our understanding of mathematics. Recall that mathematics is the science of modeling abstract phenomena. Our intuition helps us gain a foothold to understand these abstract models, in particular, by instantiating them to real-world examples we understand. However, these models are ultimately determined by their formal definitions.

If we are interested in rigorous, logical arguments, then they must also be rooted in these formal definitions rather than our intuition. This is what we mean by "formal proof!"

To put it another way, a formal proof is a logical argument whose steps of reasoning are justified by the formal definitions of whatever model we are operating in. For example, consider the inequality proof involving the mathematical factorial function from a previous reading:

I think we can all agree this a formal proof! Observe how our argument proceeds by expanding $n!$ according to its definition and appealing to mathematical facts we know from our previous math education.

In contrast, consider this less formal proof:

Why is this proof less formal than the previous one? Note that this proof does not say anything inaccurate! Formality is not about correctness! It is a matter of whether appropriate justification exists for the reasoning in the argument.

In this example, we do not justify why factorial always produces a non-zero, positive result. Here's another attempt that introduces some additional information:

Now we introduced prose to justify our reasoning, is this proof formal? I would argue not! While we have an intuition that factorial is the product of the positive natural numbers from $1$ to $n$, that is not the formal definition we have given factorial. In this sense, this third proof is still not formal because it does not rely on the formal definitions of our mathematical objects.

With this in mind, look at this excerpt from our original proof:

Since $n$ is non-zero, we know from multiplying two positive natural numbers results in a positive natural number, thus justifying our desired result:

This is awfully similar to the second proof in that we stated a "fact" without justification. Do we need to provide justification for this fact? But wait, we didn't given any justification for our mathematical induction proof principle. Do we need to justify that as well?

We can play this game ad nauseam because, like computer programs, our mathematical models are built upon stacks of abstractions. For example, underlying our proof are our principles of natural deduction. In particular, the line:

Let $n$ be a natural number.

Is really an application of our intro-∀ rule where we prove a universally quantified proposition by instantiating its quantified variable with an arbitrary value. Did we need to cite this rule in our proof to be truly formal?

Our way out of this madness is to recognize that formality in mathematical arguments is not a binary formal/not-formal question. Instead, mathematical arguments span a spectrum of formality where their level of formality is defined by what top-level assumptions they make.

In our "formal" proof above, our TRB includes:

1. First-order logic and natural deduction reasoning principles.
2. The soundness of mathematical induction.
3. Facts about arithmetic, i.e., the result of multiplying positive natural numbers.

When making mathematical arguments, we have to be cognizant of the assumptions we are making and, thus, our position on the spectrum of formality.

Symbols, Formality, and Readability

With all that being said, a common misconception we should address is that the formality of a proof is a function of the number of symbols it includes. With formality defined above as the size of our TRB, how do symbols fit into the picture? Here is our original proof again, but this time, without symbols:

You will probably find the first version of the proof much more readable than this version. Why is that? Likely, you see this version of the proof as much more verbose than the first, and it is easy to lose sight of the forest for the trees when you are wading through text.

From this, we see that symbols serve the purpose of acting as concise shorthand for formal mathematical definitions. Symbols pack much information in a small amount of space. Consequently, we can also overwhelm the reader if we include too many symbols as you likely felt when you first saw logic and natural deduction! Thus, a readable proof is typically achieved by intermixing prose and symbols, balancing the information we present to the reader to help them remember the salient details, but not overwhelm them.

Where should we sit on the spectrum of formality? How do we balance readability with all the details that are frequently present in intricate logical arguments? Just like traditional writing, there are no easy answers here, and the best way to learn is by writing a bunch, and experimenting what works for you as a writing of mathematical arguments! Throughout the rest of the course, we'll try to hone your proof writing instinct so that you can craft good mathematical prose.

Uniting Reasoning and Design

Traditionally, we think of algorithmic design and reasoning as two separate activities. First, you design an algorithm, and then, in a separate step, you reason about that algorithm. This is not wrong, but perhaps undesirable in two ways:

• In terms of workload, you are taking two passes through the code: once for construction and once for verification.
• By separating the two activities, you are not able to take advantage of one activity to assist in the other.

Recursive design and inductive reasoning, when employed correctly, alleviates these concerns. To see this, observe the similarities between our recursive design and inductive reasoning templates:

If we follow these templates, we can unite recursive design and inductive proof, so that when we build a recursive program, we can have some confidence that our program is correct, simply by following the template! To do this, we not only build a program according to the template, we also have a property in mind that we can use to check our work as we design the algorithm. We design the program in such a way that the property is "obviously" fulfilled. This has the dual benefit of not only ensuring we have fulfilled the property, but we also receive concrete guidance as to how to proceed!

An Example: Designing Map

As an example, let's consider re-designing the standard map function over lists. For example map((lambda x: x+1), [1, 2, 3, 4, 5]) -->* [2, 3, 4, 5, 6].

Before we apply the recursive design template, let's consider a property of map that ought to hold. After some thought, we might note that a simple property of map is that it should not change the number of elements in the list. Thus, we can consider the property:

Now let's design the function, (map f l), with this property in mind. For this function, f is a function and l is a list.

• When the input list l is empty, our property says that map should produce a list of length length([]) -->* 0. The only list of this sort is the empty list, so map should return an empty list in this case.
• When is l is non-empty, the list has a head and tail, and we assume that length(map(f, tail)) ≡ length(tail). We know that length(tail) is precisely one less than the length of l. So, if we take the list generated by map(f, tail), we just need to extend it by one additional element. To obtain such an element, we can transform head by f and then cons that onto map(f, tail).

Note in our design how we leverage our induction hypothesis, length(map(f, tail)) ≡ length(tail), to steer the design of the function.

In this sense, we see how verification can directly inform program design. I argue that you've likely done this when writing your programs whether you were cognizant of it or not! However, now that we've seen the connection directly, you can begin to leverage this connection whenever you write programs!