limits.html

---
layout: default
title: Limits
permalink: /limits/
epistemic_status: Conceptual explainer
epistemic_note: This is a simplified path from logic results to alignment analogies. The alignment panels pose research questions; they are not consequences of the theorems.
---

<style>
.lj { max-width: 42rem; }

.lj-intro {
  font-family: var(--font-sans);
  font-size: 0.88rem;
  color: var(--text-secondary);
  border-left: 2px solid var(--border-color);
  padding-left: 1rem;
  margin-bottom: 3.5rem;
  line-height: 1.65;
}

/* ── Section chrome ── */
.ls {
  margin-bottom: 3.5rem;
}

.ls-tag {
  font-family: var(--font-sans);
  font-size: 0.7rem;
  font-weight: 600;
  letter-spacing: 0.1em;
  text-transform: uppercase;
  color: var(--text-secondary);
  margin-bottom: 1rem;
}

.ls-stmt {
  font-size: 1.35rem;
  font-style: italic;
  color: var(--text-primary);
  margin-bottom: 1.25rem;
  line-height: 1.4;
}

.ls-prompt {
  font-size: 0.92rem;
  color: var(--text-secondary);
  margin-bottom: 0.9rem;
}

/* ── Buttons ── */
.btn-row {
  display: flex;
  gap: 0.6rem;
  flex-wrap: wrap;
  margin-bottom: 0;
}

.ibtn {
  font-family: var(--font-sans);
  font-size: 0.82rem;
  font-weight: 500;
  padding: 0.45rem 1.1rem;
  border: 1px solid var(--border-color);
  border-radius: 3px;
  background: var(--bg-primary);
  color: var(--text-secondary);
  cursor: pointer;
  transition: border-color 0.15s, color 0.15s, background 0.15s;
}

.ibtn:hover:not(:disabled) {
  border-color: var(--accent);
  color: var(--accent);
}

.ibtn.chosen {
  border-color: var(--accent);
  color: var(--accent);
  background: var(--code-bg);
}

.ibtn:disabled { opacity: 0.45; cursor: default; }

/* ── Response box ── */
.resp {
  margin-top: 1.1rem;
  padding: 1rem 1.2rem;
  border-left: 2px solid var(--accent);
  background: var(--code-bg);
  font-size: 0.92rem;
  line-height: 1.7;
}

.resp.hidden { display: none; }

.resp .note {
  margin-top: 0.75rem;
  font-style: italic;
  color: var(--text-secondary);
  font-size: 0.88rem;
}

.resp .bridge {
  margin-top: 0.9rem;
  padding-top: 0.75rem;
  border-top: 1px solid var(--border-color);
  font-size: 0.85rem;
  color: var(--text-secondary);
}

/* ── Tarski table ── */
.t-wrap {
  margin-top: 1rem;
}

.t-wrap.hidden { display: none; }

.tt {
  font-family: var(--font-mono);
  font-size: 0.8rem;
  border-collapse: collapse;
  width: 100%;
  margin-bottom: 0.8rem;
}

.tt th, .tt td {
  padding: 0.3rem 0.7rem;
  border: 1px solid var(--border-color);
  text-align: left;
}

.tt th {
  background: var(--code-bg);
  font-weight: 600;
  font-size: 0.75rem;
}

