Constructive mathematics with the predicate of the current mathematical knowledge

Apoloniusz Tyszka

Apoloniusz Tyszka

Feb 2024

0被引用

0笔记

摘要原文

We assume that the current mathematical knowledge $K$ is a finite set of statements from both formal and constructive mathematics, which is time-dependent and publicly available. Any formal theorem of any mathematician from past or present forever belongs to $K$. We assume that mathematical sets are atemporal entities. They exist formally in $ZFC$ theory although their properties can be time-dependent (when they depend on $K$) or informal. The true statement "$K$ is non-empty" is outside $K$ because $K$ is not a formal set. In constructive mathematics and the traditional Brouwerian intuitionism, the truth of a mathematical statement means that we know a constructive proof. Therefore, the truth of a statement depends on time, but the statement does not refer to time. Thus, every statement in $K$ does not refer to time. Paul Cohen proved in $1963$ that the equality $2^{\aleph_0}=\aleph_1$ is independent of $ZFC$. Before $1963$, the false statement "There is a known constructively defined integer $n \geq 1$ such that $2^{\aleph_0}=\aleph_n$" was outside $K$. Since $1963$, this statement is outside $K$ forever. The true statement "There exists a set $X \subseteq \{1,\ldots,49\}$ such that ${\rm card}(X)=6$ and $X$ never occurred as the winning six numbers in the Polish Lotto lottery" refers to the current non-mathematical knowledge and is outside $K$. Algorithms always terminate. We explain the distinction between algorithms whose existence is provable in $ZFC$ and constructively defined algorithms which are currently known. By using this distinction, we obtain non-trivially true statements on decidable sets $X \subseteq {\mathbb N}$ that belong to constructive and informal mathematics and refer to the current mathematical knowledge on $X$.