Partial function theory, L′
Jonathan Chapman, Frederick Rowbottom · 1992
Abstract L’ is a conservative extension of the (canonical) local set theory L for a topos S (described in Section 2.12), to include symbols for partial functions in S. Beeson (1980/81, 1985, pp. 97—9), has (independently) considered a comparable first-order theory. Taking on board partial function symbols presents problems like those considered by Scott (1979), where he discusses a formulation of intuitionistic logic taking into account partially defined elements. L’ will be contrasted with this formulation. For more information on Scott’s approach, see Grayson (1978) where the set theory is developed in an abstract setting; Fourman and Scott (1979) for interpretation over a complete Heyting algebra; Fourman (1977) for the interpretation in an arbitrary topos. While Scott’s system has partial function symbols via descriptions, its interpretation in a topos is relatively complicated.