## Open Logic at Open Education Week 2018

It’s Open Education Week, and the Open logic Project will be part of the OER showcase at the University of Calgary tomorrow.

## Modal Logic! Propositional Logic! Tableaux!

Lots of new stuff in the Open Logic repository! I’m teaching modal logic this term, and my ambitious goal is to have, by the end of term or soon thereafter, another nicely organized and typeset open textbook on modal logic. The working title is Boxes and Diamonds, and you can check out what’s there so far on the builds site.

This project of course required new material on modal logic.  So far this consists in revised and expanded notes by our dear late colleague Aldo Antonelli. These now live in content/normal-modal-logic and cover relational models for normal modal logics, frame correspondence, derivations, canonical models, and filtrations. So that’s one big exciting addition.

Since the OLP didn’t cover propositional logic separately, I just now added that part as well so I can include it as review chapters. There’s a short chapter on truth-value semantics in propositional-logic/syntax-and-semantics. However, all the proof systems and completeness for them are covered as well. I didn’t write anything new for those, but rather made the respective sections for first-order logic flexible. OLP now has an FOL “tag”: if FOL is set to true, and you compile the chapter on the sequent calculus, say, you get the full first-order version with soundness proved relative to first-order structures. If FOL is set to false, the rules for the quantifiers and identity are omitted, and soundness is proved relative to propositional valuations. The same goes for the completeness theorem: with FOL set to false, it leaves out the Henkin construction and constructs a valuation from a complete consistent set rather than a term model from a saturated complete consistent set. This works fine if you need only one or the other; if you want both, you’ll currently get a lot of repetition. I hope to add code so that you can first compile without FOL then with, and the second pass will refer to the text produced by the first pass rather than do everything from scratch. You can compare the two versions in the complete PDF.

Proofs systems for modal logics are tricky; and many systems don’t have nice, say, natural deduction systems. The tableau method, however, works very nicely and uniformly. The OLP didn’t have a chapter on tableaux, so this motivated me to add that as well. Tableaux are also often covered in intro logic courses (often called “truth trees”), so having them as a proof system included has the added advantage of tying in better with introductory logic material. I opted for prefixed tableaux (true and false are explicitly labelled, rather than implicit in negated and unnegated formulas), since that lends itself more easily to a comparison with the sequent calculus, but also because it extends directly to many-valued logics. The material on tableaux lives in first-order-logic/tableaux.

Thanks to Clea Rees for the the prooftrees package, which made it much easier to typeset the tableaux, and to Alex Kocurek for his tips on doing modal diagrams in Tikz.

## Now With Axiomatic Derivations!

In addition to sequent calculus and natural deduction, the Open Logic Text now covers axiomatic derivations as well. Happy Holidays!

## Making an Accessible Open Logic Textbook (for Dyslexics)

In the design and layout of the Open Logic Project texts as well as the Calgary Remix of the intro text forall x, we’ve tried to follow the recommendations of the BC Open Textbook Accessibility Toolkit already. Content is organized into sections, important concepts are highlighted (e.g., colored boxes around definitions and theorems), chapters have summaries, etc. We picked an easily readable typeface and set line and page lengths to enhance readability according to best (text)book design practices and research.

We’ve started experimenting specifically with a version of forall x that is better for dyslexic readers (see issue 22).

Readability for dyslexics is affected by typeface, type size, letter and line spacing. Charles Bigelow gives a good overview of the literature here.

Some typefaces are better for dyslexic readers than others. Generally, sans-serif fonts are preferable, but individual letter design is also relevant. The British Dyslexia Association has a page on it: the design of letters should make it easy to distinguish letters, not just when they are close in shape (e.g., numeral 1, uppercase I and lowercase l; numeral 0, uppercase O and lowercase o, lowercase a) but also when they are upside-down or mirror images (e.g., p and q, b and d; M and W). In one study of reading times and reported preference, sans-serif fonts Arial, Helvetica, and Verdana ranked better than other fonts such as Myriad, Courier, Times, and Garamond, and even the specially designed Open Dyslexic typeface.

Although it would be possible to get LaTeX to output in any available typefaces, it’s perhaps easiest to stick to those that come in the standard LaTeX distributions. The typeface that strikes me as best from the readability perspective seems to me to be Go Sans. It was designed by Bigelow & Holmes with readability in mind and does distinguish nicely between p and q; b and d; I, l, and 1, etc.

• larger type size
• shorter lines
• increased line spacing
• increased character spacing, i.e., “tracking” (although see Bigelow’s post for conflicting evidence)
• avoid ALL CAPS and italics
• avoid word hyphenation and right justified margins
• avoid centered text

The accessible version of forall x does all these things: Type size is set to 12 pt (not optimal on paper, but since this PDF would mainly be read on a screen, it looks large enough). Lines are shorter (about 40 instead of 65 characters per line). Line spacing is set at 1.4 line heights. Tracking is increased slightly, and ligatures (ff, fi, ffi) are disabled. Emphasis and defined terms are set in boldface instead of italics and small caps. Lines are set flush left/ragged right and words not hyphenated. The centered part headings are now also set flush left.

The changes did break some of the page layout, especially in the quick reference, which still has to be fixed. There is also some content review to do. In “Mhy Bib I Fail Logic? Dyslexia in the Teaching of Logic,” Xóchitl Martínez Nava suggests avoiding symbols that are easily confused (i.e., don’t use ∧ and ∨), avoid formulas that mix letters and symbols that are easily confused (e.g., A and ∀, E and ∃), and avoid letters in the same example that are easily confused (p, q). She also recommends to introduce Polish notation in addition to infix notation, which would not be a bad idea anyway. Polish notation, I’m told, would also be much better for blind students who rely on screen readers or Braille displays. (The entire article is worth reading; h/t to Shen-yi Liao.)

Feedback and comments welcome, especially if you’re dyslexic!

There’s a lot more to be done, of course, especially to make the PDFs accessible to the vision-impaired. LaTeX and PDF are very good at producing visually nice output, but not good at producing output that is suitable for screen readers, for instance. OLP issue 82 is there to remind me to get OLP output that verifies as PDF/A compliant, which means in particular that the output PDF will have ASCII alternatives to all formulas, so that a screen reader can read them aloud. Even better would be a good way to convert the whole thing to HTML/MathML (forall x issue 23).

forallxyyc-accessible

## forall x YYC: Winter is coming

Pulled the switch on the new natural deduction rules; the Winter 2018 ß version is now out. If you have corrections etc. you want included in the next edition or want to proof read the changes before the new version goes up on Amazon, now is the time.

## Natural Deduction Rules in forall x: Calgary

Prompted by a good suggestion by Richard Lawrence and support from Catrin Campbell-Moore, we’ve been working on revising the natural deduction rules used in the Calgary Remix of forall x, the intro logic text by P. D. Magnus.  The proposal is to rename some rules so the nomenclature is in line with that used in the literature on natural deduction, e.g., where the rule $A, \lnot A \vdash \bot$ is $\lnot$-elimination, not $\bot$-introduction, and $\bot \vdash A$ is now called “explosion,” not $\bot$-elimination. We’re also planning to replace the tertium non datur rule with an indirect proof rule, i.e., Prawitz’s classical absurdity rule. (Tertium non datur, which we now slightly less pretentiously call “law of excluded middle” LEM,  will stay an “official” derived rule.) The proof checker recognizes both the old and the new rules.

We have an issue on GitHub tracking the progress and a branch with the revisions. The current version of the result is attached (see esp. Sections 15.7, 16.5, 19.4-5), but a few exercises elsewhere were changed, as were some of the solutions. Comments welcome!

forallxyyc

## Textbook Satisfaction Survey Results: Intro Logic Edition

As previously reported, we here at Open Logic Central have run surveys to gather some data on the relative success our open textbooks have with students. The first survey was done in several sections of Calgary’s Logic II course, where some sections of the course used Boolos, Burgess, and Jeffrey’s Computability and Logic, and some used the OLP-derived Sets, Logic, Computation.  We’ve now run these surveys also in Logic I, our first course in formal logic. One section, taught by Aaron, used forall x: Calgary Remix, four others used either Goldfarb’s Deductive Logic or Chellas’s Elementary Formal Logic. forall x was provided free as a PDF; the hardcopy retailed in the bookstore for $12, Goldfarb for$54, and Chellas for \$40. The highlights are below. But first a

HUGE CAVEAT: As encouraging as they are, of course, the result must be taken with a large grain of salt. The sections surveyed were taught by different instructors and with different TAs, at different times of day, in different terms, with different modes of delivery, and different modes of evaluation. Students’ attitudes towards a text used in a course depend not only on the text itself, but also on their experience in the course overall. If the material covered and tested in lecture doesn’t match up with the text, they may see it as a failure of the text. The quality of instruction may influence the perception of the quality of the textbook as well. Which direction? I think either is possible. If lectures are clear, students find it easier to understand the textbook, and so find it clearer. Or, if lectures are unclear, the textbook may look clearer by comparison.

As in the previously reported results in Logic II, students consulted the open textbook much more frequently than the other two textbooks.

They also consistently used forall x more for specific purposes.

forall x also ranks significantly better on every measure of textbook quality we asked about.

Last time I made the plots laboriously in Excel and Plot.ly. This time, the plots were done in R. (Still laborious, since I knew and still know pretty much zero about R.) If you’re curious exactly how, I wrote it up. Data and code on Github.

## A Fistful of Commits

I just checked in a whole bunch of changes to the part on first-order logic. Most of it is in preparation for a new version of the Logic II textbook Sets, Logic, Computation, which Nicole is planning to use in the Fall term.  Also important, and that’s why I put it right here at the top:

PDFs now live on builds.openlogicproject.org. The builds site has a nice index page now rather than a plain file list. If you link to a PDF on my ucalgary site, please update your link; that site will no longer be updated and will probably disappear sometime soon.

Here’s a list of changes:

• I’ve revised the completeness theorem thoroughly. (This was issue 38.) The main change is that instead of constructing a maximally consistent set, we construct a complete and consistent set. Of course, those are extensionally the same; but both the reason for why we need them and the way we construct them is directly related to completeness and only indirectly to maximal consistency: We want a set that contains exactly one of A or ¬A for every sentence so we can define a term model and prove the truth lemma. And we construct that set by systematically adding either A or ¬A (whichever one is consistent) to the original set. So it makes pedagogical sense to say that’s what we’re doing rather than confuse students with the notion of maximal consistency, prove that the Lindenbaum construction yields a maximally consistent set, and show that maximally consistent sets are complete so we can define the term model from it. Credit for the idea goes to Greg Restall, who does this in his course on Advanced Logic.  (I kind of wonder why standard textbooks mention maximally consistent sets. I’m guessing it’s because if you consider uncountable languages you have to use Zorn’s lemma to prove Lindenbaum’s theorem, and then using maximality is more natural. Is that right?) A bonus effect of this change is that a direct proof of the compactness theorem is now a tedious but relatively easy adaptation of the completeness proof; and I’ve added a section on this (leaving most of the details as exercises).
• I’ve revised the soundness proofs for sequent calculus and natural deduction, where the individual cases are now more clearly discussed. (This was issue 74 and issue 125.)
• In the process I also simplified a bunch of things, filled in some details, and corrected some errors. This includes fixing issue 110, and cleaning up the whole stuff about extensionality. There is a new section on assignments which you may need to add to your driver file unless you include fol/syn/syntax-and-semantics.tex in its entirety.
• The natural deduction system now uses Prawitz’s standard rules, i.e., the double negation elimination rule has been replaced with the classical absurdity rule, and the negation rules are now the special cases of the conditional rules with ⊥ as consequent. This was issue 144. Comparing the system to other treatments in the literature is now easier, and the chapter will integrate more seamlessly with the part on intuitionistic logic that’s in the works.
• The sequent calculus chapter now uses sequents that are made up of sequences, not sets, of formulas. This was issue 145. This is the standard way of doing it, and will make it easier to add material on substructural logics. It also makes the soundness proof a lot easier to understand.
• In both the sequent calculus and natural deduction chapters, the material on quantifiers is now separated from that on propositional connectives. Eventually it should be possible to present propositional logic separately (or only), and now you can reuse only the material on propositional logic. (This was issue 77.)
• There is a new chapter on proof systems, and the intro sections from both the natural deduction and sequent calculus chapters have moved there. So if you only want one of the proof systems, you’ll have to include the relevant intro section in the chapter on the proof system “by hand.” But if you include both, you now have an additional chapter that introduces and compares them.  (This was issue 61.)
• Sets, Logic, Computation (the textbook for Logic II) now includes both sequent calculus and natural deduction!

Note: The formatting of the rules in both systems now uses a defish (“definition-ish”) environment. If your remix uses a custom -envs.sty file, you will need to add a definition for that at the end (see open-logic-envs.sty). The textbooks for Logic II and Logic III have been updated accordingly.