集合论 - note-math

对人来说, 一种理解自然数的方式是数数 (counting)

对计算机来说 (cf. logic.typ), 表示自然数的方式有

周期电路
算术元件
二进制
调用自身的函数

然而, 自然数集的元素数量是无限的, 而 bit 和计算机内存是有限的. 人类的记忆也是有限的

空间无限的问题: 现实无法构建空间无限的电路和内存. 即使能, 也受限于电流速度有限

但是可以使用潜在无限的时间来实现 "潜无限"

假设内存的上限无穷但每个周期的内存的占用都有限, 则程序有无限可能的输入, 这也是一种潜无限

然而, 甚至存在集合的元素数量不可数. Example

the set of all subset of ,
all function from to itself,

验证集合论语言的正确性需要 parser, 内存数据结构, 函数. 生成的计算机指令流的实现并不是这个目标范围的重点

集合/类型的动机

模块化和乘法分解以简化认知

Example 自然语言的主谓宾 SVO (subject, predicate, object). 假设有 10 个名词和 10 个动词. 假设我们 "忘记了 SVO 规则", 那么, 验证三个词的句子的语法正确性最多需要次. 如果理解并使用 SVO 规则, 最多需要次
如果集合的元素数量是无限的, 则集合/类型将概念有限化, 使得可以在有限时间内说出来

复杂的 set theory object (集合论对象), proposition (命题) 被储存在变量名里, 所以还是需要人类去检查所有存储在变量名里面的复杂定义, 所以可读性很重要

parser or 证明辅助程序能让人类从需要检阅所有步骤 reduce to 检阅定义 (以及检查编译器的逻辑代码), 跳过大量详细证明步骤, 就能确定证明结果的正确性. 这像 API 的情况

人脑编译器能省略和补充省略, 用容易出错和遗忘来换取临时效率

而且证明辅助还会有其它作用, 类似于, IDE/LSP/友好且互动的编译器错误信息/documentation 时代之前的编程是痛苦的, 数据和信息的组织和结构化和复用做得不好, 也没利用好计算机的强大记忆容量和时间

证明辅助的例子: acornprover, 还在开发中. 还没实现集合论 … 我的态度是, 即使可能暂时没有好的底层实现, 也可以转为寻求容易使用的语法和方便的附加工具 (e.g. LSP)

[proposition] proposition 是特殊的 (string, bool) product struct ((字符串, 真假值) 的逻辑乘积结构) 计算机数据结构. 对于数学语言, string field 使用特殊的构造规则来限制, 此 string 限制版本称为 formula (公式)

因为我们无法直接判断一个猜测的真假, 所以我们需要一种具有未定义真假值的语言

from 命题 to 未知命题的, 其真值部分被修改为 (bool, unknow) sum struct

Abbreviation true proposition 和 proposition 经常混用

很多命题是无法被计算机自动推导出来的, 需要人类去寻找可能的路径, 输入到计算机中进行验证, 或者开发更多新的自动化证明方法

我们将假设一些最开始的不需要证明的命题. 以及假设规则之使用现有命题构造新命题

Abbreviation 使用相同的符号 for formula and proposition, " is true/false/unknow",

[formula]

in (属于)

let symbol (符号) be type of math object, then is a formula

类似于 value : type or variable_name : type in programming language

symbol 不是 math object

equal (等于)

let be object, then is a formula

and, or, not (且, 或, 非)

let be formula, then

is formula

forall, exists (所有, 存在)

设是用构造的公式 i.e. 在内存中读取 , 使用特殊的函数调用, 则

is formula

inference (推导) , equivalent (等价) is formula

以下讨论 math-object-construct-rule (数学对象构造规则) alias set-theory (集合论)

[natural-number]

natrual number (自然数) and natrual number set (自然数集) is object. is true proposition

但是计算机无法处理无限. 为了让计算机能用有限的字符和内存去表示自然数集, 把和函数作为内存地址里的有限 symbol, 定义以下为 true proposition

等价于用指令流告诉计算机如何连续地 ? 也联系到归纳法

