Chapter 6 Braille

One challenge for making logic work in Braille readers is that the symbols used in the standard version of forall$𝓍$ may not be recognized by a Braille reader even if it supports Nemeth code. Here are the symbols used by forall$𝓍$ again:

logical not $\mathrm{\neg }$, logical or $\vee$, logical and $\wedge$, the conditional $\to$, the biconditional $\leftrightarrow$, the contradiction symbol $\perp$, the universal quantifier $\forall$, the existential quantifier $\exists$, equals $=$, therefore $\therefore$, single turnstile $⊢$, double turnstile $\models$, negated single turnstile $⊬$, negated double turnstile $⊭$, box $\mathrm{\square }$, diamond $\mathrm{◇}$.

As far as I know, only logical or $\vee$, conditional $\to$, the biconditional $\leftrightarrow$, and therefore $\therefore$ are included in the Nemeth standard. A Braille-enabled forall$𝓍$ could simply use different symbols for the remaining symbols, e.g., $\sim$ for logical not $\mathrm{\neg }$, for logical and $\wedge$. E.g., the formula $\mathrm{\neg }A\vee (B\wedge C)$ would instead produce . There are conventional ASCII equivalents for all the symbols which are used by the Carnap online homework system to facilitate entering logical symbols, as well as other straightforward ways to approximate symbols:

• ‣
  ​

  logical not $\mathrm{\neg }$: $\sim$, $-$,

• ‣
  ​

  logical or $\vee$: $\mathrm{\backslash }/$,

• ‣
  ​

  logical and $\wedge$: , $/\mathrm{\backslash }$,

• ‣
  ​

  the conditional $\to$: $\mathit{->}$, $>$

• ‣
  ​

  the biconditional $\leftrightarrow$: ,

• ‣
  ​

  the contradiction symbol $\perp$: $\mathrm{\_}|\mathrm{\_}$, $!\mathrm{?}$

• ‣
  ​

  the universal quantifier $\forall$: $𝐴$, $@$

• ‣
  ​

  the existential quantifier $\exists$: $𝐸$, $3$

• ‣
  ​

  the therefore symbol $\therefore$: $:.$

• ‣
  ​

  the proves single turnstile $⊢$: $|-$, $|/-$

• ‣
  ​

  the entailment double turnstile $\models$: $|=$, $|/=$

• ‣
  ​

  the modal box $\mathrm{\square }$: $\mathit{[]}$

• ‣
  ​

  the diamond $\mathrm{◇}$:

Formulas and symbols would then display like $\sim A\mathit{->}(B/\mathrm{\backslash }C)|=A\mathit{->}C$. forall$𝓍$ could also be configured to replace all symbols with the corresponding text, e.g., $\text{not}A\text{or}(B\text{and}C)$.

These solutions would require a separately compiled textbook but no change to the text itself; the macros used to generate the symbols would simply be redefined.

A possible alternate solution would be to make MathJax output the problematic symbols to Braille using the alternatives listed above, but to keep the standard symbols for display and screen reader. (MathJax provides Braille output separately from speech output.) This might require a patched version of MathJax and someone with Braille expertise to provide the transliterations of symbols into Unicode Braille strings.

Girard et al. advises to use Polish notation for users of Braille. In Polish notation, logical operators are replaced by letters, e.g., $N$ for not ($\mathrm{\neg }$), $C$ for conjunction (and $\wedge$), $D$ for disjunction (or $\vee$), $I$ for if-then $\to$, and $B$ for if-and-only-if $\leftrightarrow$. Symbols like sentence letters and predicates would be lowercase instead of uppercase. Instead of parentheses, operators are prefixed to their arguments. E.g., the formula $\mathrm{\neg }A\vee (B\wedge C)$ would then appear as $DNaCbc$, i.e., the disjunction of not a with the conjunction of b and c.

Changing the format of formulas to Polish notation would require a separate Braille version of the text where all formulas are included in Polish notation, and somewhat extensive rewriting of the textbook (passages about formation rules for formulas, etc.).

Whether the table layout produced for natural deduction proofs (which should work with screen readers) is also suitable for Braille terminals remains to be determined.