5. Informality

We have now covered all of the fundamental inference rules of natural deduction as well as the inference rules known as induction principles, with an induction principle accompanying each inductively defined data type. These reasoning principles underlie most of the proofs you will ever see in mathematics, logic, and computer science.

Footnote: One exception is that we haven’t covered the so-called axiom of choice. This axiom allows one to assume that from any given non-empty set it’s always possible to choose some particular element. This means that if you have an collection of non-empty sets, you can form a new set of elements, with one from each of the given sets, even this is true even there is an infinite number of sets to choose from. This axiom is mostly uncontroversial and is included in the set of axioms defining ordinary set theory, the foundational principles for most ordinary mathematics. We will not further consider the axiom of choice in this class.

To ensure that you have a firm grasp on each of these principles and how to use them, we have presented them with the aid of the Lean Prover. A key benefit of such a tool is that it both supports and rigorously enforces syntactically correct logic and the correct use of all inference rules. It also provides for the automated checking of the acceptability of proofs so that you don’t have to wait for a human reviewer to evaluate proofs for correctness. Lean enforces a rigorous discipline of precise and complete logical reasoning. All well trained computer scientists should be versed in such logical reasoning whether using an automated tool or not.

Once you are fluent with the formal rules of logic and proof, the next step toward mathematical maturity is to learn when and how to relax the level of formality and completeness in your proofs.

There are two reasons to be able to do this. The first is to communicate with people who are not trained in the use of automated foundational reasoning systems. Most mathematicians and computer scientists today are not. The second is that the cost of completely formal, foundation reasoning, in which every last detail of a proof is fully developed, can outweigh the benefits of such formality and completeness when it should be clear to someone trained in mathematics or computer science that certain propositions are evidently true. In such cases, one should be able to say something to the effect that, “this claim is easily proven by the use of such and such an approach.”

As we will see in this chapter, there are two distinct ways in which we can relax the level of formality and completeness in formal proofs. One is to maintain full formality, and just accept certain propositions as being true without proof, typically adding a comment to the effect that this is evidently true so we skip the task of giving an explicit proof. One can use Lean’s sorry command strategically for this purpose. While still being fully formal, this approach compromises on the completeness of proofs in the interest of not paying the costs of giving every last detail formally.

A second approach to relaxing formality and completeness is to sacrifice formality, and usually completeness, as well, by shifting to a natural language presentation style. It is very common indeed in natural language proofs to give high-level arguments, without details, for why a certain proposition is true, leaving it to the reader to judge whether or not the argument is value.

As a simple example, if the last step in a proof is to prove (1 + (1 + 1)) = (1 + 1) + 1, most mathematicians would just say, “and this is true by basic algebra,” or even, “and this is trivially true.” A proof assistant requires one to apply the associativity of addition to make the terms on both sides of the equality identical followed by the application of reflexive equality. That is what’s required to have a foundational proof, “all of the way down to the bare metal of predicate logic.”

Good judgment is required to make good decisions about when it is acceptable to skip over certain details in an incomplete formal proof or in an informal proof. There is a famous cartoon where a mathematician, standing at a chalkboard and going through a proof, says, “And here a miracle occurs.” The joke of course is that the person skipped a crucial step without justification.

Less humorously, the proposed proof of the so-called abc conjecture, by Mochizuiku, which has recently been the focus of intense international study, appears to have an error within the proof of a critical lemma. This potential error highlights the risks of “playing fast and loose” in eliding details. The mathematicians, Peter Scholze and Jakob Stix, found the apparent error and wrote about it in a report that they posted online. They state that, “We, the authors of this note, came to the conclusion that there is no proof. We are going to explain where, in our opinion, the suggested proof has a problem, a problem so severe that in our opinion small modifications will not rescue the proof strategy.” http://www.kurims.kyoto-u.ac.jp/~motizuki/SS2018-08.pdf

If you want to be absolutely sure a proof is correct, using a constructive logic proof assistant is perhaps the only solution. On the other hand, is is often not practical to use such a tool. Most mathematicians and computer scientists thus continue to rely on informal proofs. There are critically important applications of proof assistants, especially in the certification of life- and mission-critical software, but in general, it remains essential to be fluent in the presentation and consumption of informal proofs.

