Improvements outside the admitted formal language need a pre-formal stage somewhere

Type: kb/types/note.md · Tags: foundations, self-improving-systems, constraining

A proposal-selection improvement loop has two known limits: evaluation cannot select a candidate search never generates, and acceptance is warranted only for candidates the oracle can discriminate. A third concerns the representational form — the way retained content is encoded and consumed — in which any stage can inspect a candidate. An improvement whose concepts have no expression in the loop's admitted formal language is reachable only through a stage that can criticize, revise, and reject it before it has a formal representation. That stage can sit inside the loop, as a prose-reading gate or an upstream translator, or outside it, at design time, in the choice of the admitted language. In the second placement the loop's reach is fixed when the language is chosen, and learning inside that fixed decomposition inherits its mistakes. Where the stage sits is an architectural choice; that one exists somewhere is not.

The antecedent matters. A concept the admitted language already contains but the loop has not yet selected — one automaton among the automata a learner enumerates, one load-dependence among those a model grammar permits — is not outside the language. Choosing among such candidates by counterexample is revision after formal representation, and it needs no pre-formal stage inside the loop; the pre-formal work was done by whoever designed the language rich enough to contain the answer. The claim concerns externally interpreted theories about a system or its domain, read by a person or a language model. It excludes prose that binds the system through a procedure, audit, or contract.

A formal-only gate has an admission limit and a warrant limit

A formal-only gate directly admits only candidates expressed in its symbolic input language. It excludes candidates at two different boundaries. A candidate it can read may lack the proof or evidence its oracle requires: a warrant limit. A theory in another representational form is excluded before evaluation: an admission limit. The Gödel machine, the proof-gated limiting case, shows both. A rewrite may be fully expressed as a program while no proof under the fixed axioms shows that switching to it beats continuing the search — a warrant limit, which better proof search or a different axiomatization can move. And a prose conjecture — "the failures come from an unrepresented shared resource" — is not an unproved member of the candidate space; the machine searches over programs and proofs, so it is not a candidate at all — an admission limit, which stronger proof search does not touch.

Translation relocates the stage; it does not remove it

A formal-only gate can receive a prose-born improvement once something upstream formalizes it, so the gate's language bounds direct submission, not the reach of the loop around it. Translation takes two forms. A translator can resolve an unsettled theory into one determinate surrogate, fixing commitments and boundaries upstream: deciding what the prose commits to, resolving ambiguity, choosing a scope, and often revising the claim — pre-formal criticism, relocated. Or it can emit a family or disjunction of formal candidates and let later evidence eliminate members, so that revision continues within a formal representation. The second form relocates the stage further back rather than removing it: choosing which alternatives the family contains is the pre-formal decision, made once by the family's author. In either form a proof inside the selected surrogate establishes consequences under its premises; it does not establish that the surrogate preserves the source theory or fits the world. Semantic work can be relocated but not eliminated. A prose-reading gate and an upstream translator are two placements of one stage. A Gödel machine contains neither.

What the stage does, and what makes it cheap

In the stage a theory is a prototype: explicit enough to criticize and revise, with no operational machinery bound to its commitments. A language-capable critic can challenge a premise, narrow a scope, or derive a discriminating test without a build step; running the test may still need an experiment or deployment. Because the premises are explicit, reflection can target a retained commitment directly. Once the concepts stabilize, the part a formal consumer needs is codified — crossed from natural language into a symbolic artifact — while the rest stays reopenable. Many theories never leave: no formal consumer needs them, formalizing them is infeasible in practice, or their content may not be formalizable at all. The note does not estimate that residue.

Natural language is not the only prototype surface. Partial specifications and competing formal models also preserve alternatives and support revision — among alternatives an admitted language already contains. What natural language contributes is narrower and prior: it can state a commitment before any admitted language contains it. Nor does the medium make rejection cheap; authority, downstream coupling, sunk work, and rollback cost do. Nonbinding prose can motivate months of building, and a low-authority formal sketch can stay disposable. Codifying before the concepts settle freezes one projection of the theory and raises replacement cost toward entrenchment.

The relaxed Gödel machine

Commonplace has this shape, and the arrangement can be called a relaxed Gödel machine: a Gödel-shaped reflective loop with a pre-formal stage inside it. Candidates enter as natural-language theories, are criticized and revised there, and their stabilized parts harden into deterministic machinery — one worked pathway records a design decision criticized as prose and later codified into a schema and validator. The name marks the added stage only; it asserts no optimality property, and accepted changes must still become operative. It is one placement, not a template.

The stage changes the warrant target. A proof warrants entailment within a formalization; criticism judges whether the formalization's premises fit their setting, bounded by the critic's oracle domain. Neither subsumes the other. A proof gate can miss an unproved improvement or accept a valid change built on a false world-facing premise; a criticism gate can accept a bad change, after which the error becomes operative and can compound. The choice turns on the warrant required, the cost of each error, and how many candidates can be formalized at all.

World failures identify which layer must reopen

Suppose a retained theory attributes scheduler failures to demand exceeding fixed capacity. It becomes a capacity model plus a proof that the implementation respects it. Deployment still fails, because another process consumes the same resource. The proof is intact — it warrants entailment from its premises, not the interpretation that supplied them — and the world-facing premise was wrong.

Which layer reopens depends on the representation already in hand. If the model has a load-conditioned capacity parameter, a trace can revise its value and trigger a new proof without prose. If the missing dependency is precise, the symbolic model can be extended directly. If its meaning or boundary is unsettled — no admitted model says what "depends on what another process is doing" commits to — it must be stated, criticized, and bounded before a new model is built. "Parameter change" and "concept change" are relative to the model, not intrinsic to the failure. This is the codify-and-relax trajectory at the level of theories, where relaxing reopens a concept rather than swapping a component. Two external cases keep a formalization and its fit apart: Eigenius, an agent-operated execution substrate, checks proof terms in the Lean proof assistant but treats correspondence to the claim as a separate conditional check; the retained abstract-page ingest for DiscoverPhysics, a counterfactual-physics benchmark, says tasks require both a prose explanation and a Python implementation and reports that predictive accuracy can come apart from explanation quality.

Cheaper formalization moves revision into the language it already has

Formalization has separable costs — translating concepts into a model, building the artifact, generating a proof, checking it, and gathering evidence of world fit. When construction, proof, and checking fall, formal prototypes enter earlier, and where the admitted language already contains the relevant alternatives and the oracle returns discriminating counterexamples, formal iteration can settle the choice among them. For a concept outside every admitted language the bottleneck is elsewhere: deciding what the premise commits to, and obtaining evidence that the model fits the world. Cheap formalization thus defeats the cost argument for natural language without removing the stage, because it is the language's coverage, not the cost, that is short. The durable claim defends a stage, not prose, as scaffolding recurs at the deployment frontier while earlier scaffolding is absorbed. How much of a loop's candidate space lies outside its admitted language at any time is an empirical question.

Open Questions

  • When do two representations preserve enough consequences to count as the same candidate, so that a translator has moved rather than replaced it?
  • Can a loop tell, from inside, a concept outside its admitted language from one the language contains but the loop has not yet selected, or from one too costly to formalize?
  • Can a natural-language stage bound its own false-acceptance rate mechanically, or does formalizing the criticism protocol reintroduce the admission limit one level up?

Relevant Notes: