Re: Realizability and Partial Combinatory Algebras

[<jvoosten@math.uu.nl>]

Dear Peter and John,

Peter correctly pointed out the error in my message:
the problem was in the use of the "if then .. else .." syntax,
not in any form of combinatorial completeness.

Answering John: I was using a construction of \lambda x.t where
\lambda x.M is KM whenever M is any term not containing x free
(this works just as well); so in my construction,
\lambda vz. if v then xkzk(ykz) else false
DOES contain subterms xk and yk.

Anyway, I do now believe that John's latest version is correct.
This is really very nice, and a surprise (for me, at least).
I stand corrected and must apologize for my first posting in this
discussion, casting doubt on PTJ's message.

One little point, regarding Combinatorial Completeness. I believe
the following form is valid (in the situation with the weak S-axiom):
suppose t is a term, x a variable. There is a term \lambda x.t such
that for all a,a_1,...,a_n in A:
((\lambda x.t)[a_1,...,a_n])a ~ t[a,a_1,...,a_n]
So this is just like the ordinary form, except for the assertion that
(\lambda x.t)[a_1,...,a_n] is always defined. We have that
(\lambda x.t)[a_1,...,a_n] is defined whenever for some a in A,
t[a,a_1,...,a_n] is defined.

Best, Jaap