Balisage Paper: Thinking, wishing, saying

Introduction

It is probably not a good idea to make historical figures into personal heroes.^[1]

Professional historians frown on the practice. But the biographies that children read about figures of the past tend to make them into heroes and encourage the readers to emulate them; that may be part of why professional historians sometimes turn up their noses at any signs of unconditional approval (or disapproval) of any historical figure. The professional historians have a point: simple approval or disapproval is unrealistic. Human beings are mixed; they have flaws, they have virtues. And it’s probably a mistake to think of them in purely positive (or purely negative) terms.

And yet, it’s difficult for anybody — at least it is for me, and I suspect also for many people who like me enjoy reading popular books about the history of mathematics — not to think of some past figures as heroic. I’ve been thinking a lot lately about Gottlob Frege, for example: a mathematician with what we might call philosophical inclinations — I think he is probably read more in philosophy departments now than in mathematics departments — who worked throughout his career to clarify the foundations of mathematics and other important concepts, many with implications far beyond mathematics. It is to Frege that we owe, for example, the distinction between sense and reference which turns out to be crucial for addressing questions like the one Allen Renear mentioned the other day: Giorgione was so called because of his size [Renear 2019]. I am not entirely certain that anyone has solved the Giorgione problem to Allen’s satisfaction, but I suspect that if anyone were to do so they would have to rely at some level on that clarification that we owe to Frege’s work of over a century ago [Frege 1892].

Frege is also dear to my heart because he created a conceptual script, or notation, that was explicitly intended to be a partial realization of the philosophical language that Leibniz and many other people had imagined, a language in which what is now for most of us extremely difficult error-prone reasoning could be reduced to rules so that if you had a dispute with someone, you could just calculate, essentially do the math [Frege 1879].

And of course, there is the pathos of his correspondence with Bertrand Russell. You may know the story: Frege is completing a huge, two-volume work restating the essentials of mathematics using his conceptual writing [Frege 1903]; his aim aim is to clarify the logical underpinnings of every theorem and make sure that all of the inferences are clean and that there are no silent assumptions being smuggled in either unawares or intentionally. Just as he is finishing, he receives a letter from Bertrand Russell which asks a simple question about a set whose members are all of the sets that do not contain themselves. The problem is that Frege’s axioms require that that set exist, and the definition of a set requires that it not exist [audience chuckling]. So volume two of Frege’s Basic Laws of Arithmetic has an afterword that explains that the foundations of the work have collapsed [Frege 1903].^[2] [audience laughter] But he seems to have borne it with a certain amount of personal dignity.^[3]

I am similarly prone to hero worship of the mathematician David Hilbert.^[4] Like Frege, he was dedicated to clarifying the foundations of mathematics and securing its logical foundations. His book on geometry was regarded by his contemporaries as a sort of revelation because it made clearer than had ever been before how each theorem depended on others and on the axioms and what effect it would have, if the axioms were changed in various ways; this provides a more integrated view of Euclidean and non-Euclidean geometry and how they are related [Hilbert 1899].

As an admirer of both Frege and Hilbert, I experienced a certain degree of personal discomfort when I realized that they disagreed on problems that they regarded as fundamental, and I have always had trouble understanding why they disagreed, because they seemed to me to be on the same side of the issue. They were both interested in cleaning up the formality of mathematics and logic. But Frege wrote Hilbert a letter, Hilbert responded in a way that didn’t satisfy Frege, Frege published an open letter to Hilbert, and the result was a rather acrid public dispute. It’s like having two of your friends suddenly start arguing, and you’re disturbed because you want them to like each other.

But in this case, it was even more disturbing that I had trouble understanding what they were disagreeing about, and even more trouble understanding why. I have come now to suspect that it had something to do with what students of logic distinguish as proof theory and model theory. Over-simplifying greatly (which I have to do because I cannot claim any deep understanding of either proof theory or model theory), proof theory is what you get when you focus on the mechanical process of proof: how to construct proofs, how to verify them mechanically — when you treat proof as a mechanical process. I associate this with Hilbert partly because Hilbert’s logical program amounted to saying the only things that matters are the axioms and the rules of inference. The meanings of the words in ordinary language don’t matter. When we read the axioms and theorems of geometry that relate to points, lines, and planes, Hilbert is supposed to have said, we must be willing to understand them as if they referred instead to beer mugs, benches, and tables. As long as the beer mugs, benches, and tables obey the axioms, then all the theorems follow. The only meaning of words like point, line, or plane is given by the axioms and the properties and relations entailed by the axioms.