In this chapter, we therefore show you how to bridge from complete and formal proofs to both formal proofs with certain details omitted, and, more importantly, to informal proofs written in structured English or another natural language.

Our approach in this chapter will be to take a simple arithmetic proposition as a conjecture to be proved. Using each of four proof strategies, we first prove the conjecture formally, then we translate the formal proofs into informal proofs.

There are many levels of rigor and completeness in terms of which informal proofs can be written. We believe it is necessary to understand how to give a complete but informal proof first. Then one can use good judgment in deciding when it is acceptable to further relax the style of presentation by omitting details that readers can be expected to understand and accept, in order to improve that clarity of the proof without sacrificing its essential rigor.

5.1. Case Study

The conjecture that we will take as a case study is, stated informally, that if n and m are successive natural numbers, then their sum is odd. As any good mathematician would do, whether using an automated tool or not, we define our terms absolutely formally.

try it!

/-
A natural number, n, is said to be odd if
there is some natural number, m, such that
n = 2 * m + 1.
-/
def odd (n : ℕ) :=
    ∃ m, n = 2 * m + 1

/-
We will say that two natural number, n and
m, are consecutive if m = n + 1.
-/
def consecutive (n m : ℕ) : Prop :=
m = n + 1

/-
Now we can state the conjecture to be proved.
-/
def sum_consec_odd : Prop :=
    ∀ (n m : ℕ), (consecutive n m) → odd (n + m)

We will present eight proofs of this conjecture. We give two proofs, one formal and one informal, using each of four fundamental proof strategies: direct proof, contradiction, contraposition, and induction.

We note that as we go through the formal proofs, you will not necessarily be able to launch them (and have them work) in a web browser; the parts that we present are not always entirely self-contained. We refer you instead to the file containing the extended examples available in your GitHub repo for this course.

5.2. Direct Proof

A direct proof (of an implication) works simply by assuming the premise and showing that in that context, a proof of the conclusion can be given.

5.2.1. Formal Proof

We now give a direct proof of the conjecture. We comment the proof extensively to explain what each step of the proof does. As we will see in the next subsection, these comments give us an informal version of the formal proof. As you learn to write informal proofs, you should seek to write them in a way that mirrors a fully formal proof, for then every step of logical reasoning will be clear. We now present our first proof using the direct method.

try it!

theorem pf_sum_consec_odd : sum_consec_odd :=
begin
/-
What we aim to show is that for any natural numbers, n
and m, if n and m are consecutive then their sum is odd.
-/
show ∀ (n m : ℕ),
    (consecutive n m) → odd (n + m),
/-
This conjecture is a universal generalization. To prove it,
we therefor must use the introduction principle for forall.
That is, we first assume that n and m are arbitrary but
specific natural numbers, then in that context we prove
that remaining implication, (consecutive n m) → odd (n + m),
is true. So let n and m be natural numbers.
-/
intros n m,
/-
The remaining conjecture is an implication. To prove it, we
will use arrow introduction, also commonly known as a direct
proof technique. That is, we will assume that the premise is
true, and in that context we will show that the conclusion
can be proved.
-/
assume h,
/-
Now all that remains to be proven is the conclusion, namely,
odd (n + m). To prove it, we will have to use our assumption,
that n and m are consecutive. To make the goal clear, we start
by expanding the definition of consecutive.
-/
unfold consecutive at h,
/-
Our assumption, the equality, h, now enables us to rewrite
m as the successor of n, reformulating the goal to be proved
as stating that n + (n + 1) is odd.
-/
rewrite h,
/-
We can now see that our goal is almost in a form where
it can easily be proved. Our next step is to expand the
definition of odd.
-/
unfold odd,
/-
This step reveals that what remains to be proved is the
existentially quantified proposition, that there exists
an m such that n + (succ n) = 2 * m + 1. To prove such a
proposition, we must use exists introduction, providing a
witness and a proof that the witness satisfies the
remaining predicate. We start by giving the witness,
which some basic algebra suggests must be n.
-/
apply exists.intro n,
/-
The remainder of the proof requires only basic algebra.
Lean's "ring" tactic automates the construction of proofs
of such propositions for arbitrary algebraic rings, so an
easy way out is just to use ring. If you don't have a nice
tactic like this, then you have to use more primitive
rules, such as rewriting using the associativity of
addition.
-/

