note-math

For people, one way to understand natural numbers is counting

For computers (cf. #link(<logic.typ>)[]), the ways to represent natural numbers are

Periodic circuit
Arithmetic component $+ 1$
Binary

However, the number of elements in the set of natural numbers is infinite, while bits and computer memory are finite. Human memory is also finite

The problem of infinite space: Reality cannot build circuits and memory with infinite space. Even if it could, it would be limited by the finite speed of electricity.

But potentially infinite time can be used to achieve "potential infinity"

However, there are even sets with an #link(<uncountable>)[uncountable] number of elements. Example

the set of all subset of $ℕ$ , $Subset (ℕ)$
all function from $ℕ$ to itself, $ℕ \to ℕ$

Verifying the correctness of set theory language requires a parser, memory data structures, and functions. The implementation of the generated computer instruction stream is not the focus of this goal.

Motivation for sets/types

Modularization and multiplicative decomposition to simplify cognition

Example Natural language's Subject-Verb-Object SVO (subject, predicate, object). Suppose there are 10 nouns and 10 verbs. Suppose we "forget the SVO rule", then verifying the grammatical correctness of a three-word sentence requires at most $10^{3} = 1000$ times. If we understand and use the SVO rule, it requires at most $2^{3} = 8$ times.
If the number of elements in a set is infinite, then the set/type limits the concept, making it possible to say it in a finite amount of time

Complex set theory objects, propositions are stored in variable names, so humans still need to check all the complex definitions stored in variable names, so readability is very important

Parser or proof assistants can allow humans to reduce from reviewing all steps to reviewing definitions, skipping a large number of detailed proof steps, and then determine the correctness of the proof result. This is like the case of APIs

The human brain compiler can omit and supplement omissions, trading temporary efficiency for error-proneness and forgetfulness

Assistance also has other functions, like the case of, Programming before the era of IDE/LSP/friendly-and -interactive-compiler-error-messages/documentation was painful. The organization, structuring and reuse of data and information were not done well, and the powerful capacity and time of memory were not used well.

proposition_(tag) proposition is a special (string, bool) product struct computer data structure. For mathematical language, the string field uses special construction rules to restrict it, and this restricted version of the string is called a formula

Because we cannot directly judge the truth or falsehood of a guess, we need a language with undefined truth values.

from proposition to unknown proposition, its truth value part is modified to (bool, unknow) sum struct

Abbreviation true proposition and proposition are often used interchangeably

Many propositions cannot be automatically derived by computers, and humans need to find possible paths, input them into the computer for verification, or develop more new automated proof methods.

We will assume some initial propositions that do not need to be proven. And assume rules for constructing new propositions using existing propositions.

Abbreviation Use the same symbol $ϕ$ for formula and proposition, " $ϕ$ is true/false/unknow", $ϕ = 0 / 1 / ?$

formula_(tag)

let symbol $𝑎, 𝐴$ be type of math object, then $𝑎 \in 𝐴$ is a formula

$𝑎 \in 𝐴$ is similar to value : type or variable_name : type in programming language

symbol $\in$ is not math object

equal

let

𝑎, 𝑏

be object, then

𝑎 = 𝑏

is a formula

and, or, not

let $𝑝, 𝑞$ be formula, then

\begin{matrix} 𝑝 \land 𝑞 \\ 𝑝 \lor 𝑞 \\ \neg 𝑞 \end{matrix}

is formula

forall, exists

let $𝑝 (𝑎)$ be formula built with $𝑎$ i.e. read $𝑎 \in 𝐴$ in memory, used by some specific function call, then

\begin{matrix} \underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎) or \forall 𝑎 \in 𝐴, 𝑝 (𝑎) \\ \underset{𝑎 \in 𝐴}{⋁} 𝑝 (𝑎) or \exists 𝑎 \in 𝐴, 𝑝 (𝑎) \end{matrix}

is formula

inference $𝑝 \Rightarrow 𝑞$ , equivalent $𝑝 \Leftrightarrow 𝑞$ is formula

