On the Wikipedia page for Fixed Point Combinators is written the rather mysterious text
The Y combinator is an example of what makes the Lambda calculus inconsistent. So it should be regarded with suspicion. However it is safe to consider the Y combinator when defined in mathematic logic only.
Have I entered into some sort of spy novel? What in the world is meant by the statements that $\lambda$-calculus is "inconsistent" and that it should be "regarded with suspicion"?
It's inspired from real events, but the way it's stated is barely recognizable and “should be regarded with suspicion” is nonsense.
Consistency has a precise meaning in logic: a consistent theory is one where not all statements can be proved. In classical logic, this is equivalent to the absence of a contradiction, i.e. a theory is inconsistent if and only if there is a statement $A$ such that the theory proves both $A$ and its negation $\neg A$.
So what does this mean regarding the lambda calculus? Nothing. The lambda calculus is a rewriting system, not a logical theory.
It is possible to view the lambda calculus in relation to logic. Regard variables as representing a hypothesis in a proof, lambda abstractions as proofs under a certain hypothesis (represented by the variable), and application as putting together a conditional proof and proof of the hypothesis. Then the beta rule corresponds to simplifying a proof by applying modus ponens, a fundamental principle of logic.
This, however, only works if the conditional proof is combined with a proof of the right hypothesis. If you have a conditional proof that assumes $n=3$ and you also have a proof of $n=2$, you can't combine them together. If you want to make this interpretation of the lambda calculus work, you need to add a constraint that only proofs of the proper hypothesis get applied to conditional proofs. This is called a type system, and the constraint is the typing rule that says that when you pass an argument to a function, the type of the argument must match the parameter type of the function.
The Curry-Howard correspondence is a parallel between typed calculi and proof systems.
A typed calculus that has a fixed point combinator such as $Y$ allows building a term of any type (try evaluating $Y (\lambda x.x)$), so if you take the logical interpretation through the Curry-Howard correspondence, you get an inconsistent theory. See Does the Y combinator contradict the Curry-Howard correspondence? for more details.
This is not meaningful for the pure lambda calculus, i.e. for the lambda calculus without types.
In many typed calculi, it's impossible to define a fixed point combinator. Those typed calculi are useful with respect to their logical interpretation, but not as a basis for a Turing-complete programming language. In some typed calculi, it's possible to define a fixed point combinator. Those typed calculi are useful as a basis for a Turing-complete programming language, but not with respect to their logical interpretation.
In conclusion:
true and false, and propositions were things that had boolean valued output. (and were only considered propositions on the domain of things where it does output a boolean value).
$\endgroup$
I'd like to add one to what @Giles said.
The Curry-Howard correspondence makes a parallel between $\lambda$-terms (more specifically, the types of $\lambda$-terms) and proof systems.
For example, $\lambda x.\lambda y.x$ has type $a \to (b \to a)$ (where $a \to b$ means "function from $a$ to $b$"), which corresponds to the logical statement $a \implies (b \implies a)$. The function $\lambda x.\lambda y.xy$ has type $(a \to b) \to (a \to b)$, corresponding to $(a \implies b) \implies (a \implies b)$. We can convert any lambda-calculus type to a logical tautology by, in a sense, "pattern matching" on functions.
The problem arises when we consider the Y combinator, defined as $\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$. The issue arises because we expect the Y combinator, as a "fix-point" combinator, to have type $(a \to a) \to a$ (because it takes a function from a type to that same type, and finds a fixed-point for that function, which has that type). Converting this to a logical statement yields $(a \implies a) \implies a$. This is a contradiction:
$$(a \implies a) \implies a \\ \top \implies a \\ a \\(\neg a \implies \neg a) \implies (\neg a) \\ \top \implies \neg a \\ \neg a$$
Accepting $(a \to a) \to a$ in a type system leads to the type system being inconsistent. This means we can either
fix. You can just assert that there is a constant $\mathsf{fix}_A$ for each type $A$. That will already give you an inconsistent system as far as CH is concerned, as it would imply every type is inhabited by $\mathsf{fix}(\lambda x.x)$. You could additionally add $\delta$-rules to make $\mathsf{fix}$ compute, and that would turn, say, the STLC with naturals into a Turing-complete system, but you don't have to add these computational rules, and the system would still be inconsistent.
$\endgroup$
Commented
Mar 28, 2019 at 5:35