An argument by form

How can we tell true proofs from false ones? What, exactly, are the rules of a proof? These are the questions which will occupy us.

Proofs are argument by form. We'll illustrate this with three parallel examples of a particular proof form called syllogism.

As you've noticed, the form of the argument is the same in all these. If you are assured that the first two premises are true, then, without any true understanding, you (or a computer) can automatically come up with the conclusion. A syllogism is one example of a inference rule — that is, a rule form that a computer can use to deduce new facts from known ones.

Some non-proofs

Of course, not all arguments are valid proofs. Identifying invalid proofs is just as interesting as identifying valid ones.

Homer: Ah, not a bear in sight.  The Bear Patrol must be working.
Lisa:  That's specious reasoning, Dad.
Homer: Thank you, honey.
Lisa:  By your logic, this rock keeps tigers away.
Homer: Oh?  How does it work?
Lisa:  It doesn't work.
Homer: Uh-huh.
Lisa:  It's just a stupid rock.
Homer: Uh-huh.
Lisa:  But I don't see any tigers around here, do you?
  [pause]
Homer: Lisa, I want to buy your rock!
  [A moment's hesitation … and money changes hands.]
    

If Lisa isn't around, who will identify specious reasoning for us? We can certainly use her approach of finding other particular examples that follow the same argument, yet lead to a clearly erroneous conclusion.

The above examples are a bit frivolous, but the procedure of looking for counterexamples applies to many real-world dilemmas. It also highlights the difference between a correct proof, and a faulty proof that might still happen to lead to a true result. (By the way, this is the exact same skill used when trying to come up with an algorithm for a problem: “well, the algorithm works for this input, but can I find a something that makes one of the steps fail?” If so, you then try refining your algorithm “well, I can add a test to take care of that problem; is that enough so that it always works?”)

In real-world issues, there are often many subtleties, and short arguments that sound airtight might be glossing over factors which are important in practice.

The point illustrated is that often real-world arguments incorrectly imply that their result follows from the form of the argument, when in fact the form is not valid in the way a syllogism is. This fallacy can be illuminated by finding a different domain in which the argument fails. The practice of searching for domains which invalidate the argument can help both sides of a debate hone in on bringing the unspoken assumptions to light. The original argument, if its conclusion is indeed true, must be patched either by adding the unspoken assumptions or fixing the invalid form.

Other Inference Rules

Of course, there are more ways to deduce things, beyond a syllogism.

Figure 1: Glimpses of two different WaterWorld boards

(a) (b)

Consider the following argument about WaterWorld boards:

The problem is that the author of the argument presumably meant to conclude “all explored neighbors of (A) contain a pirate”.

Before we can study exact proofs, we need a way of writing exactly what we mean. This will occupy us for the next section.

The need for a precise language

These previous glitches in the WaterWorld arguments both arise, of course, because we were sloppy about what each sentence meant exactly. We used informal English — a fine language for humans, who can cope with remarkable amounts of ambiguity -- but not a good language for specifying arguments.

Consider, from a previous example, the statement “…[this is something] every Boy/Girl Scout and Architect should know”. Does this mean all people who are both a scout and architect, or everybody who is at least one or the other? Genuinely ambiguous, in English! (Often, “and/or” is used to mean “one or the other or possibly both”.)

We'll next look at a way to specify some concepts non-ambiguously, at least for WaterWorld. We need to be more careful about how we state our facts and how we use these known facts to deduce other facts. Remember, faulty reasoning might not just mean losing a silly game. Hardware and software bugs can lead to significant bodily harm (Imagine software bugs in an airplane autopilot or surgical robot system), security loopholes (e.g., in Mozilla or IE), or expensive recalls.

One reaction to the above arguments is “Well, big deal — somebody made a mistake (mis-interpreting or mis-stating a claim); that's their problem. (And sheesh, they sure are dolts!)” But as a programmer, that's not true: Writing large systems, human programmers will err, no matter how smart or careful or skilled they are. Type-checkers catch some errors upon compilation, and test suites catch their share of bugs, but many still remain in real-world software. Thus we are looking for systemic ways to reduce and catch errors, with the ultimate ideal of being able to prove programs correct.

In our study of formal logic, we'll need three things:

We'll begin with a particular syntax — propositional logic for the game of WaterWorld — before using this syntax to formally deduce safe moves.