最近又有特别多的东西进入脑子...

类型论、集合论、范畴论、类、宇宙、经典逻辑、直觉主义逻辑、算术系统、哥德尔定理、ZFC???他们是怎样的关系...

现代结构数学建立在集合论上，那建立在其他理论上的可行性？不同数学基础之所以能作为同一地位（并不一定同一效力）的对象并列存在，其必有结构上的因素，我们可以问：何种理论可以成为数学基础？可能的数学基础理论可以完全分类吗？浅浅瞎猜这就是哲学、认知等东西的终极问题。

一些尝试梳理：

类型论要求每个obj都有Type，我们可以在类型论的基础下实现弱一点的集合论，即元素是Type α的 这样的集合们构成一个Type ，Set α

可以猜想类型论和集合论是互不包含的基础理论，是对对象与行为的终极认识与理解的理论。

下面浅浅回答一下：何种理论能成为数学基础

The vocabulary of sets, relations, and functions provides a uniform language for carrying out constructions in all the branches of mathematics. Since functions and relations can be defined in terms of sets, axiomatic set theory can be used as a foundation for mathematics.

——《Mathematics in Lean》Chapter 4

集合、关系、函数能被集合实现，所以集合论可以做数学基础。

对象、函数能被类型实现，所以类型论可以做数学基础？（类型论如何刻画静态关系？）

事实上集合、关系、函数

分别对应程序中的数据、数据结构、算法，

又对应大白话中的东西，东西的关系，东西怎么动。

一个review：

我在集合论下学习结构数学归纳出的第三种数学思想是：对象特例化。

我们总认为一个对象a，存在集合A，a∈A。一般还可以要求A-{a}非空。这就代表每个对象总能被抽象，总能放入一个大背景中，多数情况下它都有并列的对象，地位相同，因此没有绝对特殊的对象。由此我养成了极端的结构化和抽象化的看问题的眼光。

现在我们在类型论下重看这个思想：

一个对象a，按定义存在类型a：A，这也代表每个对象总能被抽象，总能放入一个大背景中，没有绝对特殊的对象。

可见抽象，abstraction，（作为动作）是基础理论必须要面临的问题，必须要有的能力。而集合论和类型论贯彻了同一哲学，抽象是无止境的。但是集合论的某些悖论告诉我们：似乎某些情况下集合论的抽象能力会受到限制。

我目前的感受，文初提到的对象之间的关系应该是：

1经典逻辑、直觉逻辑→2集合论、类型论、范畴论→3算术系统、数学

一个令人印象深刻的点是：我们可以分别以集合论、类型论、范畴论为基础构造自然数。他们都陷入了哥德尔定理（bushi）

至于ZFC是什么啊...不会

————————————————1.18下午上课梳理—————————————————

  语言学

          生成语言学中的Hopf代数模型

          计算语言学与代数几何————《语言学领域有哪些令人毛骨悚然的理论》

  命题逻辑  → 一阶逻辑=一阶谓词逻辑  →  高阶逻辑=高阶谓词逻辑=广义谓词逻辑

        命题逻辑中有经典的Stone对偶

        命题逻辑↔Boolean代数 ~ Stone空间，是某种拓扑空间

            我就不明白了，拓扑空间不就是三条bool公理？

            凭什么这三条公理这么特殊，能和命题逻辑这种根本的东西形成对偶？

             Lindenbaum代数是命题理论的本质的代数不变量，草草草。

                  ————《拓扑学（点集）和逻辑学有什么联系相同的地方吗？》

            让我们考察拓扑空间上所有重要的构造，

            紧致连通分离可数的点拓性质，同伦群同调群，光滑函数层，

            胞腔，euler数：考察各种定义，betti数，

            到底哪些强依赖于拓扑空间3公理了？

    一阶谓词逻辑中，量词只能用于个体变元，∀ x, 不容许量化谓词。

    高阶谓词逻辑中取消了这一限制，允许∀ 用于命题变元和谓词变元，

    高阶逻辑更有表现力，但对一些情形应用不好。作为哥德尔的结论：

    经典高阶逻辑不允许（递归的公理化的）可靠的和完备的证明演算。Henkin模型修补

    “一阶逻辑是最适合数学的逻辑”

  数理逻辑的四个分支：

  ·集合论——————类型论 范畴论 数学基础问题，可认知对象的分类

      同伦类型论？直觉类型论？

        ZFC 是集合论的一种公理化方式

        peano公理是集合论体系下构造自然数的方式

        三个体系下都可以构造自然数。

        集合论与一阶逻辑的对偶？————实变函数中对命题的集合论式改写。

          这个对偶没有找到严肃的材料，如果为真，则从某角度说明了集合论的自然性，否则我很可能会认为容许任意抽象的类型论更自然。

        Grothendieck宇宙？拓扑斯？

        Russell悖论？

  ·递归论——————主要与计算理论相关  

      λ演算  

            是一个形式系统

            是最小的通用程序设计语言，美美（Z，+）之于Abel群。

            无类型λ演算————只有一种类型。

            有类型λ演算

      可计算性？

      P=NP？

      Curry-Howard同构？ 简单类型和λ演算之间是双射

      编程 元编程 元语言 乔姆斯基来喽

      邱奇 图灵？

  ·证明论———————数学证明的问题

    本质上是语法逻辑

  ·模型论————————形式系统与数学模型的关系

    本质上是语义逻辑

    代数几何与模型论

    命题演算的一个具体模型就是逻辑代数

    谓词演算的模型是？

    高阶逻辑的模型是？

    证明和谓词演算是什么关系？

    力迫法：构造公理系统的模型的一种方法。在集合论的模型中尤其强大？用于证明连续统猜想的独立性

           见：《数学中有哪些明明是暴力破解还给人美感的证明？》费事发财

                1波兰空间上独立集定理

                2无理旋转图不存在可测颜色

                3不存在重排不变的康托对角线borel函数

                4不存在从Viali等价关系到相等关系的borel归约

-/