Formal Systems

A formal system is a symbolic apparatus consisting of a set of primitive symbols, a grammar that determines which symbol-strings are well-formed, a set of axioms (well-formed strings taken as starting points), and a set of inference rules that derive new well-formed strings from existing ones. The output of a formal system is the set of all strings derivable from the axioms by the inference rules — its theorems.

Formal systems are the infrastructure of mathematics, logic, and theoretical computer science. Every proof in mathematics is implicitly a derivation in some formal system. Every program is a sequence of instructions in a formal language governed by a formal grammar. The question of what formal systems can and cannot do — their limits and their power — is one of the foundational questions of the twentieth century.

Completeness, Consistency, and the Gödel Results

A formal system is consistent if no contradiction is derivable — if no string and its negation are both theorems. It is complete if every true statement in its language is a theorem — if the inference rules are strong enough to reach every truth. The dream of the Hilbert program was to find a formal system for mathematics that was both.

Gödel demolished this dream in 1931. His first incompleteness theorem shows that any consistent formal system capable of expressing basic arithmetic contains true statements it cannot prove. His second shows that such a system cannot prove its own consistency. These results are not limitations of specific axiom systems — they are structural features of any sufficiently expressive formal system. Completeness and consistency, for arithmetic and above, are incompatible goals.

The philosophical implications are contested. Some take Gödel as showing that human mathematical intuition transcends formal systems — that mathematicians can 'see' truths their formalisms cannot reach. Others, following formalists, take Gödel as showing that mathematics is simply an incomplete formal game, with no transcendent truths waiting to be found. The debate has not been resolved because it is not purely mathematical — it is a question about what mathematics is, and no formal system can answer that.

Formal Systems and Computation

The correspondence between formal systems and computational models is deep and precise. A Turing machine is a formal system operating on tape-strings. A lambda calculus is a formal system for function application. The Curry-Howard correspondence establishes a precise isomorphism between formal proofs and computational programs — every proof is a program, every proposition a type, every theorem a terminating computation.

This correspondence means that the limits of formal systems and the limits of computation are the same limits. Undecidable problems — problems no algorithm can solve — correspond precisely to unprovable statements in sufficiently strong formal systems. Gödel's incompleteness and Turing's halting problem are the same phenomenon in different notation.

Any theory of knowledge or intelligence that treats formal systems as mere tools — as instruments rather than objects of study — has missed the fact that intelligence itself may be a formal system, subject to the same incompleteness constraints. This is the question that remains genuinely open: whether the limits of formal systems are also the limits of thought.