  $K$ denotes both the predicate satisfied by every currently known theorem and
the finite set of all currently known theorems. The set $K$ is time-dependent,
publicly available, and contains theorems both from formal and constructive
mathematics. Any theorem of any mathematician from past or present forever
belongs to $K$. Mathematical statements with known constructive proofs exist in
$K$ separately and form the set $K_{\textstyle c} \subseteq 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. Paul Cohen proved in $1963$ that the equality $2^{\aleph_0}=\aleph_1$
is independent of $ZFC$. Before $1963$, the statement "There is a
constructively defined integer $n \geq 1$ such that $2^{\aleph_0}=\aleph_n$"
was outside $K$. Since $1963$, this statement is outside $K$ forever.
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$. 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 mathematical statement depends on
time, where the statement is formally stated in the classical mathematics
without the predicate $K$. In this article, mathematical statements on
decidable sets $X \subseteq {\mathbb N}$ refer to time because they refer to
the current mathematical knowledge on $X$. They cannot be formally stated in
the classical mathematics without the predicate $K$ and their logical values
may change in time.
