03 一阶逻辑：完备性

title: 一阶逻辑的完备性 date: 2024-09-01 14:37:00 categories: 数理逻辑 mathjax: true katex: enable: true allpost: true copy_tex: true description: 通过一阶逻辑语言我们能够形式化数学定理，现在我们想要形式化“证明”的概…

04 一阶逻辑：表达能力

title: 一阶逻辑的表达能力 date: 2024-09-13 02:40:00 categories: 数理逻辑 mathjax: true katex: enable: true allpost: true copy_tex: true description: 一阶逻辑的表达能力

随机向量

随机向量(Random Vectors)

Model Checking

模型检验(model checking)是用于验证软件和硬件的正确性的一种方法。所谓正确性，就是软件或硬件是否正确实现了我们所希望它所具有的功能。

Schröder-Bernstein Theorem

Schröder-Bernstein's Theorem

Transformer

下面我们讨论大语言模型用于预测next token的Transformer架构。Transformer架构有三个基本组件：token的embedding(嵌入)，Attention(注意力机制)， MLP(多层感知机)。我们将深入讨论如何让大模型利用纯粹的数学机制来理解词语、结合上下文、掌握知识。

Currying

2025 徐志摩 - 再别康桥

再别康桥

Church Numerals

图灵证明了图灵机可计算的函数等价于由-calculus定义的可计算函数。下面我们就来看如何由-calculus定义可计算函数。

2 线性空间

线性方程组的两个几何视角