说一下哥德尔第一不完备定理的个人理解，非主流意见。

Smullyan把哥德尔第一不完备定理解释成，把算术系统和递归函数换成（哥德尔定理之后出现的）能完备表达全部可计算函数（图灵完备）的λ或者组合子就行了，本质上一样。

Smullyan当然很权威。但是这个解释把规则系统的不完备reduce到了计算系统的不停机，这是一个大跌眼镜的事情。因为，至少我们还知道有例如Harrop Rule这样的规则，在简单如直觉命题演算这样基础的逻辑系统中存在，它是可容不可导的。如果采用现代证明论语义，把可容性定义为模型语义，直觉命题演算逻辑就不完备了。

----

Smullyan的问题在于他没有死磕Prov是什么。

第一个可能是Prov可能被定义成语法上的逻辑连接符。这是unusual的，但是对于证明论角度这完全合法，如果元语言的「和」可以内化成目标语言的∧，那⊢也没什么不可以的，虽然这会制造混乱。

虽然Smullyan没有明确这么说，但是他的说法可以这样去理解，因为据gemini说根据Lob定理可以很容易构造出一个和柯里悖论高度类似的结果把整个系统trivialize的。于是这样看的话我们必须从两个观点中选一个：

1 哥德尔的证明使用了未能良定义的逻辑常量，所以这个证明无法接受
2 哥德尔的证明里的Prov是良定义的，系统trivial

不管接受哪一个都低估了这个证明的意义。视哥德尔的构造过程为（异常复杂和巧妙的）动用了不动点，得到了和柯里悖论没分别的结果，不奇怪。

----

Alternatively，我们放弃把Prov理解为逻辑常数，转而把它看作证明论意义上的model，如果觉得model这个词不太好，改为semantic也可以，就是Schroeder Heister主张的那种证明论语义。因为这种语义是研究规则系统的结构的，on its own merits，不用象模型论那样拖进来其它的数学对象，尤其是可能拖入不兼容的数学基础。

在这个意义上，自然数是哥德尔talk语义用的domain of discourse。Prov就成了这个domain上的数学对象，逃掉了要给出其在规则系统里的内化定义的要求。

那么基于这个理解，哥德尔的叹为观止的构造技术，在规则和模型之间一层一层，来来回回，最终来到了拷问大抱丝的终极问题，这句话本身可不可证？

----

在自然语言里「这」是指代，也因此被称为自指。在直觉里自指就像把一根绳子的两头tie在一起。但是可以这样做吗？他们两个是同一个东西吗？还是同一个名字的不同版本？但是试图回答这个问题本身，就是哲学家的方法，不是数学家的。

数学家的回答是你可以tie在一起，也可以不。你得到两个不同的拓扑。值得问的问题是，那个空间更有用呢？

----

哥德尔的直觉是它不认为自指是一个问题，他的柏拉图主义数学观让他选择了后者，即相信：一个数学系统要么是如此rich，它甚至能够模拟自己的行为，但是有个小小的遗憾是它不完备；要么它是如此的poor，以至于做不出什么真正有价值的结果。

----

对猴摸头皮类型论有了解的朋友，可能立刻就行想起Univalence公理。是的，就是这么回事。选择决定命运，选择决定理论。两个不同的拓扑。