Appendix D Notes on accessibility
Special attention has been paid to make this HTML version as accessible as possible, especially to readers using Assistive Technology (AT), such as screen readers like NVDA and JAWS. Screen readers are software designed to enable users with low or no vision to access and navigate web pages like this book. Some sighted users also sometimes prefer texttospeech (TTS) software to read web pages aloud. TTS software has fewer features than screen readers designed for nonsighted users and may not convert everything in this book to audio.
If you are using the HTML version of this book with a screen reader or Braille terminal, or are helping a student who relies on such tools (e.g., as instructor or accessibility advisor), and you have feedback please get in touch!
Navigation and styles
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 sansserif font, and blackonwhite, darkonsepia, or lightondark 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.
Symbols and formulas
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. With a mouse, you can right click on any formula to activate it. Screen readers will announce that formulas can be activated (e.g., NVDA says “application clickable” before every formula to indicate the presence of the MathJax menu.) 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 and reload the page.
Here are some of the more common symbols. Different screen readers and TTS applications will pronouce them differently, and sometimes not at all. After each symbol, we provide the customary pronounciation used by logicians.

‣
Uppercase and lowercase italic letters like $A$ (“upper A”) and $x$ (“lower x”)

‣
Uppercase and lowercase script letters like $\mathcal{A}$ (“script upper A”) and $\U0001d4cd$ (“script lower x”)

‣
Logical connectives: $\neg $ (“not”), $\vee $ (“or”), $\wedge $ (“and”), $\to $ (“only if”), $\leftrightarrow $ (“if and only if”), $\perp $ (“contradiction”)

‣
Quantifiers: $\forall $ (“for all”), $\exists $ (“there exists”)

‣
Metatheoretical symbols: $\therefore $ (“therefore”), $\u22a2$ (“proves”), $\u22ac$ (“does not prove”), $\models $ (“entails”), $\u22ad$ (“does not entail”)

‣
Modal operators: $\mathrm{\square}$ (“box”), $\mathrm{\u25c7}$ (“diamond”)
Subscripts should be pronounced by screen readers, although they may not indicate that they are subscripts. The formula ${A}_{2}$ may be read out as “upper A sub 2” or just as “A2”.
The expressions ‘blank ’ and ‘iff’ (‘if’ with two ‘f’s) are used throughout the textbook. In the HTML version, ‘blank ’ includes an invisible spelledout word ‘blank’ which screen readers should read out loud. The abbreviation ‘iff’ is short for ‘if and only if’. In the HTML version it is coded using an invisible zerospace word joiner character which should make screen readers pronounce ‘iff’ as ‘ifeff’ or ‘ayeeffeff’.
Proofs
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:
Line number 
Subproof level 
Formula 
Justification 

$1$ 
0

$(W\vee X)\vee (Y\vee Z)$

PR

$2$ 
0

$X\to Y$

PR

$3$ 
0

$\neg Z$

PR

$4$ 
open subproof,
1

$W\vee X$

AS

$5$ 
open subproof,
2

$W$

AS

$6$ 
2

$W\vee Y$

$\vee $I $5$

$7$ 
close subproof,
open subproof,
2

$X$

AS

$8$ 
2

$Y$

$\to $E $2$, $7$

$9$ 
2

$W\vee Y$

$\vee $I $8$

$10$ 
close subproof,
1

$W\vee Y$

$\vee $E $4$, $5$–$6$, $7$–$9$

$11$ 
close subproof,
open subproof,
1

$Y\vee Z$

AS

$12$ 
1

$Y$

DS $11$, $3$

$13$ 
1

$W\vee Y$

$\vee $I $12$

$14$ 
close subproof,
0

$W\vee Y$

$\vee $E $1$, $4$–$10$, $11$–$13$

It has 14 lines, with 3 premises, 2 levels of subproof nesting, and
two pairs of adjacent subproofs. For instance, the subproof beginning
on line 5 ends at line 6, and line 7 starts another subproof. So the
subproof levels of lines 6 and 7 is the same, but lines 6 and 7 are in
different subproofs. If you cannot see the subproof lines, you have to
pay special attention to how the subproof level numbers change
and when a formula is an assumption. A screen reader should
read line 7 approximately as: “7, close subproof, 2, open subproof,
upper X, AS.” The abbreviations ‘
PR
’ (for ‘Premise’) and ‘
AS
’ (for
‘Assumption’) are coded in the HTML version using the ‘abbr
’
tag.
Note that simple texttospeech applications may not read out complex tables such as the ones containing proofs or truth tables at all.
Diagrams
The text also contains a few diagrams. In the HTML version, these are provided with image descriptions, e.g.,
The image description here should read: “There are three shapes: the first shape is a grey circle labelled A, some empty space, the second shape is a white circle labelled C, and the fourth a white square labelled D.”
Table of symbols
What follows is a table of all the symbols used in the text, how they are most likely to be pronounced by screen readers, 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.
Symbol  Pronounciation  Meaning  ASCII equivalent 

$\neg $  not sign  logical not 
~ or 

$\vee $  or  logical or  \/ 
$\wedge $  and  logical and 
/\ or &

$\to $  right arrow  conditional 
> or >

$\leftrightarrow $  left right arrow  biconditional 
<> or <>

$\perp $  up tack  contradiction 
__ or !?

$\forall $  for all  universal quantifier 
A or @

$\exists $  there exists  existential quantifier 
E or 3

$\therefore $  therefore  therefore  :. 
$\u22a2$  right tack  proves   
$\u22ac$  does not prove  does not prove  / 
$\models $  true  entails  = 
$\u22ad$  not true  does not entail  /= 
$\mathrm{\square}$  white square  necessary  [] 
$\mathrm{\u25c7}$  white diamond  possible  <> 
Subscripts can be represented by an underline, e.g., ${A}_{2}$ as
A_2
.