使用TypeScript证明哥德尔第二不完备定理

介绍

在上一篇文章中，我们探讨了哥德尔第一不完备定理，并使用TypeScript创建了一个简化模型来证明任何足够强大且一致的形式系统都会包含无法在系统内证明的真实陈述。

定义

哥德尔第二不完备定理指出：任何能够表达基本算术的形式系统都无法证明自身的一致性。

回顾

让我们快速回顾第一篇文章中的关键组件：

Statement：表示逻辑陈述的TypeScript函数。如果可证明则返回true或false结果
isProvable：检查陈述是否在系统内可证明的函数
formalSystem：存储陈述的Map，以哥德尔数作为键

我们将使用这些相同的构建块来证明第二定理

Modus Ponens解释

Modus ponens是一个基本的推理规则，允许我们从条件陈述中得出有效结论。它的工作原理如下：

我们知道：A → B（如果A，则B）我们观察到：A = true

那么我们可以逻辑推断：B = true

例如：

规则：“如果下雨，地面就会湿”（R → W）观察：“正在下雨”（R = true）结论：“地面是湿的”（W = true）

在TypeScript中，我们可以这样实现Modus Ponens：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


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

实现一致性检查

一致的系统没有矛盾，例如同一个陈述不能同时为真和假。 isConsistent函数评估形式系统是否逻辑一致。Statement或其否定必须为假。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


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

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

自指一致性陈述

这个函数创建一个Statement，断言：形式系统是一致的。

1
2
3
4
5


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

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

证明

让我们将这个自指陈述添加到形式系统本身。注意我们拥有所有一致的Statement。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


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
);

那么selfConsistencyStatement在这种情况下会输出什么？如果我们使用Modus ponens规则并假设：selfConsistencyStatement() === true，这将满足我们的isConsistent约束，要求所有Statement返回布尔值以认为给定系统一致。

但当selfConsistencyStatement() === false时，同样的逻辑也适用。这将使isConsistent() === false，从而使我们的自指陈述在逻辑上正确。当一个系统的Statement可以被证明既真又假时，它就是不一致的。

现在我们已经证明selfConsistencyStatement只能以一种方式表述，这使得它使用我们的系统规则既真又假。我们已经证明任何包含基本算术能力的形式系统都无法从内部证明其一致性，从而展示了哥德尔第二不完备定理的实际应用。