Descriptive Complexity

Introduction

Most of computer science measures hardness by resources: how many steps does an algorithm need, how much memory? But in the 1970s, logician Ronald Fagin asked an entirely different question: what if we measured hardness by language?

His idea was to describe problems not as algorithms but as logical formulas. Given a finite structure — a graph, a database, a game board — can you write a single sentence in some logical language that is true exactly when the answer is "yes"? If so, what kind of sentence do you need?

The stunning discovery is that the complexity of the formula mirrors the complexity of the problem:

Fagin's theorem (1974, proven): A property of finite structures is in NP if and only if it can be expressed by a sentence in second-order existential logic (SO∃) — logic where you can quantify over relations, not just elements.
Immerman–Vardi theorem (1987, proven): On ordered structures, a property is in PTIME if and only if it can be expressed in first-order logic extended with a least-fixed-point operator (FO+LFP).

These are not approximations. They are exact, machine-independent characterizations of complexity classes — no Turing machines, no clocks, just the shape of the sentence that describes the problem.

This field, descriptive complexity, grew from Fagin's insight into a bridge between mathematical logic and the central questions of P vs NP.

Try It: LFP Reachability

Graph reachability — "can you get from node s to node t?" — is a canonical PTIME problem. It is also the showcase example for the least-fixed-point (LFP) operator.

The LFP formula for reachability says: R is the smallest set such that s ∈ R and, whenever u ∈ R and there is an edge (u,v), then v ∈ R. In first-order logic with LFP this is a single, finite sentence.

Below, build a directed graph (click Add edge, then click two nodes) and pick a source. Press Run LFP to watch the set R grow iteration by iteration until it stabilises — that stable set is exactly the set of nodes reachable from the source.

<p class="hint">Build a directed graph, choose a <b>source node</b>, then press <b>Run LFP</b> to watch the least-fixed-point iteration compute reachability step by step.</p>
<div id="controls">
  <button id="btn-edge" type="button" class="active">Add edge</button>
  <button id="btn-reset" type="button" class="ghost">Reset graph</button>
  <label class="src-label">Source node: <input id="src-input" type="number" min="0" max="7" value="0"></label>
  <button id="btn-run" type="button" class="run">Run LFP</button>
</div>
<div id="canvas-wrap">
  <canvas id="gc" width="480" height="300"></canvas>
</div>
<div id="log-wrap">
  <div id="log"></div>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: 14px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