The following discusses math-object-construct-rule alias set-theory

natural-number_(tag) $ℕ$

natrual number $0, 1, 2, \dots$ and natrual number set $ℕ$ is object. $0, 1, 2, \dots \in ℕ$ is true proposition

But computers cannot handle infinity. In order to allow computers to use limited characters and memory to represent natural numbers, let $𝑛, ℕ$ and $+ 1$ functions be finite symbols in the memory address, and define the following as true proposition

$0 \in ℕ$
$𝑛 \in ℕ ⟹ 𝑛 + 1 \in ℕ$

Equivalent to telling the computer how to continuously $+ 1$ with instruction streams? Also related to induction

The cost of finite characters is potentially infinite time, always relying on counting or periodic circuits.

empty_(tag) $\emptyset$

empty $\emptyset$ is object. let $𝑎$ be a object, $𝑎 \in \emptyset$ is false proposition

The definition of $\emptyset$ is convenient for intersections $\cap$ e.g. the intersection is empty, and the number of elements of $Subset (𝐴)$ of a finite set $𝐴$ , $2^{𝑛}$ is more convenient than $2^{𝑛} - 1$

Define language expansion

$𝑎 \neq 𝑏 ≔ \neg (𝑎 = 𝑏)$
$𝑎 \notin 𝐴 ≔ \neg (𝑎 \in 𝐴)$

Because “define language expansion” is very long, it is usually abbreviated to "definition" "def"

In fact, the symbol $=$ is also commonly used to represent defining language expansion or specifying language transformation. Specifically, the $=$ of natural numbers can be directly defined as comparing the value of memory with computer circuits.

declare-element-of-set_(tag)

If $𝐴$ is non empty $𝐴 \neq \emptyset$ (this information comes from the definition of $𝐴$ ), we can define symbol $𝑎$ and construct true proposition (let) $𝑎 \in 𝐴$

A finite number of declare statements can be constructed

enum_(tag) enumerate

$𝑎_{0}, \dots, 𝑎_{𝑛}$ is object then ${𝑎_{0}, \dots, 𝑎_{𝑛}}$ is a set

Represented as a sequence of numbers in memory

The entire set can be called in this way: record the address of the first element + the length of the array as the number of circuit cycles, and read one element per circuit cycle

formulas $𝑎_{0}, \dots, 𝑎_{𝑛} \in {𝑎_{0}, \dots, 𝑎_{𝑛}}$ are true propositions

Specifically, a single-element set $𝑎 \in {𝑎}$

define $𝐴 \subset 𝐵 ≔ \forall 𝑎 \in 𝐴, 𝑎 \in 𝐵$

equivalent_(tag) $⟺$

Some equivalent uses. For computer data, it can be proved by exhaustion that the following calculation results are equal

\begin{matrix} \neg (\neg 𝑝) & ⟺ & 𝑝 \\ \neg (𝑝 \land 𝑞) & ⟺ & (\neg 𝑝) \lor (\neg 𝑞) \end{matrix}

Similarly, in order to represent the case of "infinite elements", define language expansion or specify language transformation. For example, De Morgan law of infinite elements

\begin{matrix} \neg (\underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎)) & ⟺ & \underset{𝑎 \in 𝐴}{⋁} \neg 𝑝 (𝑎) \\ or \neg (\forall 𝑎 \in 𝐴, 𝑝 (𝑎)) & ⟺ & \exists 𝑎 \in 𝐴, \neg 𝑝 (𝑎) \end{matrix}

The concept of "infinity" is limited by using the symbol string $𝑎 \in 𝐴$ of #link(<declare-element-of-set>)[]

formula, proposition is a special data structure in memory. It can be considered that math_object, formula, proposition are the type of programming language

Many propositions are equivalent, so we can consider the "quotient" type of propositions, but the possibility of equivalence is infinite, whether it is possible to have an exhaustive algorithm, first depends on whether it is #link(<countable>)[] …

Similar to the redundancy of $\land, \lor, \neg$ , set theory construction rules may also have redundancy, or there are many equivalent definitions

