How to prove Gödel’s First Incompleteness Theorem using Typescript

The more one learns, the more they realize they don't know. In 1931, a young mathematician named Kurt Gödel proved this feeling is a fundamental feature of the universe of logic itself.

The First Incompleteness Theorem reveals a fundamental limit of logic. It indicates that any formal system of rules, provided it's consistent and complex enough for basic arithmetic, cannot be complete. As Gödel proved, such a system will always contain statements that are true but can never be proven by the system's own rules.

We see numerous examples of such systems, e.g., mathematics, any computer program or anything digital in general is such Gödel's formal system. Any digital artifact can be reduced to a natural number (01011100...) making it a valid formal system.

In this article, we’ll explore how to simulate this concept using TypeScript. This language fulfills all theorem requirements: it is capable of general-purpose computation and non-contradictory. While the full proof requires deep mathematical machinery, we’ll create a simplified model to explain Prof. Gödel's way of thinking.

Define a statement

First, we want to define the basic building blocks of our formal system. Gödel's proof started with basic operators assigned unique numbers, the same approach as tokenization during the Retrieval-Augmented Generation (RAG) process. Then he compiled basic axioms using these tokens, then more complex formulas and so on. Each of them is expected to have their own unique Gödel's number.

In our system we will operate with more complex Statements which are Typescript variadic functions accepting numbers as parameters. The original approach would require using something like Abstract Syntax tree parsing.

type Statement = (...params: Array<number>) => (boolean | unknown)

For brevity's sake, we'll take the derivation and combination of these statements out of the picture and assign these numbers using just a string hash of the statement function. Though, this problem is also Turing complete and can be resolved algorithmically.

const getGoedelNumber = (statement: Statement) => {
  return getStringHash(`${statement}`);
};

Each statement in our system can return a Boolean value or something else.

Build a formal system

First, we define basic logical properties that define equivalence relations and operations.

STATEMENTS: Array<Statement> = [
  // Reflexive
  A => A === A,
  // Symmetric
  (A, B) => A === B && B === A,
  // Transitive
  (A, B, C) => (A === B && B === C) && A === C,
  // Additive
  (A, B, C, D) => (A === B && C === D) && A + C === B + D,
  // Multiplicative
  (A, B, C, D) => (A === B && C === D) && A * C === B * D,
];

The operation of converting Gödel numbers to statements should also be possible in our system. We are going to use ECMAScript Map to achieve this.

const formalSystem = new Map(
  STATEMENTS.map(statement => [getGoedelNumber(statement), statement])
);

Check provability

Each statement in our system is considered provable when it returns a Boolean value (basically something we can agree or disagree with) or something else, which indicates it's not provable.

const isProvable = (goedelNumber: number) => {
  return (
    typeof formalSystem.get(goedelNumber)(...VARIADIC_NUMBER_ARRAY) ===
    'boolean'
  );
};

Here is the code to check provability of our system.

formalSystem.forEach(statement => {
  const goedelNumber = getGoedelNumber(statement);
  if (isProvable(goedelNumber)) {
    console.log('Provable', `${statement}`);
  } else if (!isProvable(goedelNumber)) {
    console.log('Non provable', `${statement}`);
  }
});

Create unprovable statement

To prove this theorem, Gödel complied a true statement using these rules, which cannot be proven or disproven in this system at the same time. Here is how we do this.

We will write a statement which attempts to assert that it is not provable. If the system proves it, then it must be false (a contradiction). If it does not prove it, then it is true but unprovable. Due to the lack of diagonal-lemma package in NPM, we have to use recursion.

const unprovableStatement = () => {
  return isProvable(getGoedelNumber(unprovableStatement)) === false;
};

formalSystem.set(getGoedelNumber(unprovableStatement), unprovableStatement);

try {
  console.log(isProvable(getGoedelNumber(unprovableStatement)));
} catch (error) {
  console.info(
    error.message,
    "Formal system couldn't decide if it's provable.",
    `${unprovableStatement}`
  );
}

The existence of such statements reveals a fundamental limitation on formal systems: the fact that there are mathematical and development truths beyond our capacity to fully capture through logical deduction alone.

Dima Vyshniakov @morewings