PFPL Errata

If typographic errors are found in the PFPL, post them here.

Chapter 1

• the X_s in "family of disjoint finite sets X_s" (p.5) is not italicized.
• the first sentences in the 1st and 3rd paragraphs of 1.1 (p.4) are basically the same, and similarly for the first sentences of the 1st and 4th paragraphs of 1.2.
• Delete the apostrophe in "it's fresh counterpart", p.8.

Chapter 2

• In the proof of Lemma 2.1, p. 17, P(a nat) should be P(a) (the formalism has changed since the 1st edition).

Chapter 5

• Inconsistent notation for the judgement of equality of natural numbers between the first table in chapter 2.1, the definition of is in chapter 2, and rule 5.4(a). Also, something else seems wrong since is expresses structural equality on naturals and the presence of + rules out the possibility of equality. Is n1 + n2 is n nat a different (3-place) judgement that hasn't been defined before?
• First paragraph of 5.3: add a comma after "The judgement e val".
• Second paragraph of 5.4: script X should be x-> (otherwise no fresh vars available?)

Chapter 9

• First line of 9.5: delete extra "Gödel".

Chapter 12

• Exercise 12.3: 'constructive propositional forms a Heyting algebra' is missing the word 'logic'.

Chapter 13

• Exercise 13.1 assumes the reader has already completed exercise 30.2! Also, 'inhabited your solution' should be 'inhabited in your solution'.