In lambda calculus the fixed point combinator is defined as:
$$Y=\lambda f \cdot(\lambda x \cdot f(x x))(\lambda x \cdot f(x x))$$
It is very easy to see how $Yg =g(Yg)$ for any $g$ by using $\beta$-reduction.
At the same time I wonder what is the meaning of $Yg$ when $g=\lambda x.x+1$, a fuction without fixed point.
I need somebody to explain me that please.
I know that the fixed point combinator is related to the Curry paradox which proves that the lambda calculus as a deductive system is inconsistent. Does this inconsistency has to do with the case I wrote above?
Best Answer
The pure lambda calculus does not have an inbuilt notion of $+$ or $1$. There are various encodings of the natural numbers (and arithmetic) into the lambda calculus though. For example, the Church encoding. In these cases, the arithmetic operations work well on those lambda terms which denote natural numbers, but on the rest of the lambda terms they need not behave in nice ways.
In your case, if $N$ denotes the natural number $n$ in the coding method you have chosen, then $gN$ will reduce to the code of $n+1$ (here I`ve assumed that $g$ is the encoding of the function which sends $x$ to $x+1$ into the lambda calculus). On the other hand, if $M$ is some lambda term which doesn´t denote any natural number in your encoding, then $gM$ could potentially reduce to all sorts of strange things. In particular, $g$ does have fixed points, but these fixed points cannot denote natural numbers in your encoding.