.ok  { color: #2a7a3a; }
.bad { color: var(--accent-secondary); font-weight: 600; }

.liar-row.hidden { display: none; }

/* ── Pattern diagram ── */
.pattern-diagram {
  display: flex;
  align-items: center;
  justify-content: center;
  gap: 0.9rem;
  flex-wrap: wrap;
  padding: 1rem 1.2rem;
  margin: 1.25rem 0;
  background: var(--code-bg);
  border: 1px solid var(--border-color);
  border-radius: 4px;
  font-family: var(--font-sans);
  font-size: 0.92rem;
  color: var(--text-secondary);
}

.pattern-diagram strong {
  color: var(--accent);
  font-weight: 600;
}

.pd-loop {
  font-size: 1.4rem;
  color: var(--accent-secondary);
  line-height: 1;
}

/* ── Gödel statement ── */
.g-stmt {
  font-family: var(--font-mono);
  font-size: 0.88rem;
  padding: 0.7rem 1rem;
  background: var(--code-bg);
  border: 1px solid var(--border-color);
  border-radius: 3px;
  margin-bottom: 1rem;
  color: var(--text-primary);
}

/* ── Alignment panels ── */
.al-panels {
  display: flex;
  flex-direction: column;
  gap: 0.85rem;
  margin-top: 1rem;
}

.al-panel {
  padding: 0.9rem 1.1rem;
  border: 1px solid var(--border-color);
  border-radius: 3px;
  font-size: 0.9rem;
  line-height: 1.65;
}

.al-panel p { margin-bottom: 0; }

.al-tag {
  font-family: var(--font-sans);
  font-size: 0.68rem;
  font-weight: 600;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--text-secondary);
  margin-bottom: 0.4rem;
}

.al-wall {
  font-family: var(--font-sans);
  font-size: 0.78rem;
  color: var(--accent-secondary);
  margin-top: 0.55rem;
}

/* ── Map ── */
.map-section {
  margin-top: 3.5rem;
  padding-top: 2rem;
  border-top: 1px solid var(--border-color);
}

.map-tag {
  font-family: var(--font-sans);
  font-size: 0.7rem;
  font-weight: 600;
  letter-spacing: 0.1em;
  text-transform: uppercase;
  color: var(--text-secondary);
  margin-bottom: 1.25rem;
}

.map-wrap {
  display: flex;
  border: 1px solid var(--border-color);
  border-radius: 4px;
  overflow: hidden;
  min-height: 110px;
}

.map-zone {
  padding: 0.75rem 0.9rem;
  display: flex;
  flex-direction: column;
}

.map-zone-can  {
  flex: 0 0 100px;
  background: color-mix(in srgb, var(--accent) 9%, var(--bg-primary));
  border-right: 1px solid var(--border-color);
}

.map-zone-cant {
  flex: 1;
  background: color-mix(in srgb, var(--accent-secondary) 8%, var(--bg-primary));
  border-right: 1px solid var(--border-color);
}

.map-zone-else {
  flex: 0 0 120px;
  background: var(--bg-primary);
}

.mz-label {
  font-family: var(--font-sans);
  font-size: 0.62rem;
  font-weight: 700;
  letter-spacing: 0.12em;
  text-transform: uppercase;
  color: var(--text-secondary);
  margin-bottom: 0.6rem;
}

.mz-nodes {
  display: flex;
  align-items: center;
  gap: 0.4rem;
  flex-wrap: wrap;
  flex: 1;
}

.mnode {
  font-family: var(--font-sans);
  font-size: 0.72rem;
  font-weight: 600;
  padding: 0.28rem 0.55rem;
  border-radius: 3px;
  text-align: center;
  line-height: 1.3;
}

.mnode sub {
  display: block;
  font-size: 0.58rem;
  font-weight: 400;
  color: var(--text-secondary);
}

.mnode-can {
  border: 1px solid var(--accent);
  color: var(--accent);
}

.mnode-cant {
  border: 1px solid var(--accent-secondary);
  color: var(--accent-secondary);
}

.mnode-align {
  border: 1px dashed var(--text-secondary);
  color: var(--text-secondary);
}

.mnode-theom {
  border: 1px solid var(--accent);
  color: var(--accent);
  opacity: 0.7;
}

.mz-lawvere {
  font-family: var(--font-sans);
  font-size: 0.58rem;
  color: var(--text-secondary);
  margin-top: 0.4rem;
  font-style: italic;
}

.marrow {
  color: var(--border-color);
  font-size: 0.75rem;
  flex-shrink: 0;
}

