Intro

In our previous article, we explored Gödel's First Incompleteness Theorem and created a simplified model in TypeScript to demonstrate that any sufficiently powerful and consistent formal system will contain true statements that cannot be proven within it.

Definition

Gödel's Second Incompleteness Theorem states that for any formal system that can express basic arithmetic, cannot prove its consistency.

Recap

Let's quickly refresh the key components from the first article:

• Statement: A TypeScript function representing a logical statement. Returns true or false result in case it's provable.

• isProvable: A function that checks if a statement is provable within our system.

• formalSystem: A Map that stores our statements, with their Gödel numbers as keys.

We'll be using these same building blocks to prove the second theorem

Modus ponens explanation

Modus ponens is a fundamental rule of inference that allows us to draw valid conclusions from conditional statements. It works like this:

• We know: A → B (If A, then B)
• We observe: A = true
• Then we can logically conclude: B = true

For example:

• Rule: “If it's raining, then the ground is wet” (R → W).
• Observation: “It's raining” (R = true). Conclusion: “The ground is wet” (W = true).

In TypeScript, we can implement Modus Ponens like this:

const modusPonens = (
  rule: (observation: boolean) => boolean,
  observation: () => boolean, 
) => {
  if (observation()) {
    return rule(observation());
  } else {
    return false;
  }
};

Implement consistency

Consistent system is free from contradictions, such as when the same statement can be true and false at the same time.

isConsistent function evaluates whether a formal system is logically consistent. Either Statement or its negation has to be false.

import {ABSTRACT_NUMBER_ARRAY} from './utils.js';

const isConsistent = system => {
  return system
    .values()
    .every(
      statement =>
        statement(ABSTRACT_NUMBER_ARRAY) !== 
        !statement(ABSTRACT_NUMBER_ARRAY)
    );
};

Self-referential consistency statement

This function creates a Statement that asserts: the formal system is consistent.

import {formalSystem} from './first.js';

const selfConsistencyStatement = () => {
  return isConsistent(formalSystem) === true;
};

Proof

Let's add this self-referential statement to the formal system itself. Note that we have all consistent Statements.

import {formalSystem, getGoedelNumber} from './first.js';
import {ABSTRACT_NUMBER_ARRAY} from './utils.js';

formalSystem.values().every(
  statement => statement(ABSTRACT_NUMBER_ARRAY)
); // => true

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

So what would be the output of selfConsistencyStatement in such a case? If we use Modus ponens rules and assume the following: selfConsistencyStatement() === true, that would satisfy our isConsistent constraint, requiring all Statements to return boolean to consider the given system consistent.

But the same logic would be applicable when selfConsistencyStatement() === false. This would make isConsistent() === false, thus making our self-referential statement logically correct. When a system has Statements which can be proven both true and false it's inconsistent.

Now we've proven that selfConsistencyStatement can be formulated in only one way, which makes it both true and false using our system rules. We've shown that any formal system containing basic arithmetic capabilities cannot prove its consistency from within, demonstrating Gödel's Second Incompleteness Theorem in action.