Formalisation
from 1879 Frege's Begriffsschrift
Rewrite an argument in a notation where the structure is visible and nothing can hide in the wording, then check it mechanically.
- Active
- from 1879
- Where
- Jena
- Status
- In use
- Tradition
- Analytic tools
What it is
Formalisation translates an argument out of ordinary language into a notation with fixed rules. Once translated, whether the conclusion follows becomes a question that can be settled by inspection rather than by judgement.
What it buys is the elimination of rhetorical force. An argument that reads persuasively and an argument that is valid are different things, and in the notation only one of them survives.
How it works
Identify the argument's premises and conclusion in ordinary language. Choose a notation adequate to the structure — propositional logic if the argument turns on connectives, predicate logic if it turns on quantifiers and relations. Translate, resolving each ambiguity explicitly. Check validity by the rules of the system. Translate the verdict back.
Every ambiguity resolved in the third step is a decision about what the argument said, and those decisions are where the real work and the real danger both live.
The moves, in order
- Isolate premises and conclusion in ordinary language
- Choose a notation adequate to the structure
- Translate, recording each ambiguity resolved
- Check validity mechanically within the system
- Interpret the verdict back into the original terms
The procedure
Proposition The by-law does not prohibit what the ranger says it prohibits.
- The by-law reads: no person shall permit a dog to be unrestrained in a public reserve unless the reserve is a designated off-leash area and the dog is under effective control.
- Translating, the prohibition applies when: unrestrained, and not (designated area and under control).
- By the rules of the notation, not (A and B) is equivalent to (not A) or (not B). So the prohibition applies when the dog is unrestrained and either the reserve is not designated or the dog is not under control.
- The ranger has read the exception as requiring both conditions to fail before the prohibition lifts, which would make the prohibition apply only when both the area is undesignated and the dog is out of control.
- The reserve is designated and the dog was under effective control, so both conjuncts of the exception hold and the prohibition does not apply.
Therefore The by-law does not catch this case, and the disagreement was entirely about the scope of a negation that the notation makes unambiguous.
Nobody needed a theory. What settled it was rewriting one sentence in a form where the negation could not float, which is what the method is for.
What it is good for
Long arguments, arguments with nested conditions, and any dispute where the disagreement is about structure rather than content. Statutory interpretation, contract drafting and program verification are its natural homes.
Where it fails
The translation is where everything can go wrong and nothing is checked. The notation verifies the argument you wrote down, not the argument that was made, and a translation that resolves an ambiguity the wrong way produces a confident verdict about a different argument.
It also loses what will not translate. Modality, tense, degree, conversational implicature and the difference between *and* meaning conjunction and *and* meaning and then all vanish, and arguments that depend on them cannot be handled without a richer system.
Common misconceptions
That formalising makes an argument rigorous. It makes its structure checkable, which is a different thing — a formally valid argument from nonsense premises is still nonsense.
Where it came from
Frege's Begriffsschrift of 1879, which invented quantified predicate logic and made the formalisation of mathematical argument possible for the first time.
What became of it
The foundation of mathematical logic, computer science and formal verification, and a standard tool in analytic philosophy for a century.
Lasting influence
Everything computational descends from it. So does every proof assistant and every static analyser, which are formalisation carried out by machine.
Why it still matters
Enormous, and increasingly automated.
Put another way
Rewriting an argument in a language where nothing can be said with a raised eyebrow.
Texts
Gottlob Frege, Begriffsschrift
Short, revolutionary and visually forbidding. The preface is where the ambition is stated.
Where to start
Formalise a real clause from a contract or a by-law. The exercise reveals more ambiguities in an afternoon than reading about ambiguity ever will.
The surprising bit
Frege's notation was two-dimensional, nearly unreadable and adopted by almost nobody, and the ideas in it reorganised mathematics, philosophy and eventually computing.
In their own words
I believe that I can best make the relation of my ideography to ordinary language clear if I compare it to that of the microscope to the eye
Who held it
Giuseppe Peano
Connections
- Relies on
- Deduction
- Set against
- Ordinary language
- Influenced
- Logical form, Possible worlds
- Parallel to
- Logical form
The verdict
Decisive once the translation is right, and the translation is the part nothing can check.