Is iszero of the untyped lambda calculus sound and complete? I am using the following definitions in the notation of Haskell. In case it matters, I would like to use only the $\alpha,\beta,\eta$ reductions rather than the Haskell evaluation rules.

-- boolean constants
true = \x y -&gt; x
false = \x y -&gt; y

-- 0 and increment (successor)
zero = \f x -&gt; x
inc n = \f x -&gt; f (n f x)

-- IS THIS iszero SOUND AND COMPLETE?
iszero = \n -&gt; n (\x -&gt; false) true


It seems to me that iszero needs to check if two functions are identical. Since the equivalence of two arbitrary Turing Machines are undecidable, I am wondering if the it really works. In particular,


Soundness: are all functions for which iszero returns true really zero?
Completeness: for any arbitrary function $f$, can iszero correctly determine if $f$ is equal zero?
No, iszero does not have to test whether two functions are equal. It only has to detect a difference between them, i.e., extract enough information to tell whether the given function represents a 0 or not.

You could ask the same question about equality testing. It is possible to implement an equality test eq for numbers (exercise, but implement predecessor first). Isn't it the case that eq is comparing functions for equality? No. First of all, eq does not compare arbitrary functions but only those that happen to encode numbers. Second, even when comparing two function n and m that encode numbers, it does not answer the question "are n and m equal function?" but rather "do n and m encode the same number?" These are two different questions.