Quoting Peter Lietz <lietz@mathematik.tu-darmstadt.de>:
1.) Let A be a c-pca. If I understand correctly, you say that the indexed poset that maps a set I to the set of maps from I to P(A), endowed with the usual entailment relation
Not quite - you have to define the entailment relation to match the definition of implication (put a k in there!). The cheating way to see that all this must work out is of course via the equivalence to a PCA for which the standard construction works!
2.) Given a c-pca A, you say that A equipped with the application function a.b := akb is a (proper) pca. What exactly would be a good S combinator for the new algebra ?
Note that we can find elements if,true,false \in A satisfying if true x y = x, if false x y = y, and furthermore we can arrange that true = k. (I'll use "if then else" syntax below). We want to construct S such that (in A), Skxkykz ~ (xkz)k(ykz), and Skxky is always defined. Take S to be \lambda txuyvz. if v then (xkz)k(ykz) else false using the usual Curry translation of lambda terms. To see that Skxky is always defined, note that, provably, Skxky(false)z = false. Clearly there are two versions of this result, one with the axiom sxyz ~ (xz)(yz) and one with sxyz >~ (xz)(yz). Thomas asks whether every PCA with >~ is equivalent to one with ~ (Gordon Plotkin has also asked me this natural question). At the moment, the best I can do is: for any PCA A with >~, there's a PCA B with ~ and an applicative inclusion A -> B (giving rise to a geometric inclusion of toposes). Cheers, John