부산대학교 도서관

Summary: ``One of the differences between Brouwerian intuitionisticlogic and classical logic is their treatment of time. In classicallogic truth is atemporal, whereas in intuitionistic logic it istime-relative. Thus, in intuitionistic logic it is possible to acquirenew knowledge as time progresses, whereas the classical Law of ExcludedMiddle (LEM) is essentially flattening the notion of time stating thatit is possible to decide whether or not some knowledge will {\it ever}be acquired. This paper demonstrates that, nonetheless, the twoapproaches are not necessarily incompatible by introducing anintuitionistic type theory along with a Beth-like model for it thatprovide some middle ground. On one hand they incorporate a notion ofprogressing time and include evolving mathematical entities in the formof choice sequences, and on the other hand they are consistent with avariant of the classical LEM. Accordingly, this new type theoryprovides the basis for a more classically inclined Brouwerianintuitionistic type theory.''