Hello, On Thu, 6 Feb 2003, Prof. Peter Johnstone wrote:
I'd like to know the answer to this too. Why does *everyone*, in writing down the definition of a PCA, include the assumption that Sxy is always defined? As far as I can see, the only answer is "because everyone else does so"; the condition is never used in the construction of realizability toposes, or in establishing any of their properties. In every case where you need to know that a particular term Sab is defined, it's easy to find a particular c such that Sabc is provably defined.
I'd like to vehemently contradict the claim that the condition "sab is always defined" is never used in the construction of realizability toposes. In the paper "Modified Realizability Toposes and Strong Normalization Proofs (Extended Abstract)" by Martin Hyland and Luke Ong, a weaker notion of combinatory algebra, called "conditionally partial combinatory algebra c-pca)", in which the requirement in question is actually dropped, is thoroughly examined. The axioms for a c-pca are that (K) kxy = y (S) sxyz ~= xz(yz) where by "~=" I mean Kleene-equality (i.e. the r.h.s. is defined iff the l.h.s. is defined in which case they are equal). It is not required for a c-pca that "sxy" exists, but if z exists such that xz(yz) exists then sxyz and hence sxy exists by the axiom (S). The motivation for introducing the notion of a c-pca in the paper is that there is a very relevant c-pca which is not a pca. It consists of strongly normalizing lambda terms modulo closed beta equivalence and can be used for providing a categorical point of view on the "candidates of reducibility" method for strong normalization proof. It is shown in the paper that the standard realizability tripos construction will fail to actually deliver a tripos: The set of subsets of the c-pca taken as the set of truth-values won't even model minimal logic, which is why a "modified realizability topos" construction is used in the paper. So there is a strong reason for stipulating the existence of sxy. One relaxation of the notion of pca which won't break the usual constructions but is nevertheless rarely employed (exception is e.g. Longley's work) is the following: instead of sxyx ~= xz(yz) one might merely require sxyz ~> xz(yz), i.e., sxyz is allowed to be more defined than xz(yz). However, I don't know of any interesting models which do not satisfy (S) with Kleene equality anyway. Respectfully yours, Peter Lietz