Specify (finite)

$=$ transitive := $(𝑎 = 𝑏) \land (𝑏 = 𝑐) ⟹ (𝑎 = 𝑐)$

$\Leftrightarrow$ transitive := $(𝑝 \Leftrightarrow 𝑞) \land (𝑞 \Leftrightarrow 𝑟) ⟹ (𝑝 \Leftrightarrow 𝑟)$

follow #link(<bool-algebra>)[various rules of bool in the finite case], define language transformation rules: let $𝑝 (𝑎, 𝑏)$ is formula built with independent/parallel $𝑎, 𝑏$ i.e. independent/parallel in memory read and used by specific cuntion, then

commutative-forall-exists_(tag)

\underset{𝑎 \in 𝐴}{⋀} \underset{𝑏 \in 𝐵}{⋀} 𝑝 (𝑎, 𝑏) ⟺ \underset{𝑏 \in 𝐵}{⋀} \underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎, 𝑏)

same for $⋁$

distributive-forall-exists_(tag)

\underset{𝑎 \in 𝐴}{⋀} \underset{𝑏 \in 𝐵}{⋁} 𝑝 (𝑎, 𝑏) ⟺ \underset{𝑏 \in 𝐵}{⋁} \underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎, 𝑏)

Note that I myself also feel that I cannot completely clearly handle the concepts of derivation and proof below

Natural language example of derivation

If it rains, I won't go out
It's raining
So I won't go out

This example is similar to a conditional branch

rain : bool;
out : bool;
switch (rain) {
  true => out = false,
  false => out = undefined
};

inference_(tag) For mathematical language, that is

The compiler reads the formula $𝑝, 𝑞$
The compiler reads the formula $𝑝 \Rightarrow 𝑞$ is true proposition (may be custom)
The compiler reads the formula $𝑝$ is true proposition
Then the language rule setting is that the compiler, according to this condition (from memory), assigns the bool value of the formula $𝑞$ to true i.e. sets $𝑞$ is true proposition

proof_(tag) The proof is that compiling passes $𝑝 \Rightarrow 𝑞$ is true proposition

Another kind of equivalence $𝑝 \Leftrightarrow 𝑞 ≔ (𝑝 \Rightarrow 𝑞) \land (𝑞 \Rightarrow 𝑝)$

reverse-inference_(tag) Reverse inference. If the result is that I went out, then it is definitely not the result of rain. If the result of the conditional branch is out = true, this is not the result of rain = true. Since the bool value of an ideal binary computer must be one of two, it can only be the result of rain = false. This can be written as a conditional branch

switch (out) {
  true => rain = false,
  false => rain = undefined
};

Mathematically, reverse inference is written as formula $\neg 𝑞 \Rightarrow \neg 𝑝$ , and defined equivalent to $𝑝 \Rightarrow 𝑞$

reverse-proof_(tag) Proof by contradiction is that compiling passes $\neg 𝑝 \Rightarrow \neg 𝑞$ is true proposition

Deductive proof also requires syllogism

All living things die
Humans are living things
Therefore, all humans will die

Where "all living things die" is a specially constructed proposition

syllogism_(tag) Syllogistic reasoning is a language rule

The compiler reads the formula $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎))$ is true proposition (possibly from a definition e.g. #link(<union>)[]))
The compiler reads the declaration let $𝑎^{'} \in 𝐴$ is true proposition
The compiler reads the formula $𝑝 (𝑎^{'})$
Then the compiler sets $𝑝 (𝑎^{'})$ is true proposition according to this condition (from memory)

That is, the compiler implements the specific construction of data (finite) according to the declaration $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎))$ (possibly "infinite")

Or understand it as, this rule and behavior are defining the concept of $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎))$ itself

It is also usually written as the equivalent rule let $𝑎^{'} \in 𝐴$ , then the special inference formula $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎)) ⟹ 𝑝 (𝑎^{'})$ is always true proposition. This form is often used in what #link(<proof>)[previously] said, "proving is compiling passes $𝑝 \Rightarrow 𝑞$ is true proposition"

Reverse syllogism: let $𝑎^{'} \in 𝐴$ , then the equivalent formula $\neg 𝑝 (𝑎^{'}) ⟹ \neg (\forall 𝑎 \in 𝐴, 𝑝 (𝑎)) or \exists 𝑎 \in 𝐴, \neg 𝑝 (𝑎)$ is true proposition

