# Language, Proof and Logic

## What's New in the Second Edition?

## Textbook

The main differences in the text book can be found in the chapters on Set Theory (15), and Mathematical Induction (16).
Both of these chapters have been completely rewritten to improve the exposition.
Many exercises have been added to these chapters, and these primarily involve the use of the software. Specifically, we encourage the
use of the **Lemma** inference rule to complete more complex formal proofs in set theory, and the new **Induction** inference rules
allow us to write more complex exercises involving formal induction proofs.

Chapter 10 also benefits from a discussion of the use of lemmas in completing proofs.

### Changes to the Exercises

We have introduced many new exercises into the second edition, and others have been renumbered from their position in the first edition. Instructors should be aware of this when setting exercises from the textbook. The ideal situation is that you and all of your students are using the same edition of the book, and no confusion can arise. However it is unlikely that you will live in this Panglossian world. Instructors should be prepared to deal with situations where students have a mixture of first and second edition textbooks. Exercise changes are limited to four chapters:

**Chapter 3**Exercise 3.26 has been moved from Exercise 3.29, while 3.27 used to be 3.26 and 3.28 was 3.28. The old exercise 3.28 has been removed.**Chapter 10**Three new exercises: 10.32, 10.33 and 10.34, have been added.**Chapter 15**This is tricky. Here is a picture.**Exercises 15.1--15.3**Second Edition was First Edition 15.1 15.3 15.2 new exercise 15.3 15.6 **Exercises 15.4--15.10**Second Edition was First Edition 15.4--5 15.1--2 15.6 15.4 15.7--9 15.8--10 15.10 new exercise **Exercises 15.11--15.17**Second Edition was First Edition 15.11 15.7 15.12 15.11 15.13 new exercise 15.14--15 15.12--13 15.16--17 new exercises **Exercises 15.18--15.65**These exercises are all numbered four higher than in the first edition, E.g. 15.21 used to be 15.17.**Exercises 15.66**This is a new exercise.**Exercises 15.67--15.77**These exercises are all numbered three higher than in the first edition (the old exercises 15.62 and 15.63 have been removed).

**Chapter 16**- Exercise 16.19 is new, the old exercise with this number has been deleted.
- We have changed the exposition of the axiomatization of the natural numbers to use s(0) instead of the numeral 1. Exercises 16.21 and 16.22, whose statements used to involve the numeral 1, are now stated using s(0).
- Exercises 16.24 and 16.25 are new.
- Exercises 16.26--28 used to be 16.24--26.
- The old exercises 16.27--31 have been removed.
- All of the remaining exercises in this chapter are new.

The Grade Grinder recognizes which edition of the book a student is using by their registration id (see below).

## Software

The software accompanying the second edition of the text book has been completely rewritten since the first edition. We have previously released versions of the software which update the first edition software, but each of the applications released with the second edition of LPL differ from any previously released version.

### General

