Typo in ax-10?

[zengxu-yang]

Page 71:
ax-10 in the book does not match the one in set.mm.

ax-10 $a |- ( -. A. x ph -> A. x -. A. x ph ) $.

It is actually theorem axc7 in set.mm.

axc7 $p |- ( -. A. x -. A. x ph -> ph ) $=

Also I think some of the texts in ax-5 in the book should not be in italic: "where $d ... does not occur in ...".

[david-a-wheeler]

Thanks for the comment! We haven't committed to it, but I expect there will be a revision of the book at some point, and we'll definitely review that. Please keep the comments coming!

[benjub]

I confirm that @zengxu-yang is right. For the moment, this could go in errata.md as

Section 3.3.3 (page 71) - ax-10 should read $a |- ( -. A. x ph -> A. x -. A. x ph ) $.

(and indeed, the text in italic after ax-5 (same page) is probably due to a missing '$' to close a math environment).