-- ring

/-
Otherwise, one starts by using the associativity of
addition to regroup the terms in the sum on the left to
get (n + n) + 1. The all that needs to be done is to
rewrite (n + n) as 2 * n. That, in turn, requires a
little lemma. We start by regrouping.
-/
rw<-nat.add_assoc,
/-
To complete the proof requires only basic arithmetic.
In detail, we need to rewrite n + n as 2 * n. Then the
proof of the theorem will be completed by the reflexivity
of equality.
-/
/-
To rewrite n + n as 2 * n, we need a little lemma. The
proof is by induction on n. It is obvious from basic
arithmetic that this is true, so we omit the formal
proof.
-/
have nneq2n : ∀ n : ℕ, n + n = 2 * n, from sorry,
/-
We now use our lemma to rewrite n + n as 2 * n. The
proof then follows directly, as already noted, from
the reflexive property of equality.
-/
rw nneq2n,

-- QED
end

5.2.2. Informal

A rigorous informal proof can be formed mostly by extracting the comments from the formal proof. Here is a complete, rigorous, but informal proof. It is complete and rigorous in the sense that is explicitly identifies the precise logical reasoning principles being used to justify each step.

5.2.2.1. Rigorous, Even Verbose, Informal Proof

Theorem: For any natural numbers, n and m, if n and m are consecutive then their sum is odd.

Proof: This conjecture is a universal generalization. To prove it, we use the introduction principle for forall. That is, we first assume that n and m are arbitrary but specific natural numbers, then in that context we prove that (consecutive n m) implies odd (n + m). So let n and m be arbitrary natural numbers.

The remaining conjecture to be proved is that (consecutive n m) implies odd (n + m). To prove it, we will use arrow introduction. This is also commonly known as a direct proof strategy. That is, we will assume that the premise is true, i.e., that n and m are successive numbers, i.e., that m = n + 1, and in this context we will show that the conclusion is true, i.e., that n + m is odd.

By the definition of the consecutive predicate, we have (assumed) that m = n + 1.

Then by the definition of odd, what remains to be proved is that there exists a natural number, k, such that n + (n + 1) = 2 * k + 1.

To prove such an existentially quantified proposition (constructively), we we must provide a witness and a proof that that specific witness satisfies the remaining predicate.

Basic algebra indicates that the witness that will work is n itself. Now all that remains to be proven is that n + (n + 1) = 2 * n + 1. By the associativity of addition we can write the left side, giving us the equation, (n + n) + 1 = 2 * n + 1. Clearly (n + n) = (2 * n), so the two sides are equal and the proof is complete.

QED.

In practice, mathematicians skip over many details, and the amount of detail they can reasonably elide depends on their assumptions about what their audience already knows and accepts without a detailed proof. A good practice, to avoid making mistakes, is to err on the side of giving more detail that is perhaps needed. Here we have given a fairly detailed informal proof, but to anyone trained in the art of rigorous logical reasoning it has the benefit of giving a precise justification of each step.

5.2.2.2. A More Concise But Still Rigorous Proof

Here is a more concise version of the proof that is still nearly as rigorous. In particular, it explicitly identifies at each step which rule of inference is being used to justify the step. It does it, though, without a lot of inessential additional explanation.

We apply forall introduction by assuming n and m are arbitrary but specific natural numbers. We then prove the implication, (consecutive n m) implies odd (n + m). To do this, we assume the premise, (consecutive n m), and prove the conclusion, odd (n + m). Expanding definitions we have assumed that m = n + 1 and we are to prove that there exists a k such that n + (n + 1) = 2 * k + 1. We prove this using k = n as a witness along with a proof that n + (n + 1) = 2 * n + 1. This statement is true by the application of basic operations of algebra. QED.

5.2.2.3. A Proof in a Typical Informal Presentation

Here finally is the kind of concise, and still rigorous, but informal proofs that we might expect to see in everyday mathematical writing.

Theorem: For any natural numbers, n and m, if n and m are consecutive then their sum is odd.

Proof. Let n and m be natural numbers. We must show that (consecutive n m) implies odd (n + m). So suppose n and m are consecutive. That is, m = n + 1. Now we must show there is a k such that n + (n + 1) = 2 * k + 1. Let k = n. Now n + (n + 1) = 2 * n + 1 is true by the rules of basic algebra. QED.

