Chapter 5 Proofs

Proofs are typeset with the fitch package. These are a challenge for blind users since the subproof lines carry important information as they indicate where a subproof starts and ends.

Line number	Subproof level	Formula	Justification
$1$	0	$A\rightarrow B$	PR
$2$	1	$\neg B$	AS
$3$	2	$A$	AS
$4$	2	$B$	$\rightarrow$ E $1$ , $3$
$5$	2	$\bot$	$\neg$ E $2$ , $4$
$6$	1	$\neg A$	$\neg$ I $3$ – $5$
$7$	0	$\neg B\rightarrow\neg A$	$\rightarrow$ I $2$ – $6$

Our solution is to converted them to HTML tables with an invisible table header and an invisible second column. The second column includes a number, indicating the level of subproof indentations on the corresponding line, and <SPAN> tags with aria-label attributes so screen readers will announce if a subproof has just been closed and/or a new subproof starts on the current line. The ‘PR’ and ‘AS’ labels should be pronounced ‘premise’ and ‘assumption’, respectively, by screen readers. (This solution was suggested by Audrey Yap, UVic, based on her experience with a blind student using this textbook.)

This HTML solution is only available when using BookML, since it relies on commands that allow raw HTML output not provided by LaTeXML.

ChromeVox seems to have difficulty reading out the table—sometimes it doesn’t read any MathML (including the line numbers). It should maybe pause between table cells.