
THE CREATIVE SUBJECT
This note looks at some of the consequences of considering functions
to be considered well defined if their value at successive integers is
empirically determined.
In computing science these functions appear all the time. For example
consider an operating system. Define f(n) to be 1 if at clocktick n the
null job is running, 0 otherwise. (I assume the clock is ticking even if
the machine is down.) Does this process define a function? What would
a mathematics based on the existance of such functions look like?
Such functions have been considered in the literature of intuitionism
and the discussion below is based on that.
Brouwer introduced the notion of the creative subject. Think of him
as a man involved in thinking. We introduce the predicate Prf(n,A).
Prf(n,A) is interpreted as meaning that at time n the creative subject
enough evidence to assert A. Some evident properties of Prf are:
(1) Prf(n,A) or (not Prf(n,A))
At any time n it is decidable if the creative subject(CS) can assert A
or not.
(2) (exist n Prf(n,A)) then A
If CS can assert A at time n then A is true.
(3) (Prf(n,A) and m>n) then P(m,A)
CS never forgets.
(4) (A then (exists n Prf(n,A))
This says that if A is true then eventually CS will have enough evidence
to assert it. This principle would imply A ≡ ∃n.Prf(n,A) and might seem
rather doubtful. In that case replace it by
(5) A then (not (not (exists n Prf(n,A))))
This means that it is absurd to suppose that CS could find enough
evidence to assert that he could never find a proof of A, if A is true.
(exists alpha (forall x (alpha(x)=0 or (exist x (alpha(x)=1)) ) ) )