有限的字符的代价是潜在无限的时间, 总是借助了数数或者周期电路

[empty]

empty is object. let be a object, is false proposition

The definition of 方便用于 intersections e.g. 交集为空, 和有限集的的元素数量, 比方便

定义语言展开

由于 “定义语言展开” 很长, 因此通常 abbreviated to "definition" "def"

其实 symbol 通常也被用来表示定义语言展开或者规定语言转化. 具体自然数的可以直接定义为用计算机电路比较内存的值

[declare-element-of-set]

If is non empty (此信息来自的定义), we can define symbol and construct true proposition (let)

可以构造有限个 declare 语句

[enum] enumerate

is object then is a set

表示为内存里的数列

整个集合可以被这样调用: 记录第一个元素地址 + 数组长度作为电路周期数量, 每个电路周期读取一个元素

formulas are true propositions

特别地, 单元素集合

define

[equivalent]

等价的一些使用. 对有限的计算机数据来说, 可以穷举证明以下计算结果相等

类似地, 为了表示 "无限元素" 的情况, 定义语言展开或者规定语言转化. 例如无限元素的 De Morgan law

其中 "无限" 的概念有的限化是使用 declare-element-of-set 的符号串

formula, proposition 是内存里特殊的数据结构. 可以认为 math_object, formula, proposition 是编程语言的 type

许多命题是等价的, 于是可以考虑命题的 "quotient" 类型, 但等价可能性是无限的, 是否可能从存在穷举算法, 首先要看它是否 countable …

类似的冗余, set theory construction rules 也有可能有冗余, 或者说有很多等价的定义方式

规定 (有限的)

transitive :=

follow 有限情况的 bool 的各种规则, 定义语言转换规则: let is formula built with independent/parallel i.e. independent/parallel in memory read and used by specific cuntion, then

[commutative-forall-exists]

same for

[distributive-forall-exists]

注意, 我自己也觉得我无法完全清晰地处理下面的推导和证明的概念

推导的自然语言例子

如果下雨, 我不会出门
下雨了
所以我不会出门

这个例子类似于 conditional branch (条件分支)

let rain : bool;

let out : bool;

match (rain) {

  true => out = false,

  false => out = undefined,

};

let rain : bool;

let out : bool;

match (rain) {

  true => out = false,

  false => out = undefined,

};

[inference] 对于数学语言, 那就是

编译器读取到 formula
编译器读取到 formula is true proposition (可能来自定义)
编译器读取到 formula is true proposition
然后语言规则设置是, 编译器根据这种条件 (来自内存), 赋予 formula 的 bool 值为 true i.e. 设置 is true proposition

[proof] 证明就是编译通过 is true proposition

又一种等价

[reverse-inference] 反向推导. 如果结果是我出门了, 那么肯定不是下雨的结果. 如果条件分支的结果是 out = true, 这不是 rain = true 的结果. 由于理想二进制计算机的 bool 值必定二选一, 所以只能是 rain = false 的结果. 这可以被写为条件分支

match (out) {

  true => rain = false,

  false => rain = undefined,

};

match (out) {

  true => rain = false,

  false => rain = undefined,

};

数学上, 反向推导写为 formula , 并定义等价到

[reverse-proof] 反证明就是编译通过 is true proposition

演绎证明还需要三段论 (syllogism)

所有生物都会死
人是生物
所以所有人都会死

其中 "所有生物都会死" 是特殊构造的一种命题

[syllogism] 三段论推导是语言规则

编译器读取到 formula is true proposition (可能来自定义 e.g. union))
编译器读取到声明 let is true proposition
编译器读取到 formula
然后编译器根据这种条件 (来自内存) 设置 is true proposition

也即, 编译器根据声明 (可能 "无限") 来实现对数据的具体构造 (有限)

或者理解为, 这种规则和行为就是在定义这种概念本身

通常也被写为等价的规则 let , then 特殊的推导 formula is always true proposition. 这种形式通常被用于前面所说的 "证明就是编译通过 is true proposition"

反向三段论: let , then 等价的 formula is true proposition