#controls { display: flex; flex-wrap: wrap; gap: .45rem; align-items: center; margin-bottom: .6rem; }
.src-label { font-size: .88rem; color: #555; display: flex; align-items: center; gap: .3rem; }
#src-input { width: 48px; padding: .2rem .3rem; border: 1px solid #ccc; border-radius: 6px; font-size: .88rem; }
button { font: 600 13px system-ui, sans-serif; padding: .38rem .8rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; transition: background .12s; }
button.ghost { background: #fff; color: #1d3557; }
button.run { background: #0a7d33; border-color: #0a7d33; }
button.active { background: #e63946; border-color: #c92f3c; }
#canvas-wrap { border: 1px solid #dde4ea; border-radius: 10px; overflow: hidden; background: #f8fafb; margin-bottom: .6rem; }
canvas { display: block; cursor: crosshair; }
#log-wrap { min-height: 64px; max-height: 140px; overflow-y: auto; border: 1px solid #dde4ea; border-radius: 8px; padding: .45rem .6rem; background: #f0f4f8; }
#log { font: 13px ui-monospace, monospace; color: #1d3557; line-height: 1.65; white-space: pre-wrap; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// ── Descriptive Complexity: LFP Reachability Demo ──────────────────────────
// Nodes 0..7 are fixed in a circle. The user adds directed edges.
// "Run LFP" simulates the least-fixed-point iteration for graph reachability:
//   R_0 = {source}
//   R_{i+1} = R_i ∪ { v : ∃u ∈ R_i, edge(u,v) }
// Terminates when R_{i+1} = R_i  (fixed point reached).
// This exactly matches the FO+LFP formula for reachability (Immerman–Vardi).

const N = 8; // number of nodes
const canvas = document.getElementById('gc');
const ctx = canvas.getContext('2d');
const log = document.getElementById('log');
const W = canvas.width, H = canvas.height;
const CX = W / 2, CY = H / 2, R = 105; // layout circle

// Preloaded example edges so it works out of the box
const edges = new Set(['0,1','1,2','2,4','3,5','5,3','4,6','6,7']);

let pendingFrom = null; // first click for edge-add mode
let lfpSets = []; // snapshots for animation
let animFrame = null;

// ── Geometry ───────────────────────────────────────────────────────────────
function nodePos(i) {
  const angle = (2 * Math.PI * i / N) - Math.PI / 2;
  return { x: CX + R * Math.cos(angle), y: CY + R * Math.sin(angle) };
}
function hitNode(mx, my) {
  for (let i = 0; i < N; i++) {
    const p = nodePos(i);
    if ((mx - p.x) ** 2 + (my - p.y) ** 2 < 16 * 16) return i;
  }
  return -1;
}

// ── Drawing ────────────────────────────────────────────────────────────────
function drawArrow(x1, y1, x2, y2, color) {
  const nodeR = 14;
  const dx = x2 - x1, dy = y2 - y1;
  const len = Math.sqrt(dx*dx + dy*dy) || 1;
  const ux = dx/len, uy = dy/len;
  // start/end offset by node radius
  const sx = x1 + ux * nodeR, sy = y1 + uy * nodeR;
  const ex = x2 - ux * nodeR, ey = y2 - uy * nodeR;
  const hLen = 10, hWid = 5;
  const bx = ex - ux * hLen, by = ey - uy * hLen;
  const px = -uy * hWid, py = ux * hWid;
  ctx.beginPath();
  ctx.moveTo(sx, sy); ctx.lineTo(ex, ey);
  ctx.strokeStyle = color; ctx.lineWidth = 1.8;
  ctx.stroke();
  ctx.beginPath();
  ctx.moveTo(ex, ey);
  ctx.lineTo(bx + px, by + py);
  ctx.lineTo(bx - px, by - py);
  ctx.closePath();
  ctx.fillStyle = color; ctx.fill();
}

function draw(reachSet) {
  ctx.clearRect(0, 0, W, H);
  // edges
  edges.forEach(e => {
    const [a, b] = e.split(',').map(Number);
    const pa = nodePos(a), pb = nodePos(b);
    drawArrow(pa.x, pa.y, pb.x, pb.y, '#8fa8bf');
  });
  // nodes
  for (let i = 0; i < N; i++) {
    const p = nodePos(i);
    const inR = reachSet && reachSet.has(i);
    ctx.beginPath();
    ctx.arc(p.x, p.y, 14, 0, 2 * Math.PI);
    ctx.fillStyle = inR ? '#0a7d33' : (pendingFrom === i ? '#e63946' : '#e8eef3');
    ctx.fill();
    ctx.strokeStyle = inR ? '#074f21' : '#8fa8bf';
    ctx.lineWidth = 2;
    ctx.stroke();
    ctx.fillStyle = inR ? '#fff' : '#1d3557';
    ctx.font = 'bold 13px system-ui, sans-serif';
    ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
    ctx.fillText(i, p.x, p.y);
  }
}

// ── LFP iteration ──────────────────────────────────────────────────────────
function runLFP() {
  if (animFrame) cancelAnimationFrame(animFrame);
  const src = parseInt(document.getElementById('src-input').value, 10);
  if (src < 0 || src >= N || isNaN(src)) { logLine('Invalid source node.'); return; }
  log.textContent = '';
  logLine(fmt('── Starting LFP for reachability from node %src% ──', { src: src }));
  logLine(fmt('Formula: R = lfp λR. {%src%} ∪ {v : ∃u∈R, edge(u,v)}', { src: src }));
  logLine('');

  lfpSets = [];
  let current = new Set([src]);
  lfpSets.push(new Set(current));

  for (let round = 0; round < N + 1; round++) {
    const next = new Set(current);
    current.forEach(u => {
      edges.forEach(e => {
        const [a, b] = e.split(',').map(Number);
        if (a === u) next.add(b);
      });
    });
    const changed = next.size !== current.size || ![...next].every(x => current.has(x));
    if (!changed) {
      lfpSets.push(null); // sentinel: fixed point reached
      break;
    }
    current = next;
    lfpSets.push(new Set(current));
  }

  let step = 0;
  function animate() {
    if (step >= lfpSets.length) return;
    const snap = lfpSets[step];
    if (snap === null) {
      logLine('Fixed point reached — no new nodes added.');
      logLine(fmt('Reachable from %src%: R = { %sort% }', { src: src, sort: [...lfpSets[step-1]].sort((a,b)=>a-b).join(', ') }));
      draw(lfpSets[step - 1]);
    } else {
      if (step === 0) {
        logLine(fmt('R₀ = { %src% }  (seed: just the source)', { src: src }));
      } else {
        const prev = lfpSets[step - 1];
        const added = [...snap].filter(x => !prev.has(x));
        logLine('R' + step + ' = { ' + [...snap].sort((a,b)=>a-b).join(', ') + ' }' + (added.length ? '  (+' + added.join(',') + ')' : ''));
      }
      draw(snap);
      step++;
      animFrame = setTimeout(animate, 700);
    }
  }
  animate();
}

function logLine(s) { log.textContent += s + '\n'; log.scrollTop = log.scrollHeight; }

// ── Edge-add interaction ───────────────────────────────────────────────────
canvas.addEventListener('click', e => {
  const rect = canvas.getBoundingClientRect();
  const mx = (e.clientX - rect.left) * (W / rect.width);
  const my = (e.clientY - rect.top) * (H / rect.height);
  const hit = hitNode(mx, my);
  if (hit < 0) { pendingFrom = null; draw(null); return; }
  if (pendingFrom === null) {
    pendingFrom = hit;
    draw(null);
    logLine(fmt('Selected node %hit% as edge source. Now click target node.', { hit: hit }));
  } else {
    if (pendingFrom !== hit) {
      const key = pendingFrom + ',' + hit;
      if (!edges.has(key)) { edges.add(key); logLine(fmt('Added edge %pendingFrom% → %hit%', { pendingFrom: pendingFrom, hit: hit })); }
      else logLine(fmt('Edge %pendingFrom% → %hit% already exists.', { pendingFrom: pendingFrom, hit: hit }));
    }
    pendingFrom = null;
    draw(null);
  }
});

document.getElementById('btn-run').addEventListener('click', runLFP);
document.getElementById('btn-edge').addEventListener('click', () => {
  pendingFrom = null;
  logLine('Click a source node, then a target node to add a directed edge.');
  draw(null);
});
document.getElementById('btn-reset').addEventListener('click', () => {
  edges.clear(); pendingFrom = null;
  if (animFrame) clearTimeout(animFrame);
  lfpSets = [];
  log.textContent = 'Graph cleared. Add edges, then Run LFP.\n';
  draw(null);
});

// ── Initial render ─────────────────────────────────────────────────────────
logLine('Graph loaded with example edges (0→1→2→4→6→7, 3↔5).');
logLine('Press "Run LFP" to compute reachability from node 0, or edit the graph first.');
draw(null);

<p class="hint">Build a directed graph, choose a <b>source node</b>, then press <b>Run LFP</b> to watch the least-fixed-point iteration compute reachability step by step.</p>
<div id="controls">
  <button id="btn-edge" type="button" class="active">Add edge</button>
  <button id="btn-reset" type="button" class="ghost">Reset graph</button>
  <label class="src-label">Source node: <input id="src-input" type="number" min="0" max="7" value="0"></label>
  <button id="btn-run" type="button" class="run">Run LFP</button>
</div>
<div id="canvas-wrap">
  <canvas id="gc" width="480" height="300"></canvas>
</div>
<div id="log-wrap">
  <div id="log"></div>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: 14px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
#controls { display: flex; flex-wrap: wrap; gap: .45rem; align-items: center; margin-bottom: .6rem; }
.src-label { font-size: .88rem; color: #555; display: flex; align-items: center; gap: .3rem; }
#src-input { width: 48px; padding: .2rem .3rem; border: 1px solid #ccc; border-radius: 6px; font-size: .88rem; }
button { font: 600 13px system-ui, sans-serif; padding: .38rem .8rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; transition: background .12s; }
button.ghost { background: #fff; color: #1d3557; }
button.run { background: #0a7d33; border-color: #0a7d33; }
button.active { background: #e63946; border-color: #c92f3c; }
#canvas-wrap { border: 1px solid #dde4ea; border-radius: 10px; overflow: hidden; background: #f8fafb; margin-bottom: .6rem; }
canvas { display: block; cursor: crosshair; }
#log-wrap { min-height: 64px; max-height: 140px; overflow-y: auto; border: 1px solid #dde4ea; border-radius: 8px; padding: .45rem .6rem; background: #f0f4f8; }
#log { font: 13px ui-monospace, monospace; color: #1d3557; line-height: 1.65; white-space: pre-wrap; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// ── Descriptive Complexity: LFP Reachability Demo ──────────────────────────
// Nodes 0..7 are fixed in a circle. The user adds directed edges.
// "Run LFP" simulates the least-fixed-point iteration for graph reachability:
//   R_0 = {source}
//   R_{i+1} = R_i ∪ { v : ∃u ∈ R_i, edge(u,v) }
// Terminates when R_{i+1} = R_i  (fixed point reached).
// This exactly matches the FO+LFP formula for reachability (Immerman–Vardi).

const N = 8; // number of nodes
const canvas = document.getElementById('gc');
const ctx = canvas.getContext('2d');
const log = document.getElementById('log');
const W = canvas.width, H = canvas.height;
const CX = W / 2, CY = H / 2, R = 105; // layout circle

// Preloaded example edges so it works out of the box
const edges = new Set(['0,1','1,2','2,4','3,5','5,3','4,6','6,7']);

let pendingFrom = null; // first click for edge-add mode
let lfpSets = []; // snapshots for animation
let animFrame = null;

// ── Geometry ───────────────────────────────────────────────────────────────
function nodePos(i) {
  const angle = (2 * Math.PI * i / N) - Math.PI / 2;
  return { x: CX + R * Math.cos(angle), y: CY + R * Math.sin(angle) };
}
function hitNode(mx, my) {
  for (let i = 0; i < N; i++) {
    const p = nodePos(i);
    if ((mx - p.x) ** 2 + (my - p.y) ** 2 < 16 * 16) return i;
  }
  return -1;
}

// ── Drawing ────────────────────────────────────────────────────────────────
function drawArrow(x1, y1, x2, y2, color) {
  const nodeR = 14;
  const dx = x2 - x1, dy = y2 - y1;
  const len = Math.sqrt(dx*dx + dy*dy) || 1;
  const ux = dx/len, uy = dy/len;
  // start/end offset by node radius
  const sx = x1 + ux * nodeR, sy = y1 + uy * nodeR;
  const ex = x2 - ux * nodeR, ey = y2 - uy * nodeR;
  const hLen = 10, hWid = 5;
  const bx = ex - ux * hLen, by = ey - uy * hLen;
  const px = -uy * hWid, py = ux * hWid;
  ctx.beginPath();
  ctx.moveTo(sx, sy); ctx.lineTo(ex, ey);
  ctx.strokeStyle = color; ctx.lineWidth = 1.8;
  ctx.stroke();
  ctx.beginPath();
  ctx.moveTo(ex, ey);
  ctx.lineTo(bx + px, by + py);
  ctx.lineTo(bx - px, by - py);
  ctx.closePath();
  ctx.fillStyle = color; ctx.fill();
}

function draw(reachSet) {
  ctx.clearRect(0, 0, W, H);
  // edges
  edges.forEach(e => {
    const [a, b] = e.split(',').map(Number);
    const pa = nodePos(a), pb = nodePos(b);
    drawArrow(pa.x, pa.y, pb.x, pb.y, '#8fa8bf');
  });
  // nodes
  for (let i = 0; i < N; i++) {
    const p = nodePos(i);
    const inR = reachSet && reachSet.has(i);
    ctx.beginPath();
    ctx.arc(p.x, p.y, 14, 0, 2 * Math.PI);
    ctx.fillStyle = inR ? '#0a7d33' : (pendingFrom === i ? '#e63946' : '#e8eef3');
    ctx.fill();
    ctx.strokeStyle = inR ? '#074f21' : '#8fa8bf';
    ctx.lineWidth = 2;
    ctx.stroke();
    ctx.fillStyle = inR ? '#fff' : '#1d3557';
    ctx.font = 'bold 13px system-ui, sans-serif';
    ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
    ctx.fillText(i, p.x, p.y);
  }
}

// ── LFP iteration ──────────────────────────────────────────────────────────
function runLFP() {
  if (animFrame) cancelAnimationFrame(animFrame);
  const src = parseInt(document.getElementById('src-input').value, 10);
  if (src < 0 || src >= N || isNaN(src)) { logLine('Invalid source node.'); return; }
  log.textContent = '';
  logLine(fmt('── Starting LFP for reachability from node %src% ──', { src: src }));
  logLine(fmt('Formula: R = lfp λR. {%src%} ∪ {v : ∃u∈R, edge(u,v)}', { src: src }));
  logLine('');

  lfpSets = [];
  let current = new Set([src]);
  lfpSets.push(new Set(current));

  for (let round = 0; round < N + 1; round++) {
    const next = new Set(current);
    current.forEach(u => {
      edges.forEach(e => {
        const [a, b] = e.split(',').map(Number);
        if (a === u) next.add(b);
      });
    });
    const changed = next.size !== current.size || ![...next].every(x => current.has(x));
    if (!changed) {
      lfpSets.push(null); // sentinel: fixed point reached
      break;
    }
    current = next;
    lfpSets.push(new Set(current));
  }

  let step = 0;
  function animate() {
    if (step >= lfpSets.length) return;
    const snap = lfpSets[step];
    if (snap === null) {
      logLine('Fixed point reached — no new nodes added.');
      logLine(fmt('Reachable from %src%: R = { %sort% }', { src: src, sort: [...lfpSets[step-1]].sort((a,b)=>a-b).join(', ') }));
      draw(lfpSets[step - 1]);
    } else {
      if (step === 0) {
        logLine(fmt('R₀ = { %src% }  (seed: just the source)', { src: src }));
      } else {
        const prev = lfpSets[step - 1];
        const added = [...snap].filter(x => !prev.has(x));
        logLine('R' + step + ' = { ' + [...snap].sort((a,b)=>a-b).join(', ') + ' }' + (added.length ? '  (+' + added.join(',') + ')' : ''));
      }
      draw(snap);
      step++;
      animFrame = setTimeout(animate, 700);
    }
  }
  animate();
}

function logLine(s) { log.textContent += s + '\n'; log.scrollTop = log.scrollHeight; }

// ── Edge-add interaction ───────────────────────────────────────────────────
canvas.addEventListener('click', e => {
  const rect = canvas.getBoundingClientRect();
  const mx = (e.clientX - rect.left) * (W / rect.width);
  const my = (e.clientY - rect.top) * (H / rect.height);
  const hit = hitNode(mx, my);
  if (hit < 0) { pendingFrom = null; draw(null); return; }
  if (pendingFrom === null) {
    pendingFrom = hit;
    draw(null);
    logLine(fmt('Selected node %hit% as edge source. Now click target node.', { hit: hit }));
  } else {
    if (pendingFrom !== hit) {
      const key = pendingFrom + ',' + hit;
      if (!edges.has(key)) { edges.add(key); logLine(fmt('Added edge %pendingFrom% → %hit%', { pendingFrom: pendingFrom, hit: hit })); }
      else logLine(fmt('Edge %pendingFrom% → %hit% already exists.', { pendingFrom: pendingFrom, hit: hit }));
    }
    pendingFrom = null;
    draw(null);
  }
});

document.getElementById('btn-run').addEventListener('click', runLFP);
document.getElementById('btn-edge').addEventListener('click', () => {
  pendingFrom = null;
  logLine('Click a source node, then a target node to add a directed edge.');
  draw(null);
});
document.getElementById('btn-reset').addEventListener('click', () => {
  edges.clear(); pendingFrom = null;
  if (animFrame) clearTimeout(animFrame);
  lfpSets = [];
  log.textContent = 'Graph cleared. Add edges, then Run LFP.\n';
  draw(null);
});

// ── Initial render ─────────────────────────────────────────────────────────
logLine('Graph loaded with example edges (0→1→2→4→6→7, 3↔5).');
logLine('Press "Run LFP" to compute reachability from node 0, or edit the graph first.');
draw(null);

Result

Console

Notice that the iteration always terminates (the set can only grow, and the graph is finite). The number of rounds is at most |V|, so the whole process runs in polynomial time — matching the FO+LFP = PTIME theorem perfectly.

The Real Complexity

Here is the precise picture that descriptive complexity draws:

Fagin's theorem (1974) — proven: A class of finite structures is in NP if and only if it is definable by a sentence of second-order existential logic (SO∃). An SO∃ sentence looks like: ∃R φ(R), where R is a relation you're allowed to "guess" and φ is a first-order formula that checks whether R witnesses the property. Guessing a relation is exactly what a nondeterministic machine does in polynomial time.

Immerman–Vardi theorem (1987) — proven: On finite ordered structures (those with a built-in linear order on elements), a property is in PTIME if and only if it is expressible in FO+LFP — first-order logic augmented with a least-fixed-point operator. The ordering matters: without it, logical expressibility cannot pin down PTIME exactly (an open problem remains for unordered structures).

The logical hierarchy mirrors the complexity hierarchy:

Logic fragment	Complexity class
FO (first-order logic)	$AC^{0}$ (constant-depth circuits)
FO + LFP (ordered)	PTIME
SO∃	NP
SO (full second-order)	PH (polynomial hierarchy)

Why it matters for P vs NP: FO+LFP ≠ SO∃ is a precise logical statement equivalent to PTIME ≠ NP. So proving that reachability cannot be expressed without the LFP operator would prove P ≠ NP — showing how the logical and computational problems are the same question in different clothes.

The field also spawned finite model theory, which studies the expressive power of logical languages over finite structures, informing database query languages and verification.

Where It Matters

Descriptive complexity is not just a theoretical curiosity — it shapes how we think about what computers can efficiently describe and check:

Database query languages: SQL's core (relational algebra, first-order logic) corresponds exactly to $AC^{0}$ . Adding recursion — as in Datalog or SQL's $WITH RECURSIVE$ — bumps you into FO+LFP, capable of expressing reachability and therefore PTIME queries. The theorem tells you what you gain by adding recursion.
Model checking: verifying that a hardware or software system satisfies a temporal logic specification is a fixed-point computation. The connection to descriptive complexity explains both its power and its limits.
Circuit complexity: the logical hierarchy (FO ⊆ FO+LFP ⊆ SO∃) corresponds to the circuit complexity hierarchy ( $AC^{0}$ ⊆ P ⊆ NP), giving tools to prove circuit lower bounds.
Proof complexity and automated reasoning: understanding which properties require second-order quantification informs the design of SAT solvers and theorem provers — related to SAT.
Finite model theory: the broader field answers questions like "which graph properties can be expressed by a first-order sentence?" (answer: very few — connectivity cannot), with implications for graph databases and knowledge representation.

The result is a rare case where pure mathematical logic directly explains why certain database queries are harder than others, and why adding a RECURSIVE clause to a query changes its computational power fundamentally.

Conclusion

Descriptive complexity rewrites the question "how hard is this problem?" as "how complex a sentence do you need to express it?" The answer turns out to be the same — exactly.

Fagin's 1974 theorem (NP = SO∃) and the Immerman–Vardi theorem of 1987 (PTIME = FO+LFP) are cornerstones: they show that complexity classes have a logical identity, independent of any machine model. The gap between these two languages — between FO+LFP and SO∃ — is the same gap as between P and NP.

So the deepest open problem in computer science has a logical twin: can you prove that the least-fixed-point operator is not enough to define every NP property? No one has. And until someone does, P vs NP remains open — in the language of logic as much as in the language of algorithms.

Comments

Loading comments...

https://www.kipuhub.com/en/article/descriptive-complexity/Content licensed under CC BY-NC 4.0.

Cookies & privacy

When a formula in logic perfectly captures a complexity class