A later mathematician characterized Hilbert’s view as essentially reducing logic to a meaningless game played with empty symbols.^[5] There seems to me to be a serious purpose to that emptying out of meaning: if we can manage to make mathematical proof a meaningless game, then the only thing that will matter will be whether a proof follows the rules of the game. If the symbols have been drained of all meaning beyond what is given in the axioms, then there is much less chance of unstated assumptions sneaking into the proof. The history of attempts at formalizing logic is full of cases where unstated assumptions did manage to sneak in. Euclid’s theorems, for example, don’t actually all follow from his axioms; Frege identified some unstated assumptions that must be made in order for the theorems to follow from the axioms.

But Frege was interested, as I mentioned, in the clarification of concepts. This entails careful consideration of the meaning of terms. It’s not hard to imagine that draining terms of all meaning, in the style of Hilbert, would not appeal much to Frege. Frege wanted logic to be clean and formal, but he is interested in reasoning about real things, not about empty symbols. And he appears to have been troubled by the suggestion that the axioms of geometry might just as well be thought of as applying to beer mugs, benches, and tables, as to points, lines, and planes.

Now, like everything else, I see this tension between proof theory and model theory reflected in the world of markup. We all write specifications of various kinds: we specify vocabularies, we specify languages, we specify software tools. And specifications typically have conformance clauses.^[6] When we use specifications in real systems we often need to talk about the question Is X a conformant implementation (or application, or whatever) of Y? We would like that question to have a crisp answer. And we would like it to be consistent among people; we would not like the answer to the question Is this a conforming application of TEI? to depend on the mental state of the person making the judgment.

One way to do that is to ensure that all conformance rules are empirically checkable. That way, assuming that we can agree on what the empirical tests show, we can agree on whether X is conforming to Y or not. So, for example, in the XSD specification version 1.1, there are explicit regular expressions and explicit context-free grammars — go figure — which define the lexical spaces of all of the simple types. This replaces some slightly informal, occasionally handwaving prose in version 1.0. Nobody really complained about the prose of 1.0, but version 1.1 is much cleaner because it is much easier to check mechanically whether a given string is or is not potentially a literal value in a given simple type. So the rules of 1.1 are more easily testable.

Some people say that all conformance rules should be testable assertions. I can see their point. And yet, I am not wholly convinced. XSD also says that for each simple type, the lexical space is the set of finite strings that match the specified grammar or pattern. There are public comments on the spec saying, Really, you shouldn’t say that. You shouldn’t say that they are finite strings because that is not a testable assertion. You can’t write a test to distinguish a processor that successfully excludes all infinite strings! [audience laughter] And therefore it is not a testable assertion, and it shouldn’t be a normative statement. I had to say at least once to the Working Group as a whole and more than once to some individuals in the Working Group, We do need that statement, even though I agree I don’t know how to write that test, because if the strings in question are not guaranteed finite, the regular expressions do not have a defined meaning. If we want the regular expressions to be a testable conformance statement for the lexical space of a simple type, we have to specify that the strings are finite, because if the string is infinite, the regular expression is untestable.

A similar problem comes up in vocabulary conformance. For any large vocabulary designed for wide use and local adaptation — like all the ones discussed on Monday — we often want and behave as if we had rules that allow reasonable customizations [Kimber 2019, Lapeyre 2019, Viglianti 2019, Vitali and Palmirani 2019, Walsh 2019]. We often have a sort of gut feeling of what constitutes a reasonable customization. It’s clear, for example, that HTML is modularized and it’s intended to be modularized in a way that makes it easy for you to adapt it and use parts of HTML in other vocabularies. And it’s clear that the drafters of the HTML modularization spec thought that some adaptations should count as reasonable and conforming, and that others should count as not reasonble and non-conforming. But defining the boundary between what is a reasonable adaptation and what is a non-reasonable adaptation is very difficult. The closest that anybody has come are the vocabularies like DITA, which say the only thing you can do is restriction. This works because restriction, at least, we can mostly test (syntactic restriction). If we want to allow any syntactic extension at all, however, experience shows that it’s very difficult to distinguish reasonable changes from unreasonable changes, and the upshot is that some people end up saying, either out of conviction or because they can’t think of any way to get out of it, Well, the set of legal syntactic changes are anything you can do by redefining any of our parameter entities. And if you have a vocabulary like TEI or JATS or HTML, that essentially means you can gut the entire place, rebuild it from scratch, and call it an adaptation.

The meta-schema approach that Wendell Piez discussed this morning illustrates this problem as well, by the rules it imposes [Piez 2019]. Not only do the XML representations of particular data have to conform to an XSD schema — and the JSON files conform to a JSON schema — but the designers of the system have imposed upon themselves the rule that the two schemas have to say the same things in order to avoid having any rules for JSON files that cannot be checked mechanically by a JSON schema checker, and analogously for the XML side.