我们可能永远不知道一个 bool unknow 的 proposition 是否能被构造性地证明, i.e. 有限步骤编译成功

target proposition 来自哪里? 可能是相关于现实世界的模型

证明需要展开大量句子, 尽管计算机处理 string 是非常快的. 无论如何, 性能优化? 仅在需要时使用 (lazy load)? 两个 proposition 不相互依赖时, 并行 (parallel)? 假设已经证明过的结果 (incremental compilation)?

A proposition has many proofs with different runtime data flow, 可以认为它们属于同一个 quotient proof of this proposition

以下的 object construction rules, 除了交集, 一般都给出 non-emtpy sets

let be set of sets

[union]

define object 和语言展开

is non-emtpy unless

我们不对定义 union. 下同. 理由是 let is always false proposition, 这使得很多东西不能用

enum is special case of sum/union?

[intersection]

[map] alias [function] [constant-dependent-product]

let is math object. 定义 map space , map as math object 的规则是

其中, 两个 symbol 组合成新的 symbol

denoted by

denoted by . in finite case, number of elements

的使用虽然看起来有问题, 但它们仍然在 symbol & symbol 串方面是可以定义的

如果谈到 map 具体代表什么, 由于非具体构造性, 没有一般编程语言那样的具体的 return, 或者 return 的是新定义的 symbol, math object, 语言展开

Prop

[subset]

denoted by . 根据 proposition-function 等价于 map space . in finite case, number of elements

没有元素的集合是任何一个集合的子集, 将这个规则加进子集的定义中. define be true proposition.

map space 和 subset 引入了高级别的无限

一件初看反直觉的事情是, 我们似乎知道所有或所有 , 却无法数出来 cardinal-increase uncountable. 但是, "知道所有 " 究竟是什么意思? 事实上, 试着考虑 "一般方式之找一个的无限子集" 这一个问题, 就会发现这不是简单的

类似地, 虽然可数已经可以定义一些实数 e.g. , 但如果不借助 subset or map, 可数地构造无法得到全部

[proposition-function]

let , is already constructed

is object

[product]

let be set of sets, let

is non-emtpy unless (related to [axiom-of-choice] )

Abbreviation . in finite case, number of elements

[pair] alias [constant-dependent-sum]

consant-dependent-product . consant-dependent-sum is

[sum]

let be set of sets, let

is non-emtpy unless

in finite case, number of element

[coordinate-component]

product component

or
sum component

define

的其它用法

内存里的 identifier 的别名
内存里的函数返回值. so 应该理解为 add function 的返回值是

[compare-math-lang-with-programming-lang]

数学语言中的 ∈ 和编程语言中的 : 之间的区别是什么?

数学语言与编程语言非常相似, 都需要编译器检查一系列语言规则

一些区别:

一般应用编程语言已经使用了递归, 但数学语言将递归指令本身视为类型. 或者将递归指令称为自然数的递归定义, 或生成自然数的指令. 这使得我们可以讨论一般的自然数, 而无需生成具体的自然数 (由计算机或人脑的周期性电路生成)
主流的通用编程语言 (没有自然数集和依赖类型) 仅使用有限次 and, or 来生成新类型, 例如 struct, enum. 这依赖的是计算机能够表示特定数量的自然数. 另一方面, 数学语言有无限版本的 and, or 来生成新的类型 (或集合), 例如 forall, exists，它们不像有限次的 and, or 那样表示. 而且 "无限" 甚至可以超越可数的自然数

在底层，数学语言或编程语言都可以用周期电路, 内存位和逻辑门来表示

数学语言从自然数 (以及命题演算和集合论规则) 开始. 例如, 实数是基于自然数定义的. 然而, 它仍然需要 "变量" 的概念, 例如 let a in A 中的 a

通用编程语言从内置类型开始. 从概念, 认知, 应用的角度来看, 最好将它们视为原始概念或计算机内存中的位的结构, 而不是使用数学上的自然数来构造它们

[hierarchy-order-of-set]

以上构造的 set 称为 zero (hierarchy) order set

then let be math object, in first order set

再次使用 object construction rules, 得到的东西也定义为属于

