作者: Douglas Bridges , Hajime Ishihara , Bas Spitters
DOI: 10.1016/S0019-3577(02)80024-6
关键词:
摘要: 1 Department of Mathematics & Statistics, University Canterbury, Private Bag 4800, Christchurch, New Zeeland, e-mail: d. bridges@math, canterbury, ac. nz 2 School Information Science, Japan Advanced Institute Science and Technology, Tatsunokuchi, Ishikawa 923-12, Japan, ishihara@jaist.ac.jp 3 Computer Nijmegen, the Netherlands spitters@cs.kun.nl Communicated by Prof. A.S. Troelstra at meeting September 30, 2002 In this paper we consider following question: given a linear operator 4 on Hilbert space, can compute projection closure its range? Instead making notion computation precise, use Bishop's in- formal approach [1], in which 'there exists' is interpreted strictly as 'we compute'. It turns out that reasoning to capture interpretation be described intuitionistic logic. This logic differs from classical not recognising certain principles, such scheme 'P or P', generally valid. Since do adopt axioms are classically false, all our theorems acceptable mathematics. To answer initial question affirmatively, it enough show range ran(T) T space H located - is,