现在我们知道所有物理定律都是数学方程，反之亦然
这意味着物理学是基于数学的
现在的问题是“是所有数学方程都被视为逻辑论证/公式，还是所有逻辑论证/公式都被视为数学？”
即哪一个是基于另一个的？
========================================================
说物理学以数学为基础是一种误导。
物理定律并不是数学定理。例如，它们并不是由 ZFC 公理推导出来的。相反，我们发现物理事物的行为可以用数学来描述。
以 F = MA 为例（我知道牛顿已经被取代，但它仍然有效）
这不是数学真理。它不可能是，因为 "F"、"M "和 "A "只是变量，与某种固定的解释无关，可以取任何值。作为一个（近似的）物理事实，如果你把一个运动物体的加速度增加一倍（而不改变它的质量），那么这个物体所受的力也会增加一倍
好吧。有一个哲学项目试图证明数学在某种意义上可以还原为逻辑，这被称为逻辑主义。但是，我认为许多哲学家和数学家都认为数学依赖于具体的数学公理，因此不能还原为逻辑。
========================================================
罗素和怀特海在《数学原理》中试图证明数学可以简化为逻辑。我认为共识是它并没有完全发挥作用。
在《算术基础》中，弗雷格试图证明数学如何还原为逻辑，这种立场被称为逻辑主义。为此，他基本上用严格的逻辑术语定义了数学的基本构建模块，例如 0、1 和大于 1 的数字。
就像哲学中的任何流派或思想一样，有人赞同它，也有人不赞同。但我确实认为可以公平地说，无论哪种方式，逻辑通常被认为比数学更基础。
我当然从未听说过有人主张逻辑可以简化为数学。
========================================================
库里-霍华德对应关系很简洁，因为它表明计算机编程的逻辑在某种意义上等同于更“传统”的逻辑形式。非正式地说，它在证明和程序之间以及命题和类型之间建立了对应关系。Curry-Howard 对应的广义形式能够通过依赖类型处理量化逻辑。
这种对应关系已应用于设计 Coq 和 Lean 等证明辅助工具，这些工具基本上是编程语言和逻辑系统的合二为一，并且越来越多地用于检查和形式化数学证明。
兰贝克-库里-霍华德版本添加了范畴论。我对此知之甚少，我不确定它有多深，但大致上它将某些类别中的对象与逻辑命题/类型以及态射与证明/程序相关联
我不知道这是否意味着逻辑可以“简化”为数学，但它确实表明很难将两者整齐地分开
========================================================
作者：lambek-curry-howard——数学证明是程序，程序是同构的数学证明。
图灵计算机的停机问题与逻辑中的哥德尔不完备性直接相关。该死的几乎同样的事情。
Lambda 演算和图灵机也有直接关系。
尽管它有点错误，但我建议您研究一下乔姆斯基层次结构以了解这个概念。它说明了图灵计算机在计算语言方面有多么强大。除此之外没有什么，它是洋葱的最外层外壳，即乔姆斯基层次结构。
========================================================
在计算机科学中，流行使用关系逻辑，而不是谓词逻辑。但事实上，几乎是一样的，我们只有两种量词“any”或“exist”