How formal precision and informal readability work together in mathematical writing.
Mathematics uses both formal and informal language. Formal language gives precision. Informal language gives readability. A good mathematical text usually combines them.
A formal language has exact syntax. It specifies which expressions are valid and how statements are formed. For example, first-order logic has variables, quantifiers, predicates, connectives, and formation rules.
∀x (P(x) → Q(x))This expression is formal. Its structure is explicit. The quantifier binds x. The implication connects two predicates. The meaning depends on an interpretation, but the syntax is fixed.
Informal mathematical language is the language used in books, papers, lectures, and notes. It mixes ordinary prose with symbols.
Every continuous function on a compact interval is bounded.This sentence is informal, but it has precise mathematical content. In a fully formal setting, one would specify the domain, codomain, topology, definition of continuity, and definition of boundedness.
| Language | Strength | Cost |
|---|---|---|
| Formal | Exact and checkable | Verbose |
| Informal | Readable and efficient | Relies on convention |
| Structured informal | Precise enough for humans | Requires discipline |
Most mathematics is written in structured informal language. It is not fully formal, but it is constrained by definitions, notation, and proof norms.
A fully formal version of a theorem may be much longer than its textbook version. For example:
If f is continuous on [a,b], then f is bounded.A formalized version must encode real numbers, intervals, functions, continuity, order, compactness or completeness, and boundedness. The informal sentence compresses all of this using shared mathematical context.
This compression is useful. It lets readers focus on the main idea. But compression can hide assumptions.
| Informal phrase | Hidden context |
|---|---|
f is continuous | Domain, codomain, topology |
G is simple | Group? Graph? Module? |
x is small | Relative to what bound? |
almost all | Finite exceptions? Measure-one? Probability-one? |
canonical | Defined by what universal property or convention? |
Informal language becomes dangerous when hidden context changes the truth of a statement.
For example:
Every polynomial has a root.This is false over the real numbers but true over the complex numbers, for nonconstant polynomials. The statement needs a field.
Better:
Every nonconstant polynomial over C has a root in C.The improved version states the ambient structure.
Formal language avoids this ambiguity by forcing every object into a defined context. Proof assistants do this strictly. A term must have a type. A theorem must state all assumptions. A proof must use valid rules.
Informal mathematics relies on reader inference. This is efficient when the audience shares conventions. It fails when the conventions are unclear.
A good mathematical sentence makes the inferential load reasonable. It does not need to state every foundational detail, but it should state every assumption that affects the result.
Poor:
The function has an inverse.Better:
The function f : X → Y has an inverse because it is bijective.Better still, when structure matters:
The continuous bijection f : X → Y has a continuous inverse, since X is compact and Y is Hausdorff.The final version includes the assumptions needed for the topological conclusion.
Formal and informal language also differ in proof style.
A formal proof is a sequence of valid inference steps. Each step must be justified by a rule, axiom, definition, or previously proved theorem.
An informal proof is an argument written for a trained reader. It may omit routine steps, combine several logical moves, or use phrases such as “clearly,” “by construction,” or “without loss of generality.”
These phrases should be used carefully.
| Phrase | Acceptable when | Risk |
|---|---|---|
| Clearly | The step is genuinely immediate | Hides a hard argument |
| By construction | The object was defined to satisfy the property | Construction may not ensure it |
| Without loss of generality | Symmetry or reduction is explicit | May discard cases incorrectly |
| It follows | Previous result directly applies | Missing assumptions |
| Canonical | The choice is natural and invariant | May hide arbitrary choices |
Informal proof is not weaker by default. It is a different representation. A well-written informal proof can be rigorous if every omitted step is recoverable.
The key standard is reconstructability. A proof is acceptable when a competent reader can expand it into a formal proof without changing its meaning.
| Standard | Question |
|---|---|
| Local meaning | Are all symbols defined nearby? |
| Assumptions | Are required hypotheses stated? |
| Inference | Can each step be justified? |
| Scope | Are variables and cases controlled? |
| Expansion | Could the proof be formalized in principle? |
Formalization is useful for checking edge cases. It forces explicit treatment of domains, coercions, equality, termination, and dependencies. Many informal errors are type errors or missing assumptions.
For example, a proof may define a map:
f : A → Bbut later apply f to an element outside A. Informal notation may hide this. A formal system rejects it.
Similarly, a proof may use division by x without proving x ≠ 0. A formal proof requires the missing condition.
Informal writing should borrow this discipline. Before using an operation, ensure it is defined. Before invoking a theorem, check its hypotheses. Before claiming uniqueness, specify the equality relation.
The best mathematical language moves between levels.
| Level | Example | Use |
|---|---|---|
| Prose | “The map preserves distance.” | Explains idea |
| Symbolic | d(f(x), f(y)) = d(x,y) | States property |
| Formal | Typed theorem in a proof assistant | Enables checking |
These levels should support each other. Prose explains why. Symbols state what. Formalization checks how.
A useful writing pattern is:
Introduce the objects.
State the claim.
Give the idea.
Write the proof.
Record the dependencies.For example:
Let V be a finite-dimensional vector space over a field k, and let T : V → V be linear. We show that T has an invariant subspace under the stated hypotheses. The idea is to use the factorization of the characteristic polynomial. ...This style gives enough structure before symbolic manipulation begins.
Mathematical language should be formal where ambiguity would change meaning and informal where formal detail would obscure the argument. Precision and readability are not enemies. They are two constraints on the same design problem.