How do you know if “by inspection” is a valid argument?

Question

Sometimes while certain deductions may seem obvious, they are only obvious because of much prior work.

For instance, even describing something as simple as $1+1=2$, you would first need to:

• define group containing a set of objects $S$,

• define the operation of addition such that $S \times S \rightarrow S$,

• define that the set is closed under this operation $(S_{1},S_{2}) \rightarrow S_{1}+S_{2}$,

• define that addition is associative $(S_{1}+S_{2})+S_{3}=S_{1}+(S_{2}+S_{3})$,

and it even continues on from there.

So, if you can't even argue “by inspection” for something as elementary as $1+1=2$, what exactly makes it valid for more complex derivations dealing with summations or matrices or special functions of a complex variable and etc.?

Answer 1

I'll give two explanations, not completely unrelated. In the vein of Sean Roberson's comment, it often is intended in an informal sense that the result can be shown with a bit of thought. To answer your question in that case, you choose to use it by gearing it to your target audience. If you have a subproof (that you've produced yourself and) that is uninteresting and for which you expect the readers to be able to provide themselves, then using "by inspection" may be appropriate.

At the complete opposite end of formality, consider mechanized theorem provers like Coq, Isabelle/HOL, Mizar, and Agda. In at least the ones based on dependent type theory, like Coq and Agda, a potentially huge (but finite) amount of computation can go into verifying a single step of a proof. In Agda, you might define the natural numbers as follows:

data Nat : Set where
    Z : Nat
    S : Nat -> Nat

with addition then defined recursively as follows:

_+_ : Nat -> Nat -> Nat
x + Z = x
x + (S y) = S (x + y)

We can define $1$ and $2$ via:

one : Nat
one = S Z

two : Nat
two = S (S Z)

We can then prove that one + one equals two via:

one_plus_one_equals_two : Id (one + one) two
one_plus_one_equals_two = Refl

where, for completeness, Id is defined as:

data Id {A : Set} (x : A) : A -> Set
    Refl : Id x x

To verify that one_plus_one_equals_two is well-typed, and thus, effectively, a valid proof, we need to know whether one + one is the same as two. To do this, Agda computes one + one and two to normal form. If they have the same normal form, then they are considered the same. In this case, that normal form is S (S Z). Note that it does require some computation via the definition of + to reduce one + one to S (S Z).¹

You do not need to justify the steps of computation. A mechanized proof checker for Agda is expected to be able to perform these computations itself. This is one formal perspective on steps which might be said to be show "by inspection". Indeed, often statements that are asserted to be try "by inspection" are straight computations. This is largely consistent with mathguy's comment. In other words, if it is a purely mechanical computation, then "by inspection" would almost certainly be reasonable. For an informal proof, you'd still want to tailor this to your audience. There are a surprisingly large number of things that can be verified purely mechanically. I recommend the book A=B for some non-trivial examples. I probably would spell out some of the details of the equality of two hypergeometric series, even though they are mechanical verifiable.

For example, checking whether two polynomials with rational coefficients are equal is a purely mechanical process. If my proof relied on the fact that two polynomial expressions were equal, I would not painstakingly go through a step by step argument in terms of the axioms of commutative ring theory. I would just throw them into a computer algebra system to make sure, and then just assert that they are equal with little to no argument in the informal proof. With a little care, you can arrange it so that Agda can compute the proof that two polynomials are equal. This is what the RingSolver module does. Doing so leaves a potentially large and non-trivial computation to the proof checker, but it is a completely mechanical process that's completely specified by the computational rules that are part of the definition of Agda itself. This is a formal analogue of leaving it up to the reader to check the equality of two polynomials.

¹ Note that Agda can't solve just any equality automatically. If you ask it the equivalent of whether x + Z = x, it will happily immediately say it is via the first line of the definition of +. However, if you ask it the equivalent of whether Z + x = x, it is unable to show this just by computation. The definition of + does not specify how to handle the case where the second argument is a variable.