Appendix D Notes on accessibility

We have adopted the HTML style provided by BookML, developed for the Leeds mathematics department by Vincenzo Mantova. It provides a collapsible navigation menu, buttons at the top of each page to select the font size, switch between serif and sans-serif font, and black-on-white, dark-on-sepia, or light-on-dark display options.

The body of the page starts with an invisible link to skip to the beginning of the content, past the navigation sidebar and style buttons. The buttons are, in order:

• ‣
  ​

  ‘toggle sidebar’ to turn the navigation bar on or off;

• ‣
  ​

  ‘font settings’ for font size, serif or sans serif font, and light, sepia, or dark modes;

• ‣
  ​

  ‘download’ for links to download the PDF versions; and

• ‣
  ​

  ‘information about the toolbar’ for a popup that shows keyboard shortcuts for navigation.

Those keyboard shortcuts are: left and right arrow for moving to the previous and the next page, and ‘s’ to toggle the navigation sidebar.

All logical symbols and formulas in this book are converted to MathML and displayed using MathJax. MathJax provides additional accessibility features for formulas, which are found in the MathJax context menu—activate/right click on any formula to activate it. If your screen reader does not read out formulas such as $\forall x(A(x)\wedge B(x))$ you may need to activate Speech Output in the Speech submenu of the MathJax accessibility menu.

For reference, here is a table of all the symbols used in the text, how they are (probably?) pronounced, and what they are called in the text. In the rightmost column we provide a suggested way to enter them using ASCII characters, if inserting special symbols (in a homework assignment or email to your instructor, say) is not an option.

Subscripts should be pronounced by screen readers, although if the subscript is a number, they may not be. They can be represented by an underline, e.g., $A_2$ as A_2.

The expressions ‘blank’ and ‘if⁠f’ (‘if’ with two ‘f’s) are used throughout the textbook. In the HTML version, ‘blank’ includes an invisible spelled-out word ‘blank’ which screen readers should read out loud. The abbreviation ‘if⁠f’ is short for ‘if and only if’. In the HTML version it is coded using an invisible zero-space word joiner character which should make screen readers pronounce ‘if⁠f’ as ‘if-eff’.

The natural deduction proofs in parts IV, VII and VIII use vertical lines to indicate where subproofs start and end. Such vertical lines extend from the assumption line of the subproof to its last line and are displayed between the line numbers and the formulas in any given line. This makes proofs a special challenge for users with low vision or complete loss of vision.

To make these proofs accessible in this HTML version, proofs are coded as tables. Each table line has four columns: the line number, a subproof level indicator, a formula, and a justification. The subproof level indicator is a number recording how many nested subproofs the current line is contained in. It is 0 if the line is not contained in a subproof, 1 if it is in a subproof, 2 if it is in a subproof nested within another subproof, and so on. When reading out a subproof level indicator, screen readers should also announce if a subproof has just been closed on the previous line, and when a new subproof starts. The table header rows and subproof level indicators are hidden so that proofs visually appear as in the printed text.

Here is an example of such a proof: