I teach in an AI programme, which over the past few years saw starkly rising student numbers. To cope with larger groups of students we are increasingly making use of digital methods in our teaching. To interact with large groups of students, we use online platforms where students do not only find all the materials, but where they can also prepare and hand in home-work, discuss with lecturers and interact with fellow students. In addition, we make use of digital assessment. Students log in to specialised software and take their exams on a laptop. Such digital exams are easier to manage, easier to archive and (most importantly) easier to grade. However, the topics I teach – foundational set theory, logic, formal language theory and semantics – present a typographic hurdle for digitalisation. To produce algebraic proofs, logical formulas, automata graphs, etc. on a computer, you need relatively advanced knowledge of typographic scripting systems (e.g. \(\TeX\)) or of ways in which wysiwyg software can produce non-standard symbols. There are two problems with this. First of all, this knowledge is not always present; it simply cannot be presupposed. Second, and more importantly, even if this knowledge is there, the typographic step slows students down whenever they are using a computer to work with the materials. Given the typographic complexity of formalistic notation, students struggle to do well at digital exams, where producing the notation is a particularly unwelcome distraction.
The upshot is that you learn and that you do logic, set theory etc. much faster by working with it with pen and paper than by working on a computer. This situation is not just at odds with how teachers increasingly tend to use digital tools. There is, in fact, a general trend where students rely increasingly on laptops (or similar devices) for studying. Students use their laptop as their main study environment. The laptop not only contains their powerpoint presentations and their word processed essays, it contains their library, their schedule, the course materials, the lectures, the wealth of secondary resources to be found on youtube, wikpedia etc.; it even contains their working environment when working with other students using online collaboration platforms. For many students, the laptop is the central vehicle used for studying. And, disappointingly, those logic or maths exercises are excluded from this fabulous learning tool. Only hand-written logical formulas allow for quick thought, for swift exchange of ideas. You don’t do logic on a computer.
I’d like to know whether it needs to be like that. Couldn’t we have a way of doing logic, set theory, etc. with a much more accessible notation? In particular, couldn’t such disciplines have a notation that is keyboard accessible? What I mean by that is that the notation used is reproducible on a keyboard using at most a key combination involving SHIFT. Standard keyboards, be they the physical ones that come with laptops, or the screen-based ones on tablets or phones come with but a limited array of non-numerical, non-letter symbols. Here’s the range my laptop keyboard allows using at most SHIFT:
~ ` ! @ # $ % ^ & * ( ) _ + - = [ ] { } | " : ; ’ / ? . > , <
The notation I use in my research and in my teaching tends to rely on an entirely different set of symbols, symbols altogether unavailable through standard keyboards:
\(\neg\ \land\ \lor\ \exists\ \forall\ \rightarrow\ \models\ \vdash\ \Box\ \Diamond\ \cup\ \cap\ \subset\ \subseteq\ \wp\ \in\ \emptyset\ \lambda\)
Is it possible to replace this notation by keyboard accessible notation for the benefit of our students? What are the design considerations here?
Some keyboard accessible notation already exists. For instance, \(\lambda\) is lambda in Lisp and \ in Haskell. In R, && corresponds to \(\land\), while in C++, it’s AND or &. It should be clear, however, that programming languages tend not to host a set of expressions with the breadth of the list of symbols above. There are examples of programming environments where logical notation is more broadly adopted, however. I am particularly thinking of theorem provers (or proof management systems). I’m only familiar with Coq (website), which comes with an extensive set of notational conventions and many extensions into different logical corners. One of those libraries concerns predicate logic. A FOPL statement like
\(\forall x[P(x)\rightarrow \exists y[P(y) \land (R(x,y)\lor R(y,x) ]]\)
is given by the following Coq line:
(forall x: P x, exists y: P y, R x y \/ R y x)
For my purposes the notation of quantification is slightly frustrating – I am used to quantifiers prefixing a single instead of two open propositions. But that’s a small detail. And even if we generally agree on notation - most of us accept some degree of dialectal variation. All in all, I actually find this notation pretty readable - and it is definitely fast to produce, even though it may take a little bit of getting used to. (Things may further improve if one sugars statements with parentheses for readability.) I see no reason why - in the long run - we couldn’t switch to a notational convention like that of Coq, thereby allowing students to write logic in a digital environment, just like they would on paper. Mathematics and logical conventions are constantly undergoing change. Think for instance of how modern logical notation differs from that in Boole’s work or Frege’s Begriffschrift. Also, the restricted quantification notation in the above Coq statement does in some disciplines constitute a deliberate development of notation, a departure from the simple prefix notation that I prefer. If switching to keyboard accessible notation brings significant educational benefits, then scholars will surely swiftly adapt just as easily as they have done with previous changes.
So I think Coq (and perhaps other cases?) illustrate that it is perfectly possible to do logic without typographic hurdles. Obviously, however, the question is by what authority someone can introduce some new keyboard accessible notation. Even if the notation is useful for the student to learn some formal discipline, ultimately what matters is how broadly this notation is accepted and followed. The only way I can see new notation being adopted is if that notation comes with a specific use. Coq and programming languages are a good example. You use \ for \(\lambda\) in the context of Haskell programming, just like you use (say) /\ for \(\land\) if you’re in Coq. These programming environments need to rely on keyboard accessible notation. Without it, they wouldn’t function. (Imagine a programming language with the same typographic complexity as logic, where if x=<10 then b:=FALSE is notated notation “\(x\leq 10\Rightarrow b\rhd\bot\)” – clearly ludicrous.) But without such an environment where the notation is necessary, what makes new notation stick? Coq has very specific applications, that will not suit every user of logical formalism. (Personally, it doesn’t suit my semantic focus, for instance.) As such, environments like Coq are not enough in general use to dictate notation. Here lies the crux of the matter, I think. We have a broadly accepted set of (regrettably typographically heavy) notational conventions for blue-sky logic and maths. We may additionally have keyboard accessible variations for these, whenever a computerized application is involved, but these applications address particular sub-disciplines and, consequently, that new notation is only relevant to a subset of the broader community. Crucially, it is ludicrous to think that there could be an all purpose programming environment for all that is logic and maths. And, thus, it is hard to see how we can impose keyboard accessible notation on a new generation of students.
Unless we figure out what the regularities are in existing keyboard accessible notations. Here, I see some opportunities. For instance, forall appears a pretty natural notation for \(\forall\), as it is used for universal quantification in Coq, Haskell, Prolog and is, indeed, how \(\TeX\) creates \(\forall\). For conjunction, & (e.g. java) or and (e.g. python) are common choices. Adopting such choices, even alllowing for some dialectal variation, could surely be easily taken up.
Once we get to more specific areas, things become harder, however. What about, modal logic, for instance? The convention to use \(\Box\) for necessity and \(\Diamond\) for possibility is very useful, since they allow the expression of modal concepts as propositional operators (rather than, say, quantifiers over possible worlds.) But it is hard to replace these with something keyboard accessible. I would object to notation that uses English words like necessary and possible, or perhaps must and can, since the corresponding natural language expressions come with specific restrictions on their interpretation. The word possible, for instance, tends not to be interpreted deontically, yet if it is to replace \(\Diamond\), it should in principle be able to cover the general modal notion that has the quantificational force of possibility. Other potential borrowings from natural language are unsuitable for similar reasons: might (exclusively epistemic), may (exclusively deontic), can (never deontic).
One other disadvantage of using English words for notation is that this notation fails to be insightful about what logic or mathematics is about. Conjunction is not the logical counterpart of the English word and. It is first and foremost a formal connective that behaves in ways that parallel or contrast other connectives. It may be instructive to point out to students that the similarity in notation of using \(\cap\) for set intersection and \(\land\) for propositional conjunction can be connected to the fact that both do similar things. For one, if we interpret propositions as sets of possible worlds, then the interpretation of \(\land\) is that of set intersection. More broadly, \(\top\) (the true proposition) can be seen as the identity element for conjunction, just like the universe \(\mathcal{U}\) is the identity element for intersection. Similarly, \(\bot\) (the false proposition) is the identity element for disjunction and \(\emptyset\) is it for union.
\[ \begin{array}{rcl} \mathcal{U}\cap X&=& X\\ \emptyset\cup X &=& X\\[2ex] \top\land p&=& p\\ \bot\lor p&=& p\\[2ex] 1*p&=&p\\ 0+p&=&p \end{array}\]
From this perspective, it would be a pity to replace \(\cap\) by intersect and \(\land\) by and, etc. A notation like Coq’s /\ seems much more suitable. Even better would be to simply use * for conjunction/intersection and + for disjunction/union, although unfortunately * would then clash with the Kleene star.
Considerations like these make it unlikely that we could come to a broadly adopted keyboard accessible notation without lengthy discussion, and moreover it will increase the number of variations in use. I hope, however, that I am being overly negative. Perhaps there are already many more ideas on this out there than I am aware of. From my perspective, it’s clear that we should take notation seriously. Let’s get rid of all those constraining typographic hurdles and rethink how we write formalism down.