.map-note {
  font-family: var(--font-sans);
  font-size: 0.78rem;
  color: var(--text-secondary);
  margin-top: 0.75rem;
  line-height: 1.55;
}
</style>

<div class="lj">

  <div class="epistemic-note">
    <span class="epistemic-label">Conceptual explainer</span>
    <span>This is a simplified path from logic results to alignment analogies. The alignment panels pose research questions; they are not consequences of the theorems.</span>
  </div>

  <p class="lj-intro">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.</p>

  <!-- ════════════════════════════════════════
       I. THE LIAR
  ════════════════════════════════════════ -->
  <section class="ls" id="s-liar">
    <div class="ls-tag">I · The Liar</div>

    <p class="ls-stmt">"This sentence is false."</p>
    <p class="ls-prompt">Assign it a truth value.</p>

    <div class="btn-row">
      <button class="ibtn" id="l-t" onclick="liar(this,'true')">True</button>
      <button class="ibtn" id="l-f" onclick="liar(this,'false')">False</button>
    </div>

    <div id="liar-resp" class="resp hidden">
      <span id="liar-body"></span>
      <p class="note">Neither assignment survives in the ordinary two-valued treatment. This motivates restrictions on self-applying truth predicates; by itself, the example is not Tarski's theorem.</p>
      <p class="bridge">Tarski asked: what exactly does this tell us about what truth can be, and where it can be defined?</p>
    </div>
  </section>

  <!-- ════════════════════════════════════════
       II. TARSKI
  ════════════════════════════════════════ -->
  <section class="ls" id="s-tarski">
    <div class="ls-tag">II · Tarski</div>

    <p>Suppose we try to define truth formally. We want a predicate <code>T(x)</code> such that for every sentence <em>s</em> in our language:</p>
    <p style="font-family:var(--font-mono);font-size:0.88rem;margin:0.75rem 0 1rem 1rem;">T("s") &harr; s</p>

    <p class="ls-prompt">Watch what happens when we apply it.</p>

    <div class="btn-row">
      <button class="ibtn" onclick="tarski1(this)">Apply T to ordinary sentences ~></button>
    </div>

    <div id="t-table" class="t-wrap hidden">
      <table class="tt">
        <tr><th>Sentence</th><th>Content</th><th>T("s") ↔ s</th></tr>
        <tr>
          <td>P</td>
          <td>"Snow is white."</td>
          <td class="ok">✓ works</td>
        </tr>
        <tr>
          <td>Q</td>
          <td>"Grass is green."</td>
          <td class="ok">✓ works</td>
        </tr>
        <tr class="liar-row hidden" id="lrow">
          <td>L</td>
          <td>"T(L) is false."</td>
          <td class="bad">T("L") ↔ ¬T("L") &nbsp;⚡</td>
        </tr>
      </table>
      <div class="btn-row" id="t-btn2-wrap">
        <button class="ibtn" onclick="tarski2(this)">Now apply T to the Liar sentence ~></button>
      </div>
    </div>

    <div id="tarski-resp" class="resp hidden">
      <p><code>T("L") ↔ ¬T("L")</code> is a contradiction for this unrestricted self-applying predicate.</p>
      <p class="note">Tarski's undefinability theorem applies to sufficiently expressive formalized languages under specific assumptions: an adequate truth predicate for the language cannot be defined within that same language. A richer metalanguage is one standard response.</p>
      <p class="bridge">Under which conditions can a formal system prove every sentence true in its intended interpretation?</p>
    </div>
  </section>

  <!-- ════════════════════════════════════════
       III. GÖDEL
  ════════════════════════════════════════ -->
  <section class="ls" id="s-godel">
    <div class="ls-tag">III · Gödel</div>

    <p>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:</p>

    <div class="g-stmt">G &nbsp;:&nbsp; "This statement is not provable in PA."</div>

    <p class="ls-prompt">What happens when PA tries to settle G?</p>

    <div class="btn-row">
      <button class="ibtn" id="g-prove"   onclick="godel(this,'prove')">PA proves G</button>
      <button class="ibtn" id="g-noprove" onclick="godel(this,'noprove')">PA cannot prove G</button>
    </div>

    <div id="godel-resp" class="resp hidden">
      <span id="godel-body"></span>
      <p class="note" id="godel-note"></p>
      <p class="bridge">For systems meeting the theorem's hypotheses, provability does not exhaust truth in the intended interpretation. This conclusion is scoped to those hypotheses, not to every formal language or verification task.</p>
    </div>
  </section>

  <!-- ════════════════════════════════════════
       INTERLUDE: THE PATTERN
  ════════════════════════════════════════ -->
  <section class="ls" id="s-pattern">
    <div class="ls-tag">The pattern</div>

    <p>Three related constructions.</p>

    <p>The Liar tried to settle its own truth. Tarski's <code>T</code> tried to define truth for every sentence including the one defining <code>T</code>. Gödel's <code>G</code> claimed something about its own provability. Each case: <strong>a system trying to settle a property of itself</strong>, where the property requires stepping outside the system to evaluate.</p>

    <div class="pattern-diagram">
      <span>System <strong>S</strong></span>
      <span class="pd-loop">&#x21BA;</span>
      <span>evaluates property <strong>P</strong> of <strong>S</strong></span>
    </div>

    <p>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.</p>

    <p class="ls-prompt" style="margin-top:1.4rem;">The alignment section asks where analogous self-reference might arise in AI evaluation. That extrapolation is not a consequence of the theorems.</p>
  </section>

  <!-- ════════════════════════════════════════
       IV. ALIGNMENT
  ════════════════════════════════════════ -->
  <section class="ls" id="s-align">
    <div class="ls-tag">IV · Alignment</div>

    <p>Suppose you are trying to build an AI system aligned with human values. Three possible analogies are worth keeping separate.</p>

    <div class="al-panels">
      <div class="al-panel">
        <div class="al-tag">Analogy: specifying "aligned"</div>
        <p>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.</p>
        <p class="al-wall">&#x21B3; Question: which judgments must remain outside the formal target?</p>
      </div>

      <div class="al-panel">
        <div class="al-tag">Analogy: verifying alignment</div>
        <p>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.</p>
        <p class="al-wall">&#x21B3; Question: what lies outside the verifier's declared scope?</p>
      </div>

      <div class="al-panel">
        <div class="al-tag">Empirical risk: optimizing a proxy</div>
        <p>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.</p>
        <p class="al-wall">&#x21B3; Separate question: under which interventions does the proxy remain valid?</p>
      </div>
    </div>

    <p class="ls-prompt" style="margin-top:1.25rem;">A toy framing compares two reporters: a <strong>translator</strong> intended to report world-facts and a <strong>simulator</strong> 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 <a href="/blog/limits-of-formalization">full argument ~></a></p>
  </section>

  <!-- ════════════════════════════════════════
       V. ELSE
  ════════════════════════════════════════ -->
  <section class="ls" id="s-else">
    <div class="ls-tag">V · Else</div>

    <p>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.</p>

    <p>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.</p>

    <div class="al-panels">
      <div class="al-panel">
        <div class="al-tag">LTL + model checker</div>
        <p>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.</p>
        <p class="al-wall">&#x21B3; Safe within scope. Silent outside.</p>
      </div>
      <div class="al-panel">
        <div class="al-tag">ETP + theorem prover</div>
        <p>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.</p>
        <p class="al-wall">&#x21B3; Safe within scope. Silent outside.</p>
      </div>
      <div class="al-panel">
        <div class="al-tag">Logical induction</div>
        <p>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.</p>
        <p class="al-wall">&#x21B3; Safe within scope. Silent outside.</p>
      </div>
    </div>

    <p style="margin-top:1.25rem;font-size:0.9rem;color:var(--text-secondary);font-style:italic;">The design goal is explicit abstention outside the declared domain. The construction must still demonstrate that the boundary is enforced rather than merely asserted.</p>
  </section>

  <!-- ════════════════════════════════════════
       MAP
  ════════════════════════════════════════ -->
  <div class="map-section">
    <div class="map-tag">The map so far</div>

    <div class="map-wrap">

      <div class="map-zone map-zone-can">
        <div class="mz-label">Can</div>
        <div class="mz-nodes">
          <div class="mnode mnode-can">
            recursion
            <sub>self-ref that works</sub>
          </div>
        </div>
      </div>

      <div class="map-zone map-zone-cant">
        <div class="mz-label">Can't</div>
        <div class="mz-nodes">
          <div class="mnode mnode-cant">
            Liar
            <sub>truth collapses</sub>
          </div>
          <span class="marrow">~></span>
          <div class="mnode mnode-cant">
            Tarski
            <sub>undefinability</sub>
          </div>
          <span class="marrow">~></span>
          <div class="mnode mnode-cant">
            Gödel
            <sub>incompleteness</sub>
          </div>
          <span class="marrow">~></span>
          <div class="mnode mnode-cant">
            Rice
            <sub>semantics</sub>
          </div>
          <span class="marrow">~></span>
          <div class="mnode mnode-align">
            alignment
            <sub>open frontier</sub>
          </div>
        </div>
        <div class="mz-lawvere">one diagonal argument · Lawvere (1969)</div>
      </div>

      <div class="map-zone map-zone-else">
        <div class="mz-label">Else</div>
        <div class="mz-nodes" style="flex-direction:column;align-items:flex-start;gap:0.3rem;">
          <div class="mnode mnode-theom">LTL<sub>temporal</sub></div>
          <div class="mnode mnode-theom">ETP<sub>equational</sub></div>
          <div class="mnode mnode-theom" style="opacity:0.4;">&#x22EF;</div>
        </div>
      </div>

    </div>

    <p class="map-note">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.</p>
  </div>

