Originally CREAT.SUB[PC,RWW]  1973-12-09

THE CREATING SUBJECT

This note reinterprets some of ideas of Brouwer about what he called
the 'creating subject'.  We think that his basic intuition (ha ha) was
right but in light of our current thinking he actually underestimates
its power.  To be clear he developed these ideas before there were 
actual computers and the desiremto actually use them to build
'understanding systems' was largely beyond any practical thought.

Today this idea is commonplace both in academic settings and companies,
who are trying to provide products that can 'understand' the nature a
computermuser and use this knowledge to provide responses more useful
to a users 'needs'.

Brouwer introduced the notion of the creating subject.  Think of them
as a person involved in the process of thinking.  We formalize this 
by saying that an individual alwats reasons relatative to a particular
[context].  Every [context] has only a finite number of [fact]s so in a
[context] we have 

We introduce the predicate FACT-OF(f,c) meaning that f is a [fact] of
the [context] c.  Note there is an obvious reconizer for FACT-OF, ie it
is decidable in the traditional senes.  So 

(1)		(OR (FACT-OF f c) (NOT (FACT-OF f c)))

Thus at any time our creative subject(CS) can 'assert' (wff-of f) or not
(relatative to c).  Unlike Brower for us

(2i)		(IF (FACT-OFf f c) THEN (wff-of f)) 

is unlikely to be 'true'=because for us , ie a 'consequences' of c, in our
thinking the best we can do is

(2)		(IF (FACT-OFf f c) THEN (FACT-OF f C)) 

which is obvious. We do not accept that there is a uncontextualized place
where [wff]s don't require both a well definded [language] and a reason for
being asserted.  [context]s contain [fact]s which nat only include a [wff]s
but also have other information (eg s [justification], which explains why
a [fact] is included in its [context]).

nd 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)) ) ) )