We may never know whether a proposition of bool unknow can be constructively proved, i.e. compiled successfully in a limited number of steps

Where does the target proposition come from? It may be related to a model of the real world

The proof requires expanding a large number of sentences, although computers are very fast at processing strings. In any case, performance optimization? Use only when needed (lazy load)? Parallel (parallel) when two propositions are not interdependent? Assume already proven results (incremental compilation)?

A proposition has many proofs with different runtime data flow, which can be considered to belong to the same quotient proof of this proposition

The following object construction rules, except for the intersection, generally give non-empty sets

union_(tag)

define object $⋃ 𝐴$ and language expansion

\begin{matrix} 𝑥 \in 𝑎 \cup 𝑎^{'} & ≔ & (𝑥 \in 𝑎) \lor (𝑥 \in 𝑎^{'}) \\ 𝑥 \in ⋃ 𝐴 & ≔ & \underset{𝑎 \in 𝐴}{⋁} 𝑥 \in 𝑎 \\ ≔ & \exists 𝑎 \in 𝐴, 𝑥 \in 𝑎 \end{matrix}

is non-emtpy unless $\forall 𝑎 \in 𝐴, 𝑎 = \emptyset$

$𝐴 \cup 𝐴 = 𝐴$

We do not define the union for $𝐴 = \emptyset$ . Same below. The reason is that let $𝑎 \in 𝐴 = \emptyset$ is always a false proposition, which makes many things unusable

sum_(tag)

\begin{matrix} 𝑥 \in 𝑎 ⊔ 𝑎^{'} & ≔ & (𝑥 \in 𝑎) \oplus (𝑥 \in 𝑎^{'}) \\ 𝑥 \in ⨆ 𝐴 & ≔ & ⨁_{𝑎 \in 𝐴} 𝑥 \in 𝑎 \\ ≔ & \exists! 𝑎 \in 𝐴, 𝑥 \in 𝑎 \end{matrix}

is non-emtpy unless $\forall 𝑎 \in 𝐴, 𝑎 = \emptyset$

in finite case, number of element $| ⨁_{1}^{𝑛} 𝐴_{𝑖} | = \sum_{1}^{𝑛} | 𝐴_{𝑖} |$

enum is special case of sum/union?

intersection_(tag)

\begin{matrix} 𝑥 \in 𝑎 \cap 𝑎^{'} & ≔ & (𝑥 \in 𝑎) \land (𝑥 \in 𝑎^{'}) \\ 𝑥 \in ⋂ 𝐴 & ≔ & \underset{𝑎 \in 𝐴}{⋀} 𝑥 \in 𝑎 \\ ≔ & \forall 𝑎 \in 𝐴, 𝑥 \in 𝑎 \end{matrix}

$𝐴 \cap 𝐴 = 𝐴$

product_(tag)

