构造性元逻辑下停机问题不可判定性抽象化的证明问询

咱们先设定一个包含自然数、布尔值、列表、不交并和集合的构造性元逻辑环境，接下来用它来对图灵机进行推理——我们可以定义以下元逻辑层面的函数与集合：

• TMData：代表所有有限布尔序列构成的集合，形式化定义如下：

  TMData : Set == Seq(Bool)
  

• TMEval：这是图灵机的「大步操作语义」函数，它接收一个图灵机算法alg和输入input，如果算法发散就返回"null"，否则返回计算结果，定义如下：

  TMEval(alg: TMData, input: TMData) : TMData + "null"
  

接下来我们可以定义一个元逻辑谓词，用来描述“某个图灵机是否具备解决停机问题的能力”：

SolvesHalting(halt_solver: TMData) == 
               ∀inp_alg: TMData, TMEval(halt_solver, inp_alg) = (TMEval(inp_alg,[]) = "null" ? [0] : [1])

简单来说，这个谓词的核心意思是：对于任意一个图灵机算法inp_alg，停机判定器halt_solver能精准返回结果——当inp_alg在空输入下发散时返回[0]，停机时返回[1]。

最后是我们要证明的元逻辑定理：

THEOREM HaltingUnsolvable == ∀ alg: TMData : ¬ SolvesHalting(alg)

也就是不存在任何能解决停机问题的图灵机算法，这个定理是可以在我们设定的构造性元逻辑框架内完成证明的。

备注：内容来源于stack exchange，提问作者Suraaj K S