The Creating Subject

Originally CREAT.SUB[PC,RWW] 1973-12-09
A work in progress

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 our desirem to 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' a computerm use and provide meaningful responses to their 'needs'.

Brouwer introduced the notion of the creating subject. Think of the creating subject as a person involved in the process of thinking. We formalize this idea by imagining 1) that an individual always reasons relatative to some particular [context], where eery [context] has only a finite number of [fact]s, the ones it accepts as true in that [context].

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

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

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

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

is unlikely to be 'true' in some other [context]. We do not accept that there
is a uncontextualized place where [wff]s are meaningful without referem\nce
to a well definded [language] and aren.t associated with a [justification]
for being asserted. [context]s contain [fact]s which not only include a [wff]s
but also have other information (eg s [justification], which explains why
a [fact] is included in its [context]).

The Kriesel axions for a CS assert the if the CS knows A at time n then A 
is true now and fot all future times

(3)		(Prf(n,A) and m>n) then P(m,A)

ie, for a CS trueh, once extablished, is forever true and it will never be
forgotten.

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

kreisel informal rigour and completeness