\begin{matrix} 𝑥 \in 𝑎 \times 𝑎^{'} & ≔ & (𝑥 (𝑎) \in 𝑎) \land (𝑥 (𝑎^{'}) \in 𝑎^{'}) \\ 𝑥 \in \prod 𝐴 & ≔ & \underset{𝑎 \in 𝐴}{⋀} 𝑥 (𝑎) \in 𝑎 \\ ≔ & \forall 𝑎 \in 𝐴, 𝑥 (𝑎) \in 𝑎 \end{matrix}

is non-emtpy unless $\exists 𝑎 \in 𝐴, 𝑎 = \emptyset$ (related to axiom-of-choice_(tag) )

Abbreviation $𝐴 \times 𝐴 = 𝐴^{2}$ . in finite case, number of elements $| \prod_{1}^{𝑛} 𝐴_{𝑖} | = \prod_{1}^{𝑛} | 𝐴_{𝑖} |$

$𝑥 (𝑎)$ means reading two symbols as a combined symbol

map_(tag)

let $𝐴, 𝐵$ is math object. The rule for defining map space $𝐴 \to 𝐵$ , map $𝑓$ as math object is

\begin{matrix} 𝑓 \in (𝐴 \to 𝐵) & ≔ & \underset{𝑎 \in 𝐴}{⋀} 𝑓 (𝑎) \in 𝐵 \\ ≔ & \forall 𝑎 \in 𝐴, 𝑓 (𝑎) \in 𝐵 \end{matrix}

denoted by $𝑓 : 𝐴 \to 𝐵$

denoted by $𝑓 \in 𝐵^{𝐴}$ . in finite case, number of elements $| 𝐵^{𝐴} | = | 𝐵 |^{| 𝐴 |}$

Although the usage of $𝑓, 𝑓 (𝑎), 𝑓 (𝑎) \in 𝐵$ seems problematic, they can still be defined in terms of symbol & symbol strings

If we talk about what the map $𝑓$ specifically represents, due to non-concrete constructiveness, there is no specific return like in general programming languages, or what return is a newly defined symbol, math object, language expansion

subset_(tag)

𝑆 \in Subset (𝐴) ≔ 𝑆 \subset 𝐴

denoted by $2^{𝐴}$ . According to #link(<proposition-function>)[] equivalent to map space $𝐴 \to {0, 1}$ . in finite case, number of elements $| 2^{𝐴} | = 2^{| 𝐴 |}$

define $\emptyset \subset 𝐴$ be true proposition

map space and subset introduce high-level infinity

One seemingly counterintuitive thing at first glance is that we seemingly know all $𝑆 \subset ℕ$ or all $𝑓 : ℕ \to ℕ$ , but cannot count them #link(<cardinal-increase>)[] #link(<uncountable>)[]. However, what exactly does "know all $𝑆 \subset ℕ$ " mean? In fact, trying to consider the question of "finding an infinite subset of $ℕ$ in a general way" reveals that this is not simple.

Similarly, although countable can already define some real numbers e.g. $\sum \frac{1}{𝑛!} = 𝑒$ , if not with the help of subset or map, countable construction cannot obtain all $ℝ$

proposition-function_(tag)

let $𝑎 \in 𝐴$ , $𝑝 (𝑎) : 𝐴 \to {0, 1}$ is already constructed

${𝑎 \in 𝐴 : 𝑝 (𝑎)}$ is object

𝑥 \in {𝑎 \in 𝐴 : 𝑝 (𝑎)} ≔ (𝑥 \in 𝐴) \land 𝑝 (𝑥)

define

𝐴 = 𝐵 ≔ (𝑥 \in 𝐴) ⟺ (𝑥 \in 𝐵)

Other usages of $=$

Alias of identifier in memory
Return value of function in memory. so $1 + 1 = 2$ should be understood as the return value of the add function is $2$

hierarchy-order-of-set_(tag)

The set constructed above is called a zero (hierarchy) order set

$𝐴 \in Set$ or $𝐴 \in Set 0$

then let $Set 0$ be math object, in first order set

$Set 0 \in Set 1$

Using object construction rules again, what we get is also defined as belonging to $Set 1$

Anyway, we can always construct such a language with types and bool and various rules in the compiler. Although there are compilers for compilers, the number of compiler layers can also be infinite …

let $Set 1$ be math object, $Set 1 \in Set 2$ . And so on …

Example

$Set \times Set \in Set 1$
$(Set \to Set) \in Set 1$
$Group \in Set 1$
$\begin{matrix} (𝐺, 𝑚) \in Group ≔ \\ 𝐺 \in Set \\ 𝑚 \in Set \\ property-group-multiplication (𝐺, 𝑚) \\ (e.g. 𝑚 \in (𝐺^{2} \to 𝐺)) \end{matrix}$
Can be divided into multiple sentences, so that it is convenient to add/remove properties to get different structs

$Set 0, Set 1, \dots$ looks like the set of natural numbers $ℕ$ , so should we assume a new hierarchy $Set ℕ$ again? Then for $Set ℕ$ , continue to use the object construct rule …

Will the above construction rules lead to contradictions or computer deadlocks?

If we keep constructing infinitely, does this language have an end?

universal-set_(tag)

Does there exist a "set of every set", a "universal set", a "universal-type"?

Defined using set theory rules

𝐴 ≔ {𝑥 \in universal-set : \neg (𝑥 \in 𝑥)} \in universal-set

Then let the compiler calculate the bool of the proposition $𝐴 \in 𝐴$ . Since $𝐴 \in universal-set$ = true, the compiler only calculates the bool of $\neg (𝐴 \in 𝐴)$ , and then discovers the not function, so it calculates the bool inside not, but this returns to calculating the bool of $𝐴 \in 𝐴$ . The compiler may choose to enter a circuit dead loop.

For finite sets, $𝑥 \notin 𝑥$ or cannot be judged, e.g. ${1} \notin {1}$ , because $1 \neq {1}$ , or there is no definition that $𝑥 \in 1$ is a true proposition.

Related to self-referential paradox. Example "This sentence is wrong" gives a computer dead loop

this_sentence_is_false : bool = false;
loop:
  switch (this_sentence_is_false) {
    false => this_sentence_is_false = true,
    true => this_sentence_is_false = false
  } 
  goto loop
};

