Scott's models and illative combinatory logic.

Martin W. Bunder · Notre Dame Journal of Formal Logic · 1979

Scott's model Φoo for pure combinatory logic (see [8]) satisfies all these properties, but his graph model in [10] does not satisfy (77) (or (ζ)), (ξ) is satisfied but Scott seems to have some doubt about it. In [7] where Kleene sets up a formal system in which intuitionistic mathematics can be developed, (ξ) and (77) are not used. Kleene defines λuX only if X is a te rm, λuX is then a functor (which is not a term). In his formal system equality is defined only over terms so that (ξ) and (77) are meaningless.

Read the paper · More papers on PaperTik