Calculemus, Amended

…sibi mutuo dicere: calculemus. G. W. Leibniz, unpublished manuscript, 1680s

The prologue left Leibniz at his counting-board, promising that two philosophers in dispute would one day need to argue no more than two accountants do. Twelve chapters later, here is what was left of the promise when someone built the board.

It did not mean that disputes end. The teacher and the pupil of the first chapter are exactly where Gellius left them, except that their argument now has four written answers instead of two shouted ones, and you can see which of the four you gave. Titius still wants his thing back from Maevius, and six bodies of law still split three against three, except that the one fact that flips three of them has a name. The bear still gets the roots. Points nine and ten of a document signed in Minsk still do not say which comes first, and the machine, asked, said so twice and stopped.

What the promise meant was narrower and, I think, better. Let us calculate does not mean let us settle it by calculation. It means: we wrote down the rules, the facts and the disputed readings, and the machine showed which answers follow from them and which do not. A dispute run through this machine comes back sorted: here is the part that follows from the rules and facts accepted for this calculation, whose acceptance remains open to challenge; here is the part that follows only if you read the text this way; here is the part where the rules are silent; here is the part that someone with authority must decide; here is the part the model never contained. The philosophers still have to argue. They argue about less, and they can see what they are arguing about.

Three negations, once more

The book was built on three sentences, each with a “not” in it, and each chapter tried to earn one.

The answer is not a verdict. It comes in four kinds, and “not established” is not “refuted”; it comes with a date, and changing the date changes it; it comes with a list of what was assumed; and when the rules hand the question to a court, or to the bear, the machine hands it on and says so, rather than guessing. A reader who receives an answer from a machine of this kind and reads only its first word has not read the answer.

The model is not the source. What answers is a reading of the statute built by someone, to some depth, with some things left out, and the reading is inspected, measured, and open to objection through channels that change nothing by themselves. A calculation can return the right date while citing the wrong basis. Checking whether an answer follows from a model does not establish whether the model follows from the law. That question is a person’s.

The proof is not the truth. Two programs agreeing byte for byte proves they agree. A certificate accepted by the checker proves that the conclusion follows from these rules and these facts for the steps the checker confirmed. The remaining steps it took as assumptions, and it named them one per line. A comparison can agree even when a premise is missing; the certificate must be checked against its own requirements. Green is a claim about what the check checks. It is worth having. It is not truth.

What the machine refuses, and where

Six questions have emerged throughout the book. Here they are together, with the boundaries each one reveals.

Does the machine ever refuse to answer? Yes, in three ways that look different: when the rules assign the question to a judge, it returns a request addressed to that judge; when the answer depends on a reading that has not been chosen, it returns “not established” with the empty line for readings showing; when a fact the rules require has not been supplied, it says which one, and will not fill it in. The bear’s question, the seven days, the one-tenge confirmation.

What happens when the law is silent? “Not established”, which is a different answer from “refuted”, and the machine keeps them apart even where a human reader would merge them. Gaius after a year of possession; the closed list of the Minsk note.

Who chose the reading? A named person, in a named place, and the choice can be switched by the reader without touching the rules. The seven-day clock; the sequencing of Minsk.

What does the model leave out? The system records which parts of a source have executable coverage and which remain outside it. Where exclusions are deliberate, their reasons can be recorded. Where no explanation has been supplied, that absence must remain visible. The Social Code; the eight blocks of the comparative chain.

If every check passes, is the answer right? No. The checks measure agreement between the machine and its own record of what it checks. The independent comparison; the certificate whose references must all lead to stated grounds.

What does the proof prove? Inference, and only inference, from these rules and these facts, with the assumptions listed one per line. The checker’s verbose report; the forged certificate refused.

The author’s choices

Every case in this book was chosen, and I have tried to say so where it mattered. I chose old and foreign cases where I could, because a reader who has no stake in Protagoras or Titius can watch the machine without watching their own money. I chose a model contract and a fairy tale for the chapters about amendment and calculation because they let us change a condition without confusing an example with an actual dispute. I chose to run every case on the day I wrote about it and to print what came back, including the limits on what each answer establishes, because a book about a machine that claims to be checkable has to be checkable itself. The examples state their conditions so that a reader can challenge a premise, a reading or a step rather than merely trust the conclusion.

I did not choose the machine’s answers. Where I expected one and got another, the other is what is printed: the year that Gaius’s answer was “not established” rather than “refuted”; the difference between a checked inference and a step admitted as an assumption.

Calculemus, amended

Leibniz imagined the accountants sitting down together and agreeing on the sum. The picture is right and the moral was too large. Two accountants agree on sums because sums are the kind of thing one agrees on; the philosophers’ dispute was never a sum, and no board will make it one.

What a board can do, it turns out, is tell the philosophers which of their sentences were sums all along, and which were readings, and which were silences, and which were somebody’s to decide. That is less than Leibniz hoped, and it comes with a condition he did not write down, which this book has tried to write for him.

Let us calculate. And let us write down, beside every answer, what we did not.