Or use layering to bypass the self-referential paradox (this_sentence = false) = true. We consider them to be different sentences and judgments, believing that it cannot be self-referential.

If we can count a number, we consider it a natural number.

If language rules can be written and language objects constructed in a finite number of steps, we consider it constructible and expressible. For set theory, what can be constructed in such a finite number of steps is called a math object.

Regarding the problem of infinite natural numbers, if natural numbers are defined by counting or induction or periodic circuits, then the problem of infinity is pushed to infinite time.

For set theory language, assume that universal-set or universal-type leads to the construction of something that causes the circuit to enter an infinite loop.

dependent-distributive_(tag)

union & interset

⋂_{𝑎 \in 𝐴} ⋃_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = ⋃_{𝑥 \in \prod 𝐴} ⋂_{𝑎 \in 𝐴} 𝑥 (𝑎)

⋃_{𝑎 \in 𝐴} ⋂_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = ⋂_{𝑥 \in \prod 𝐴} ⋃_{𝑎 \in 𝐴} 𝑥 (𝑎)

sum and product

\prod_{𝑎 \in 𝐴} ⨆_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = ⨆_{𝑥 \in \prod 𝐴} \prod_{𝑎 \in 𝐴} 𝑥 (𝑎)

⨆_{𝑎 \in 𝐴} \prod_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = \prod_{𝑥 \in \prod 𝐴} ⨆_{𝑎 \in 𝐴} 𝑥 (𝑎)

draft of proof: expand, use parallel distributive cf. #link(<distributive-forall-exists>)[]

set-minus_(tag)

$𝐴 ∖ 𝐵 ≔ {𝑥 \in 𝐴 : 𝑥 \notin 𝐵}$ . if $𝐵 \subset 𝐴$ then define $𝐵^{∁} ≔ 𝐴 ∖ 𝐵$

symmetric-set-minus_(tag)

$𝐴 Δ 𝐵 ≔ (𝐴 ∖ 𝐵) ⊔ (𝐵 ∖ 𝐴) = (𝐴 \cup 𝐵) ∖ (𝐴 \cap 𝐵)$

coordinate-component_(tag)

product component
$(\begin{matrix} \prod 𝐴 & ⟶ & 𝑎 \\ 𝑥 & ⟿ & 𝑥 (𝑎) \end{matrix})$
sum component
$\begin{matrix} 𝑎 & ⟶ & ⨆ 𝐴 \\ 𝑥 & ⟿ & 𝑥 (𝑎) \end{matrix}$