</div>

<script>
function show(id) {
  document.getElementById(id).classList.remove('hidden');
}

// ── I. Liar ───────────────────────────────────
function liar(btn, val) {
  var other = document.getElementById(val === 'true' ? 'l-f' : 'l-t');
  btn.classList.add('chosen');
  btn.disabled = true;
  other.disabled = true;

  var body = document.getElementById('liar-body');
  if (val === 'true') {
    body.textContent = 'If the sentence is true, then what it says is the case: it is false. Contradiction.';
  } else {
    body.textContent = 'If the sentence is false, then what it says is not the case: it is not false, so it is true. Contradiction.';
  }
  show('liar-resp');
}

// ── II. Tarski ────────────────────────────────
function tarski1(btn) {
  btn.disabled = true;
  show('t-table');
}

function tarski2(btn) {
  btn.style.display = 'none';
  document.getElementById('lrow').classList.remove('hidden');
  show('tarski-resp');
}

// ── III. Gödel ────────────────────────────────
function godel(btn, val) {
  var other = document.getElementById(val === 'prove' ? 'g-noprove' : 'g-prove');
  btn.classList.add('chosen');
  btn.disabled = true;
  other.disabled = true;

  var body = document.getElementById('godel-body');
  var note = document.getElementById('godel-note');

  if (val === 'prove') {
    body.innerHTML = 'Under the assumptions used in Gödel\'s construction, a proof of G would conflict with what G expresses about its own provability.';
    note.textContent = 'The precise conclusion depends on the system and consistency or soundness conditions stated by the theorem.';
  } else {
    body.innerHTML = 'Gödel\'s construction shows that, for a system meeting the theorem\'s hypotheses, G is not provable within that system.';
    note.textContent = 'From the metatheory, and under the relevant assumptions, G has the intended interpretation: the system does not prove it.';
  }
  show('godel-resp');
}
</script>