5.3. Proof by Contradiction

We have already proven the validity in classical predicate logic of negation elimination, also known as the method of proof by contradiction. You will recall that this method proves a proposition, P, by showing that assuming not P leads to a contradiction. This proves not (not P). The classical principle of negation elimination then allows one to deduce P.

5.3.1. Formal

try it!

/-
Proof by contradiction is equivalent to negation elimination,
which is not classically valid. We accept the axiom of the
excluded middle, from which it is easy to prove the validity
of negation elimination. Because we've prove its validity in
this way before, we just accept it here axiomatically.
-/

axiom proof_by_contradiction : ∀ { P : Prop }, ¬¬P → P

/-
Our proof by negation also relies on the fact that if something
is not true for all objects of a given type then there exists an
object of that type for which it is not true. Having proved this
proposition previously, we again take it here as given.
-/

def not_all_exists :
    ∀ {T : Type} {P : T → T → Prop},
    ¬ (∀ (t1 t2 : T), P t1 t2) ↔
    (∃ (t1 t2 : T), ¬ P t1 t2) := sorry

/-
We now state and prove the main theorem using the method of
proof by contradiction.
-/

example : sum_consec_odd :=
begin
/-
We start by expanding named terms into
their corresponding definitions, to make
it clearer exactly what is to be proved.
-/
unfold sum_consec_odd,
unfold consecutive,
unfold odd,     -- note renaming of variable
/-
The proposition to be proved is a universal
generalization, so use the forall introduction
principle, and assume that we have arbitrary
but specific natural numbers, n and m.
-/
intros n m,
/-
The remaining proposition to be proved in this
context is an implication. We use a direct proof
strategy, which is to say that we assume that the
premise is true and then show that the conclusion
follows.
-/
assume h,
/-
The conclusion is an existentially quantified
formula that basically asserts that n + m + 1
is odd. We will prove this by contradiction.
This means that we replace the conjecture by
its double negation, the assume the negation
of the conjecture (there's the "negation" part
of proof by negation), and then show that this
assumption gives rise to a contradiction.
-/
apply proof_by_contradiction,
assume k,
/-
Now we just have to show that the assumptions
we've made are contradictory. The contradiction
is revealed by showing that we also can prove,
as a lemma, the opposite of our assumption: that
there exists a natural number, m_1, such that
n + m = 2 * m_1 + 1.
-/
have contra : ∃ (m_1 : ℕ), n + m = 2 * m_1 + 1,
-- to prove this we use exists introduction
apply exists.intro n,
-- we rewrite the goal using our assumed equality
rewrite h,
-- finally we prove the goal using basic algebra
ring,
/-
The proof now is completed by the application of
false elimination. Because our assumption that
m + n is not odd led to a contradiction, we can
reject it; so indeed if n and m are consecutive
the n + m + 1 is even.
-/
contradiction,
-- QED
end

5.3.2. Informal Proof

An informal proof can be given using exactly the same logic but without as much detail. The assumption is that the reader will understand why each step makes sense without having each step explained in detail.

Theorem: Prove that if n and m are natural numbers, m = n + 1 implies that there exists a k such that n + m = 2 * k + 1.

Proof: Let n and m be natural numbers (forall introduction). We give a direct proof of the remaining implication. That is to say, we first assume the premise, that m = n + 1, and then show that the conclusion follows. We prove the conclusion by contradiction. That is, we assume that it is not the case that there is a k such a k. This assumption gives rise to a contradiction. We prove that this is so by proving a lemma that directly contradicts the assumption. In particular, we show that there is such a k. Let k = n. Clearly, then n + (n + 1) = 2 * n + 1. We have thus proved the negation of the assumption, and now by negation elimination, we have proved that the original conclusion is true: the sum of n and m is odd, as claimed. QED.

We make several notes about these proofs. First, we used sorry to tell Lean to accept not_all_exists as being true, axiomatically. Using the axiom keyword would be equivalent. We are using sorry as a way to mark places where we could give a formal proof but choose not to. One can use sorry strategically in formal proofs, to avoid having to give complete proofs all at once. It can be appropriate to do this (1) if it’s obvious that the claim to be proved is true and it’s not worth the trouble to give a formal proof of it, or (2) if one wants to make progress on the rest of a proof and intends to return to replace the sorry with an actual proof later on.