The interfaces of the applications have been unified to use a new application toolbar which appears across the top of the application window. The tool bar contains controls for changing the font size and style, to print the current document and obtain help. In addition this toolbar contains controls for the critical application functions (E.g., checking steps in Fitch, checking truth values in Tarski's World, etc;) We hope this this will result in applications that are more intuitive for our users.

Each of the applications now allows users to specify preferences such as the size and style of text that they wish to use, whether to use step numbers and bold proof lines in Fitch, how to create blocks in Tarski's World, and so on.

**Boole**contains no new features, but has been completely re-implemented for the new edition.**Fitch**contains three new inference rules:**Lemma**,**Peano Induction**and**Strong Induction**.The

**Lemma**rule allows the use of a proof, previously stored on disk, to be used to justify a step in another proof. The use of the lemma rule is described in chapter 10 of the second edition of the textbook. Briefly, the lemma must contain exactly one goal and the proof must be correct. A use of the lemma must cite exactly the same number of steps as the lemma file contains premises, and the premises and goals must collectively*match*. The lemma may use abstract formulae, E.g.`P`, and abstract constants, E.g.,`n`and this will match any formula (resp. constant) in the containing proof, provided a match can be found which works for all premise and goal formulas._{1}The lemma is read from the file when the Lemma rule is first used. Subsequent changes to the lemma proof file will not be seen by the containing proof.

The lemma can be expanded ''in place'' in the containing proof using a control associated with the use of the inference rule.

- The
**Peano Induction**and**Strong Induction**rules allow the construction of proofs using this technique. This was previously possible only by the addition of appropriate instances of the induction axioms added to the proof as premises. These rules are described and used extensively in chapter 16 of the text. We hope that the provision of these rules allows the more intuitive construction of proofs by induction. We have introduced many exercises involving the construction of formal proofs using induction on the natural numbers into that chapter. numbers

Fitch also contains a new feature which we call

*goggles*. This feature applies to the**Taut Con**and**FO Con**inference rules and allows the user to see the information that is taken into account when assessing the correctness of these inferences. For example, when Taut Con's goggles are switched on, atomic (and quantified) formulas in the inference are replaced by blocks of color, with each different color representing a different formula (which may have multiple occurrences). This emphasizes that only the identity of formulae and the propositional connectives are used in assessing the correctness of an inference using Taut Con. For FO Con, the specific predicate symbols in the inference are replaced by blocks of color.Fitch also contains a new feature which allows users to automatically introduce supports after specifying the conclusion of an inference and the rule to use. For example If a user introduces a step containing

*A & B*and specifies the inference rule*&-Intro*, then the**Add Support Steps**command will create two new steps containing*A*and*B*respectively.The main new feature of

**Tarski's World**is the introduction of new controls for use within the Henkin-Hintikka game.The first set of controls impacts the display of information during the game. These can be used to allow some steps to be performed without interaction when desired. Three kinds of steps may be controlled:

**Rewrites**where a formula is replaced by an equivalent one, E.g., when a biconditional is replaced by the conjunction of implications,**Formula Choices**where the program chooses a formula to commit to, E.g. when a conjunction is believed to be true, and the program tries to choose a false conjunct, and**Block Choices**where the program chooses a block as a witness to the truth value of a formula, E.g. when a universal formula is believed to be true, and the program tries to choose a block which does not satisfy the open formula. In each case, the user can opt out of interacting with the program at these steps by toggling a check box at the beginning of the game. This is useful when the user is comfortable with propositional logic and wishes to focus on the steps which involve the role of quantifiers.A new control in the game itself allows the user to back up in the game to the point at which they most recently made a choice. This is more convenient than the previous implementations in which backing up was achieved only one step at a time, even if the previous step did not involve a choice on behalf of the user.

**Submit**is basically unchanged in its functionality, except that the user is prompted to confirm their email address the first time they make a submission. We have found that a number of students mistype their email address the first time that they make a submission with the result that they register with the wrong email address. As a consequence they do not receive grade reports, and must visit our web site to correct their registration.In addition, when we detect email addresses that do not accept mail from us, either because the email address has been mistyped, or perhaps for some more transitory reason such as the mailbox being over quota, we will not accept further submissions from the user until they fix the problem. This will avoid students repeatedly submitting work for a broken email address, perhaps because they have saved this address as part of their profile information.

**The Grade Grinder**now accepts the submission of files in response to "turn-in" exercises (exercises that had to be turned in on paper in the first edition). The Grade Grinder does nothing with these files except to store them in the archive. Like all other original files, these can be viewed or downloaded on the web site. The main advantage is that this avoids the necessity of managing student work submitted on paper.Only text (.txt) and rich text format (.rtf) files may be submitted to the Grade Grinder, and files must be named

**Solution N.M**where N.M is the number of the exercise. At most one solution file is accepted per exercise, so if the exercise calls for answers to several questions all of the answers should be included in a single file.There is nothing analogous to time stamps for solution files.

The Grade Grinder recognizes the edition of the book that a student is using by the prefix of the registration id. The first digit of the registration id indicates the edition of the book that it is associated with. First edition registration ids begin with the prefix L12- (or L11- for very old books). Second edition registration ids begin L21- (and eventually L22-, and so on.)

**The Web Site**has been updated to allow students to see their grade reports as instructors have always been able to. This too will avoid problems resulting from the use of broken email addresses, since students will be able to view their grade reports whether or not they have received email from the Grade Grinder.Instructors may now read or download reports related to time stamp collisions on the web site. Previously these were only available on request.

### New File Formats

Boole and Fitch both have new file formats. Both are implemented to be backward-compatible with the old format. This means that new versions of Boole and Fitch can read files created with earlier versions of the software. If such a file is read by the application and then saved, the new version will prompt for a new file name to allow the user to keep the old version of the file for use with the old file with earlier versions. Neither application is forward compatible, i.e. old versions application cannnot be used to read files produced by the new versions.