Limits to Formalization

What happens when you try to measure what resists measurement.

Conceptual inquiry This page combines established results in logic with open extrapolations about specification and alignment. The extrapolations are questions, not consequences of the theorems.

What happens when you take fuzzy input and produce something measurable and checkable? Tarski and Gödel establish precise limits for formal languages and systems that meet their hypotheses.12 I use those results as reference points for a broader question: where does a mechanically checked artifact cease to support the interpretation we place on it? The analogy is suggestive, but it is not itself a theorem.

I’m interested in the maximal complexity that can be compressed through formalization, the syntax-semantics interface (where structure ends and meaning begins), and whether there exists a natural language kernel that is fully formalizable3.

One direction, inspired by iterative formal development in Lean, is to treat formalization as bootstrapping: use an implementation and its specification to construct a more precise successor. Each iteration forces syntactic commitments,4 but whether those commitments preserve the original intent remains an empirical and interpretive question.

Longer treatments: the limits-of-formalization post, the limits/ interactive that walks the first walls by hand, and the self-reference map.

  1. Roughly: an adequate truth predicate for a sufficiently expressive formalized language cannot be defined within that same language under the theorem’s hypotheses. A richer metalanguage is one standard response; the exact formulation matters. ↩

  2. Roughly: any consistent, effectively axiomatized formal system strong enough to represent the relevant arithmetic is incomplete, and under related hypotheses cannot prove its own consistency. The exact hypotheses matter. ↩

  3. Controlled natural languages (such as Attempto Controlled English) are fragments designed to map cleanly to formal logic. Where to draw a useful boundary between controlled and open-ended language is a design choice, not a settled natural division. ↩

  4. Implementation forces choices where a specification is silent. Those choices can increase precision, but they can also preserve or amplify a misunderstanding; convergence in syntax does not guarantee convergence on intent. ↩