Second, we note that even though we promised to give a proof by contradiction, at the highest level of our proof, we use the principle of forall introduction, and then arrow introduction (a direct proof strategy). Only then do we apply negation, or proof by negation, to finish off the proof. It is vitally important to understand that in general, every step in a proof uses some proof strategy, and in general, one uses different strategies at different steps.

The proof, whether the formal or informal version, is really therefore a proof by forall introduction, leaving the proof of the following proposition as a subgoal, followed by a direct proof of the subgoal, leaving only the conclusion of the implication to be proved by contradiction. Most textbooks would simply call the proof a proof by contradiction. Knowing the full suite of inference rules of predicate logic lets you see the real nature of these proofs. In general, they are proofs by top-down refinement employing different basic inference rules or other already proven theorems at each step.

5.4. Proof by Induction

Todo

Add explanation.

5.4.1. Formal

try it!

example : sum_consec_odd :=
begin
/-
What is to be proved is the proposition,
∀ (n m : ℕ), m = n + 1 → odd (n + m). Our
definition of odd uses the variable m, so
to avoid confusion, we'll pick new names,
s and t, for the variables, n and m, in
the proposition to be proved.
-/
show ∀ (s t : ℕ), t = s + 1 → odd (s + t),
/-
This is a universal generalization. To
prove it, we apply the principle of forall
introduction assuming we have arbitrary but
natural numbers, n and m and by then
showing, in that context, that the
remaining proposition is true.
-/
intros s t,
/-
What remains to be proved is the
implication, t = s + 1 → odd (s + t).
We will prove it by induction on n.
-/
induction s with s' Ih,

/- BASE CASE

First we prove it for the base case,
where n = 0.  In this case, the goal
is t = 0 + 1 → odd (0 + t). We prove
this implication with a direct proof.
We assume the premise and show that
the conclusion follows.
-/
assume h,
/-
We simplify the goal by replacing t
with its assumed value, 0 + 1.
-/
rw h,
/-
We're down to showing that 0 + (0 + 1)
satisfies the odd predicate. We unfold
the definition of odd to start.
-/
unfold odd,
/-
What now remains to be proved is that
there's some m_1 that makes the equation
true. Basic algebra tells us that m_1 = 0
will work as a witness.
-/
apply exists.intro 0,
/-
The remaining goal is easily prove
by applying basic rules of algebra
(in the ring of natural numbers).
this is proven by simple algebra.
-/
ring,

/- INDUCTIVE CASE

We now turn to the inductive case. We
are to prove that if the claim holds
for some value, n', then it necessarily
holds for n' + 1. We take (and here Lean
gives us) the premise as an assumption.
In this context we have to show that
the conclusion follows.

To begin we assume the premise of the
implication to be proved.
-/
assume h,
/-
We see that the goal can be simplified
by using our assumption, h to rewrite
the occurrence of t in the goal.
-/
rw h,
/-
What we've now got to prove is
(1 + s') + ((1 + s') + 1) is odd.
All that remains is to use the
definition of odd and basic algebra
to complete the proof. The only
slightly subtle point is that to
prove oddness one needs to take
s' + 1 (nat.succ s') as a witness.
-/
unfold odd,
apply exists.intro (nat.succ s'),
ring,
/-
Note that we don't even need to use
the induction hypothesis to finish
this proof, so it's not really a very
good example of proof by induction.
Nevertheless, the strategy works,
albeit in an unusually simply way.
-/
end

5.4.2. Informal

5.4.2.1. Verbose

To prove the universal generalization, we apply the principle of forall introduction: we assume that we have arbitrary but specific natural numbers, n and m, and we show that, in this context, the remaining proposition is true. So let n and m be arbitrary but specific natural numbers.

What remains to be proved is the implication, t = s + 1 implies odd (s + t). We will prove it by induction on n.

Base Case:

First we prove it for the base case, where n = 0. In this case, the goal is t = 0 + 1 implies odd (0 + t). We prove this implication with a direct proof. We assume the premise and show that the conclusion follows.

We simplify the goal by replacing t with its assumed value, 0 + 1.

At this point, we’re down to showing that 0 + (0 + 1) satisfies the odd predicate. We unfold the definition of odd to start, and provide 0 as a witness, and finish it off with basic algebra.

INDUCTIVE CASE:

We now turn to the inductive case. We are to prove that if the claim holds for some value, n’, then it necessarily holds for n’ + 1. We take (and here Lean gives us) the premise as an assumption. In this context we have to show that the conclusion follows.

To begin we assume the premise of the implication to be prove, and in this context we prove the conclusion.

We simplify the conclusion to be proved by using our assumption to rewrite the occurrence of t in the goal as (nat.succ s’ + 1).

What we now have to prove is (1 + s’) + ((1 + s’) + 1) is odd. All that remains is to use the definition of odd and basic algebra to complete the proof. The only slightly subtle point is that to prove odd-ness one needs to take s’ + 1 as a witness.

QED.

5.4.2.2. Concise

Proof. Let s and t be arbitrary natural numbers and assume t = s + 1. We are to show odd (s + t). The proof is by induction on n.

Base Case (n = 0):

In this case, the proposition to be proved is t = 0 + 1 implies odd (0 + t). As t = 0 + 1, odd (0 + t) means odd (0 + (0 + 1)). To prove that 1 is odd, let k = 0 and use basic algebra to finish the proof.

Inductive case.

We are to prove that (if t = s’ + 1 then odd (s’ + t)) then (if t = (s’ + 1) + 1 → odd ((s’ + 1) + t)))).

