Let Us Calculate

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

Sometime in the 1680s, in a manuscript he never sent to a printer, Leibniz described a world in which arguments end quietly. When controversies arise, he wrote, two philosophers will need to dispute no more than two accountants do. It will be enough for them to take pens in hand, sit down at their counting-boards, and say to each other, with a friend called in as witness if they like: let us calculate.

The sentence is usually quoted as the daydream of a mathematician. It was not. The man who wrote it held a doctorate in law, earned at twenty, in 1666, at the small university of Altdorf, with a dissertation on perplexing cases: disputes in which the rules, honestly applied, point in two directions at once.

Here is one of the cases he examined, already ancient then. A teacher of rhetoric takes on a wealthy pupil and agrees on a fee: half now, half on the day the pupil pleads his first case in court and wins it. The pupil learns, then takes no cases. The teacher sues for the outstanding fee and addresses his pupil before the judges: you will pay either way. If I win, you pay by the judgment. If you win, you have won your first case, and you pay by the contract. The pupil reverses the argument: I pay neither way. If I win, the judgment says I owe nothing. If I lose, I have not won my first case, and the contract says I owe nothing.

Stop here and take a side. Does the pupil owe the money? Most people answer within a few seconds, and most answer with a reason the other side has already turned around. The judges in the story could not decide and put the case off to a distant day. The twenty-year-old Leibniz found a way out, in one line, and the first chapter will test it. For now, keep your answer.

In the first chapter the same case will be put to a machine, and the machine will answer it four different ways, depending on what it is told to count, before it is given Leibniz’s way out. Most answers people give are among the four. If yours is not, keep it anyway: the chapter ends with what is still open, and that is where it belongs.

Leibniz promised that calculation would end the dispute. Three centuries of attempts have given the promise a reputation, and the latest attempt speaks in fluent paragraphs: ask a language model about the law and it answers at once, with the assurance of a well-read colleague, whether or not the case it cites exists. This book is about a narrower machine. It is given the text of a rule, rewritten by a person into a form that can be run. Asked about a case, it returns what follows from that rewriting, with the articles it used beside the answer, and it stops where the rewriting stops. It does not understand, does not guess, does not decide.

In this book, formalisation means translating selected statements from a source into explicit rules and concepts that a computer can execute. Every such translation involves choices about meaning, scope and interpretation.

The question of this book is what remains in dispute after such a machine has answered. The short version: the part that turns on people, and all of it now has a name. Which reading of the text was chosen, and by whom. Which document turned a claim into a fact. Who is to decide what the text leaves to judgment. Whether the rewriting is faithful to the source. Whether the checks that vouch for the machine prove what they seem to. The machine cannot settle any of these for you. What it can do is refuse to hide them, and that is the deal this book offers: every chapter shows, in plain words, where the machine stops and hands the question back.

You will not be asked to take the machine’s word. Every chapter puts a case to it and then changes one thing: a verdict is added, a date moves, a document is withdrawn, an argument is switched on. You will be asked to say what should happen before the machine says what did. Sometimes you will be right and the machine will be right. Sometimes an answer will depend on a premise you had not noticed, and the chapter will show where it enters and what changes when it is withdrawn. The experimental notes record the dates, model versions, assumptions and result fingerprints available for the runs discussed here. They also identify gaps in the retained records; a historical summary is not a complete execution archive. This does not establish that the conclusions are true. It gives readers identifiable premises and inference steps to inspect, reproduce and challenge.

The book has three parts, and each is a denial of a sentence that will tempt you by the end of it. The answer is not a verdict: what the machine returns has no legal force, and its value lies in naming what the decision turns on. The model is not the source: between the law and the machine stands a person who rewrote the text, and every answer carries that person’s choices. The proof is not the truth: the machine is checked by a second machine and both by a written specification, and the third part asks what agreement establishes, what a certificate proves, and what neither can tell us about the truth of the premises.

The most tempting sentence of all is “the machine proved that under the law…”. It never does. It proves what a reading yields. Whether the reading is the law is a question for people, and this book is about asking it well.

It is written for anyone who has been told “it depends” and never learned on what. You may have lost a dispute and still not know whether you lost on the rule or in a gap. You may be a journalist checking a decision, an official defending one, a developer asked to automate one. Each chapter ends by identifying what remains open to challenge. Lawyers may recognise questions of interpretation, authority and evidence; engineers may recognise questions of modelling, verification and system boundaries. Neither perspective is required to follow the argument.

The machine has a name, Arxo, and its language has a name, Arxo Law. Both are open. The book is not a manual for either: manuals go out of date with the first correction, and the questions here do not.

How to Read a Machine Answer

Established: support was derived for the proposition, with none for its negation. Refuted: support was derived only for its negation. Established and refuted: both have support. Not established: neither has support. These are the four truth statuses; the last is not a negative answer.

Other labels describe other layers. Not executable concerns the model’s coverage. Admitted concerns a certificate step accepted without verification. A request for judgment concerns a decision reserved to an authority. None is a fifth truth value.

The comparisons in this book submit the same rules, facts and question to two independently written implementations and compare their answer documents. Agreement establishes agreement; it cannot by itself establish that the model is faithful to its source. The experimental notes distinguish these historical comparisons from the supplemental checks made for this revision.

The experimental notes collect the retained records and their limits.

Let us calculate, then, and keep count of what is left.