1.2 Defining a proof  (Page 5/5)

Consider the following argument about WaterWorld boards:

The problem is that the author of the argumentpresumably meant to concludeall 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, becausewe were sloppy about what each sentence meant exactly. We used informal Englisha 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/oris used to meanone 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 isWell, big dealsomebody 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 reduceand catch errors, with the ultimate ideal of being able to prove programs correct.

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

• Syntax (language)a precise syntax and vocabulary for expressing concepts without ambiguity,
  • Propositional logic,
  • First-order logic (propositional logic, plus relations and quantifiers)
• Semantics (meaning) and modelinghow to connect these formal languages to whatever topic we want to reason about (including our software).
• Reasoning (proofs)methods of deducing new facts from old. We'll see three types of reasoning, and how to usethem for each of our two logics:
  • Truth tables
  • Boolean Algebra
  • Inference Rules

We'll begin with a particular syntaxpropositional logic for the game of WaterWorldbefore using this syntax to formally deduce safe moves.