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 speciflying arguments.
ASIDE: Laws and contracts are really written in a separate language from English legalese full of technical terms with specific meanings. This is done because, while some ambiguity is tolerable in 99% of human interaction, the remaining 1% can be very problematic. Even so, legalese still contains intentionally ambiguous terms: When, exactly, is a punishment "cruel and unusual"?
What exactly is the "community standard" of indecency? The legal system tries to simultaneously be formal about laws, yet also be flexible to allow for unforeseen situations and situation-specific latitude. (The result of this tension is the position of Judge.)
ASIDE: Court decisions, while dense reading, are often the model of well-presented arguments.
Consider, from a previous example (Example 1.1), 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 Englishl (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 Mozillal6 or IEl7 ), or expensive recalls (p. 7).
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.
ASIDE: Other professions have checklists, protocols, and regulations to minimize human error; programming is no different, except that the industry is still working on exactly what the checklists or training should be. Someday, a license will be required for practicing software, at least for software involved with life-safety.
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 modeling -- how 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 use them for each of our two logics:
- Truth tables
- Boolean Algebra
- Inference Rules
We'll visit these topics in an interleaved manner first propositional logic (immediately with its semantics) and three methods of reasoning for it; then first-order logic and an in-depth look at its interpretations, and finally the methods of reasoning for first-order logic.
We'll begin with a particular syntax propositional logic for the game of WaterWorld before using this syntax to formally deduce safe moves.