无论如何我们总是可以在编译器中构造这种带有类型和 bool 和各种规则的语言

let be math object, . 诸如此类 …

Example

可以被分成多句, 使得可以方便的加入/移除 property, 来得到不同的 struct

看起来像自然数集 , 所以应该再假设新的 hierarchy 吗? 然后对 , 继续使用 object construct rule … 虽然确实可以抽象地定义以及后续的东西, 但是, 具体自然数的是需要的, 且也需要无限的集合阶层, 递归下降意义下的潜无限的输入 (可能的定义需要作为输入的一部分), 但递归下降的语言规则是有限的

通常我们不需要显式 hierarchy of set, 例如, 我们只需要构造这样的具体类型, 但不需要提到类型作为元素属于类型

语言是潜无穷的, hierarchy-order-of-set 语言也是如此. 当然绝大多数编程语言都是潜无穷的

这种 hierarchy 之外是否可能存在很多不是线序 or 全序的东西?

似乎有两种 math object

已经用有限步构造出来的 math object. 它代表以一些规则所构造的类型
直接假设的 math object 类型或者抽象的 type, 内存中的类型及其变量作为一种 placeholder (占位符). 在编程中, 这种概念叫做 generics (泛型). 它代表抽象符号之间的类型关系. 有时需要 generics 的 instantiation (实例化) or monomorphization (单态化) 之后才能通过编译

type 之间的同态的使用可以对证明带来方便. 有时可以让计算从特殊情况推出一般情况的证明, 如果特殊情况的证明没有用到特殊情况的专有性质, 则实际上是隐藏的对一般情况的证明

[universal-type]

universal-type 的问题, 或者 type of every type 的问题

这里的容易忽略的一点是, "type of every type" 中的 "type" 指的是什么? 所谓的 "type" 是什么意思? 某种二元变量 bool 函数 or 二元谓词逻辑命题?

从构造性的角度, 需要语言规则去定义一种 "type". 但是, 为了定义 "type of every type", 需要知道所有的构造 "type" 的语言规则. 即使我们知道逻辑门, 周期电路, 内存, 我们也真正不知道所有语言规则或程序, 除非真的写出来 …

即使不考虑 "type of every type", 也能有自指问题. 在数学语言的递归下降构造规则中, math_object type 并不参与在构造规则中. 如果一个类型 T 自指地参与到构造规则中, 则这种语言或程序是非终结的, 例如 T : T, 即使每个周期使用的内存有限, 也无法在有限时间内运行完程序. 注意, 一般的编程语言可以有无限循环 (由不同的原因)

假设程序定义了一种 universal-type 的概念, 且 universal-type 又可以用来构造 "type", 则 universal-type 就自指地参与到了 "type" 的构造规则中, 导致非终结语言或程序

Example [Russell-paradox]

使用 set theory rules 定义

然后让编译器去计算命题的 bool, 由于 = true, 编译器只计算的 bool, 然后发现 not 函数, 所以计算 not 里面的 bool, 但这又回到了计算的 bool, 编译器可能选择进入电路死循环

对于有限集, , 或者无法判断 , e.g. , 因为 , 或者没有定义这个命题是 true proposition

如果考虑集合 hierarchy, 对于很可能从而因为第一个条件不满足

Example [self-referential-paradox] 自指悖论. "这个句子是错的"

this_sentence_is_false : bool = false;

loop:

  match (this_sentence_is_false) {

    false => this_sentence_is_false = true,

    true => this_sentence_is_false = false,

  goto loop

};

this_sentence_is_false : bool = false;

loop:

  match (this_sentence_is_false) {

    false => this_sentence_is_false = true,

    true => this_sentence_is_false = false,

  goto loop

};

或者用分层绕过自指悖论 (this_sentence = false) = true. 认为它们是不同的句子和判断, 认为它并不能自指

[dependent-distributive]

let be set of sets, let , and let be set of sets, index by its elements

union & intersection

sum & product

draft of proof: 展开, 使用 parallel distributive cf. distributive-forall-exists

[set-minus]

. if then define

[symmetric-set-minus]