Five stops. From no intuition to a working map of what formal systems can and cannot do, and what can be built within those limits.
"This sentence is false."
Assign it a truth value.
Suppose we try to define truth formally. We want a predicate T(x) such that for every sentence s in our language:
T("s") ↔ s
Watch what happens when we apply it.
Take a consistent, effectively axiomatized formal system strong enough to represent the relevant arithmetic; use PA as the running example. Gödel constructs a sentence that can be read, at the metalevel, as:
What happens when PA tries to settle G?
Three related constructions.
The Liar tried to settle its own truth. Tarski's T tried to define truth for every sentence including the one defining T. Gödel's G claimed something about its own provability. Each case: a system trying to settle a property of itself, where the property requires stepping outside the system to evaluate.
Diagonalization and fixed-point constructions connect the Liar paradox, Tarski's undefinability theorem, Gödel's incompleteness theorems, Rice's theorem, and the halting problem. Lawvere's fixed-point theorem supplies a general categorical framework for many such results; their hypotheses and conclusions still differ.
The alignment section asks where analogous self-reference might arise in AI evaluation. That extrapolation is not a consequence of the theorems.
Suppose you are trying to build an AI system aligned with human values. Three possible analogies are worth keeping separate.
A value specification may be incomplete, context-dependent, or partly about how future cases should be evaluated. That is a specification problem. It resembles the object-language/metalanguage distinction, but it does not automatically instantiate Tarski's theorem.
↳ Question: which judgments must remain outside the formal target?
A verifier establishes only properties expressible in its specification language and justified by its proof system. Gödelian incompleteness applies only if that system meets the theorem's preconditions; many bounded verification problems do not.
↳ Question: what lies outside the verifier's declared scope?
Optimization can weaken the relationship between a measurable proxy and its intended target. This is a Goodhart-style empirical failure mode, not a diagonal theorem.
↳ Separate question: under which interventions does the proxy remain valid?
A toy framing compares two reporters: a translator intended to report world-facts and a simulator intended to report human belief. This distinction helps expose different validation targets; it does not prove that either reporter must encounter a particular theorem. The full argument ~>
The formal results are structural within their stated hypotheses. Restricting a language or task can place a verifier outside those hypotheses, although other limitations may remain.
This is the grumeter: a formal fragment whose claims are checked against an external verifier within a declared domain, not a system proven safe in general. Expressive enough for a bounded domain, sitting at the right type level, with known accuracy and explicit limits. Not trying to speak everything. Measuring how much can be spoken safely, in this domain, right now.
A grumeter for temporal hardware properties. Model checking bounded or finite-state systems can decide scoped claims such as: "this signal never exceeds threshold while this condition holds." This property language does not meet the incompleteness theorem's preconditions.
↳ Safe within scope. Silent outside.
A grumeter for equational theories. A prover can check implication claims for declared formal inputs. That checking relation is exact within the formal setup; correspondence between natural-language intent and the formal input remains external.
↳ Safe within scope. Silent outside.
A conceptual probabilistic analogue. Logical induction assigns evolving probabilities to logical sentences rather than requiring immediate truth values. Whether it provides a useful measurement instrument for this application is an open question.
↳ Safe within scope. Silent outside.
The design goal is explicit abstention outside the declared domain. The construction must still demonstrate that the boundary is enforced rather than merely asserted.
Lawvere's fixed-point theorem helps compare several diagonal results, but the alignment extrapolations remain conjectural. The ELSE region is a proposed research program: build scoped instruments, check their formal claims externally, and test whether they actually abstain outside their declared domains.