On the other hand, JATS people and TEI people and DITA people all say Whatever you do, don’t mess with the semantics, and in those communities we will find many people who want preservation of semantics to be part of the conformance rule. Because messing with the semantics is just beyond the pale; we don’t want it to happen. We want to discourage it, and to the extent that our definition of conformance has any effect in the real world, to the extent that we’re programmed to think of conformance as a positive thing, we don’t want to apply that badge of approval to something of which we disapprove. But we have a problem: nobody knows how to define semantics or the preservation of semantics in a mechanically-testable way.

This may be related to our level of understanding what we’re talking about. If we understand something really, really well, we can often reduce it to a set of mechanically checkable rules. Indeed, we often take that as a measure of understanding. If you can’t reduce something to mechanically checkable rules, we sometimes think and say, then you don’t really understand it. I believe that this intuition may be part of the rationale for the rule that says normative statements should always be testable assertions. On this view, untestable assertions indicate you haven’t really thought it through and don’t really understand your conformance requirements.

I should make explicit here that I’m associating the notion of mechanically performable tasks (like mechanically checkable proofs) with mechanically checkable validity and mechanically checkable conformance and proof theory and Hilbert all on one side, and I am associating everything else — in particular the idea that there may be things that we can’t say explicitly, or at least not in a mechanically-checkable way — with Frege and with model theory. Any listeners or readers who actually understand proof theory and model theory are asked to be kind; if necessary, please regard it as a rather fanciful poetic analogy. Perhaps it will be clearer just to talk in terms of things we can make explicit and do within a particular formal system, and things that are harder to handle that way — things that require that we go outside the formal system.

Working within the system

Now, there are occasional exceptions, but by and large in any system of logical proof what you can manage to prove depends in practice on how well you can use the system. If you’re good at it, you can manage proofs that other people cannot manage. The same thing is true for programming languages: all programming languages are essentially equally expressive (they’re all Turing complete), but what we can manage to write in any given programming language depends on how well we know the language and how good we are as programmers. And similarly, when we work in an XML environment or vocabulary, a lot depends on how well we use the system. So it makes sense that at a gathering like this of people who are concerned with constructing partially formalized, partially checkable systems, we spend a lot of time figuring out better ways to use what we have.

Metalinguistic reflection

Of course, our attitude toward validity is likely to vary, not just based on whether we’re thinking top-down or bottom-up, and on whether we’re using AI or not, but also based on what we think validity or schemas are for. The other day Wendell Piez, and then the group as a whole, identified several views of schemas that are intertwined but I think worth distinguishing:

The fertility of that exercise suggests to me that meta-linguistic reflection in general is going to be useful, and so I was grateful to Jeff Beck for his careful, detailed discussion of the problems that arise in one particular context, when one group of people are making rules for another group of people who are making rules for a third group of people who are going to be writing schemas and documents [Beck 2019]. Debbie Lapeyre’s survey of the history of vocabulary-making described a really remarkable shifts in attitude toward the making of vocabularies and toward the style of vocabularies that people should make and the way that they should be constrained and documented [Lapeyre 2019]. Bethan Tovey’s paper on the theory of markup and part-of-speech tagging and the way they relate gave me new perspectives on things, and I hope you as well [Tovey 2019]. And then, of course, there was Allen Renear on the problem of encoding [Renear 2019]. It seems clear to me that Bethan Tovey and Allen Renear will both line up with Frege as analysts of concepts and against the empty game with symbols team — it’s good to have them on our side [audience chuckling].

Making the system stronger

Now, back to Hilbert for a moment. There is some appeal in his method for restricting oneself rigorously to what can be made explicit and to processes or proofs that can be checked mechanically. But if we follow Hilbert in making proof and mechanizable processes into meaningless games with symbols, we risk eliciting a follow-up question that I have never known how to answer: Why should we be playing this particular game and not some other meaningless game with the same or different symbols? Why these rules of proof and not these other rules of proof? In practice, the answer is that we want proofs to guarantee the truth of the consequences given the truth of the premises. Those are, so to speak, the meta-rules for the game.

But if we started from the position that our work (whether mathematics or markup) is an empty, meaningless game with symbols, where did those meta-rules come from? Why should we play a game that follows a particular set of meta-rules and not one that violates them? What can it mean to say that a particular meaningless game with symbols guarantees the truth of the consequences, given the truth of the premises? If we care about preservation of truth as a meta-rule, then maybe the game is not meaningless after all. I don’t how it could be. So perhaps meaninglessness is not a property of the game, but only the proper spirit in which to play it? I could understand that, but that wasn’t what Hilbert seemed to be saying at the outset.^[8]

For that reason, the empty-game view of mathematics and of markup seems problematic on its face to me. I heard once about a Working Group meeting where the group was arguing about a proposed change to their specification. And at one point someone supported the change asked one of the opponents to justify the retention of the existing text from version 1.0 of the specification. What, they asked, is this paragraph trying to accomplish? To which the answer was What it is trying to accomplish is being compatible with the 1.0 specification. Now since this was the text of the 1.0 specification they were talking about, I personally would have thought that was a rather low bar for measuring the usefulness of a paragraph. (I think in fairness to the individual involved, the individual must have meant to answer not the question What is the text trying to do? but Why do you not want to change it? But I have certainly been in Working Group situations where it seemed to me that the point of any particular piece of prose was to be that particular piece of prose, and it made it hard for me to evaluate it in the same way that it’s hard for me to explain, if logic is just a meaningless game with symbols, why we should use rules that preserve truth under logical inference, and not other rules.

In theory, it doesn’t matter which programming language we use because they’re all Turing complete and what we can say in one, we can say in the other. But the subjective experience of using different languages varies a lot, and the same thing applies to markup languages. Given things like the @class attribute in HTML; or the @type attribute in TEI (which is almost but not quite universal); the @specific-use attribute of JATS; or the @role attribute of DocBook — given those semantic escape hatches, it seems clear that for a very large body of documents, there is no difference in expressive power among these vocabularies. What you can express in one, you could express in another in a loss-less way. You could develop a pair of round-trip transformations to go from one of these vocabularies to another, and back, and get back a document with the same semantics. But the subjective experience of using the vocabularies is quite different, because some of those ways of rendering the meaning will be extremely inconvenient, and others will not. So it makes sense that in addition to teaching ourselves to use our systems as well as we can, we spend a lot of time working on making our systems as capable as possible and extending their boundaries, extending their expressive power, and extending their convenience.

The work by Anne Brüggemann-Klein, Christina Grubmüller, Philipp Ulrich, and their absent collaborator is a good example here [Al-Awadai et al. 2019]. They have found ways to make WebSockets available to the XML stack, and to derive automatic state-checking procedures from a statechart XML document. Those techniques will make a huge improvement in the lives of anyone who uses the XML stack to build the kind of applications that the authors are talking about. And does anyone now build applications that don’t run in the web? For those people it might not be quite so important, but I think for the 99% it is very important. Hugh Cayless’s work on making TEI standoff markup work in the browser [Cayless 2019] marks a similar advance in convenience for users of the XML stack. Hugh was politely diffident about his work and maintained that it still has a way to go, but I think he has gotten quite a distance, and I look forward to seeing him get the rest of the way. Ashley Clark’s report from the Women Writers Project described their tools and a process of gradual improvement over time in their ability to perform the extremely difficult, deceptively simply-described task of showing the user all the words in the text [Clark 2019]. For those of us who occasionally struggle when we attempt to advance the state of our tools, it is inspiring to see such consistent, assiduous work even in cases where every inch of progress costs an awful lot of effort. And for the same reason I was extremely grateful to Norm Walsh and Gerrit Imsieke for their presentation on XProc 3.0 [Walsh and Berndzen 2019]: as someone who falls both into the class of people who have successfully used XPath 1.0, and into the class of people who have crashed and burned spectacularly in efforts to use XPath 1.0, I am extremely grateful for the prospect of an XProc language that is more usable and more powerful.

A different boundary between our explicitly formalized systems and the rest of the world was addressed by Jim Mason, when he traced the history of the idea that at least some of what is implicitly present in a text might be made explicit without overt markup [Mason 2019]. To be honest, my experience with SGML markup minimization was that it was always error-prone when I tried it, so I never got the results I hoped for [audience chuckling]. But the idea is nevertheless a compelling one, as illustrated by its perpetual recurrence in new forms. Equally compelling is the idea behind Sam Wilmott’s talk: that if our languages define the worlds in which we can think, then defining a new language amounts to defining a new world [Wilmott 2019]. I think we should all be grateful to Sam for showing us the prospect of a new world in which to think and work.

Often, I think we can think of the work we’re trying to do as trying to take some problem, or some application domain, and move it from the realm of the implicit and unspecified and inexplicit into the light, into a place where we can name things and make things explicit and, in lucky cases at least, formalize them. But there are cases where we may never make it to complete explicitness. Chandi Perera’s talk on accessibility the other day gave us a good example of a case where validity and success in passing every mechanical test we can devise is perhaps a necessary condition, but is not a sufficient guarantor of accessibility. Why? Because accessibility involves the communication of understanding to the reader — making information accessible to the reader — and it is questions of meaning and understanding and semantics that we have the hardest trouble formalizing.

Conclusion

I began by talking about Frege and Hilbert and their varying approaches to formal logic. Some of you may have been saying, Wait. How can you talk about formal logic at the turn of the century and mention Frege and Hilbert and not mention Kurt Gödel? Well, you’re right; I can’t [audience laughter]. Kurt Gödel proved a number of important theorems in his life; he is best-known for his two incompleteness theorems [Gödel 1931]. But the first major result that he proved and announced at a scholarly conference was a completeness theorem. He proved the completeness of first-order predicate calculus, that is, roughly the logic that Russell and Whitehead defined in their Principia Mathematica [Whitehead and Russell 1910-1913] and was formalized in different ways later by Hilbert. And that completeness theorem is worth thinking about for a moment. What he proved was that every statement which is true in all possible worlds, that is, under every possible interpretation of a particular set of logical sentences, is provable; and every statement that is provable is true in all possible interpretations. So what he showed was that proof is complete for first-order predicate calculus. And then the next day in a closing discussion at that conference, he got up and said, Oh, and by the way, I’ve also proved that it’s incomplete. [audience laughter]

Now, I won’t attempt to teach you all about Gödel’s first incompleteness theorem. Some of you will have read popularizations about it, as have I; it amounts roughly to showing first how we can encode — I’m going to use Allen Renear’s term — any logical expression in a formal, logical language, which he [Gödel] defines, as a number, and how we can construct a sentence whose meaning can be informally paraphrased as The sentence with this number is not provable. Now that is similar in some ways to Russell’s set that doesn’t contain itself in that neither of the two obvious ways to think about the sentence are quite satisfactory. If the sentence is true, then what you have established is that there are true sentences that are not provable within the system: the system is incomplete. And if the sentence is false, what you’ve established is that the sentence is actually provable, although we don’t necessarily have a proof. But that would mean that we could prove false statements. You can see how anybody would be kind of upset [audience chuckling] once they got their head around it. By all historical accounts nobody got their head around it at that meeting, so there was no cry of shock or dismay. John von Neumann apparently understood it on the train ride home and immediately wrote a letter saying, Oh, well, if that is true, it would follow that you cannot prove the consistency of first-order logic. And Gödel replied, Yes, that is quite true. I didn’t mention that result but I did achieve it before I got your letter [audience laughter].^[9]

How can it be, however, if first-order logic is complete, that we can have a Gödel sentence that is true but unprovable? The answer appears to be: the sentence has the meaning assigned only when the axioms in question are interpreted as applying to numbers. There is a whole structure of interpretation — I’ll take a risk and say meaning — associated with the sentence there. Gödel, it is worth pointing out, did not regard the sentence as undecidable; he regarded it as clearly true. He had shown the sentence to be true by a line of argument that he thought was essentially irrefutable and which has certainly never been refuted. And therefore there is a sense in which he had proved that the sentence was not provable. It’s not provable within that one system. It’s provable in a larger system, and a system, be it noted, in which the meaning that we are associating with the sentence that is involved and the numbers involved is relevant.

There is at least one philosopher who identifies Gödel’s work as the beginning of model theory [Hintikka 2000]. It is thus more than a little ironic that throughout his life Gödel exhibited not the slightest interest in model theory. He had created it, but only as a side effect. He was really only interested in proof theory. Gödel also believed that the moral of the story is not what some of the cool kids in the comparative literature department used to make of it, which is Oh, all human systems are incomplete, the world is dark, etc., etc., life is hard [audience laughter]. For Gödel, the moral of the story was: human reason cannot be reduced to a mechanical game; it always transcends the purely mechanical. Mathematics will always be interesting because there will always be a need for human reason.

At the beginning of the conference, Tommie Usdin said that she still hoped for a world in which explicit markup is possible and helps people get their work done [Usdin 2019]. I share that wish, as I expect most of you do too. I think we may never get to the point of making everything explicit; there may be some things that we just don’t know well enough to make them explicit — make them formalizable in the way that is necessary. But as Chandi Perera said about accessibility, a little bit is a lot better than none at all. And we can try. We can try to extend the boundaries of our understanding, the boundaries of our power to make things explicit and work with those things. And one of the most effective way we can do that is to help each other by getting together every now and then and talking about what we have done, both from a practical point-of-view and from a theoretical perspective because, after all, there is nothing as practical as a good theory.