To begin we assume the premise of the implication. This is our induction hypothesis. In this context we prove that the conclusion follows.

To do this we assume that t = (s’ + 1) + 1. The conclusion can then be rewritten as the proposition, odd ((s’ + 1) + (s’ + 1) + 1). To prove this is true, let k = (s’ + 1)). By simply algebra, the conjecture is thus true for (s’ + 1) if it is true for s’.

5.4.2.3. Combining

Combining the proof of the base case with the proof of the inductive case proves the conjecture is true for all natural numbers. QED.

We note that this is an especially simple proof by induction. We didn’t even need to refer to the induction hypothesis to finish off the proof. In proofs by induction more generally, one needs and induction hypothesis to complete a proof.

5.5. Proof by Contraposition

5.5.1. Formal

try it!

-- having already proven validity of contraposition we take it as a given
axiom contrapositive : ∀ {P Q : Prop}, P → Q ↔ ¬ Q → ¬ P

/-
We elide the comments from this formal proof and
give what would have been our comments in the form
of the informal proof below. Confirm for yourself
that the informal proof mirrors the formal one.
-/
example : sum_consec_odd :=
begin
unfold sum_consec_odd,
intros s t,
rw contrapositive,
assume h,
assume k,
unfold consecutive at k,
rw k at h,
have contra : odd (s + (s + 1)),
apply exists.intro s,
ring,
contradiction,
end

5.5.2. Informal

To prove the given universal generalization, we apply the principle of forall introduction: we assume we have arbitrary but specific natural numbers, n and m, and in this context we prove that the remaining proposition is true.

What remains to be proved is the implication, t = s + 1 implies odd (s + t). We will prove it by contraposition. To prove the goal it will suffice to prove its contrapositive, namely, not odd (s + t) implies not (consecutive s t).

We give a direct proof of this implication: we assume not odd (s + t) and show that in this context we can prove that not (consecutive s t).

We prove the conclusion by negation. That is, we assume consecutive s t and show this leads to a contradiction.

The definition of consecutive s t is t = s + 1. We use this fact to rewrite not odd (s + t) as not (odd (s + (s + 1))). To expose the contradiction, we prove as a simple lemma, odd (s + (s + 1)) using basic rules of algebra.

The contradiction provides for the use of false elimination to complete the proof.

QED

5.6. Summary

In this chapter, we have showed you how to apply the comprehensive knowledge you have gained of the rules of inference of predicate logic, including the induction principles that accompany each inductively defined data type, to write informal proofs of the kind you will see in everyday mathematics and computer science. When asked to write an informal proof, we encourage you to start with a complete and verbose version in which each step is justified by reference to a specific inference rule. When you are convinced you’ve got a good proof, you can then clean it up by removing information that is not essential for conveying the formal essence of the argument.

5.7. Exercises

Todo

See homework assignment