Paradox

I discovered a paradox in the version of lambda logic that I am creating. It is not difficult to fix. However, I'll explain the paradox before I explain how I fixed it.

Here it is symbolically (or rather, semisymbolically, because I'm not using any math rendering):

L = lambda x . (x x)
H = lambda x . exists y . output((x x), y)
I = lambda x . (H x (L L) 1)

With these definitions, the expression (H I) is paradoxical. I'll explain why.

The first important thing is that I am treating an existential statement as if it were a function that returned true or false. In lambda logic (the official version), this is allowed:

True = lambda x y . x
False = lambda x y . y

So, True is a function that takes 2 arguments and returns the first, while False takes two and returns the second. This should be thought of in terms of if/then/else statements. We can make triples (a b c), and if a evaluates to True, b is returned (the "then" clause); but if a turns out false, then c gets returned.

I define L for convenience. L takes an input, x, and returns x applied to itself. The compound statement (L L) is an infinite loop in lambda calculus: it takes L and applies it to itself, resulting in (L L) again. This isn't paradoxical in itself, because the logic does not assume that a result exists for every computation.

The second term, H, takes a term and detects whether it has a result when applied to itself. That is the meaning of "exists y . output((x x), y)": there exists an output of (x x). (I could have used the L construct, writing (L x) instead of (x x), but that wouldn't be any shorter, would it?) So, the way to read (H x) is "x outputs something when handed itself as input".

I is what I call the switch operation. If F is a function that returns some result (when applied to itself), then (I F) doesn't return anything. If F doesn't, (I F) does. How does it work? Well, I is written in the if-then-else format. The "if" part is the "H x", meaning "x returns something when applied to itself". The "then" part is (L L), a statement that never returns anything. The "else" is just 1, a number. Any concrete thing could be put in this spot; it just gives the function something definite to return.

Now, the paradox comes when we consider (H I). This expression asks the question, "Does the switch operation return anything when applied to itself?" Either it does or it doesn't. If it does, then (because it is the switch operator), it doesn't. If it doesn't, then it does. Contradiction. Paradox.

The problem is that I am allowing lambda-terms to be formed with non-computable elements inside them (such as the existential statement inside H). To avoid the paradox, but preserve the ability to represent any statement on the arithmetical hierarchy, I should restrict the formation of lambda terms. A set of computable basic functions should be defined. The list could include numerical equality, addition, subtraction, multiplication, exponent, et cetera. (Any operation that takes nonnegative integers and returns nonnegative integers.) However, it is sufficient to include only the function F(x), where F(x)=x+1. (Everything else can be developed from this, using lambda calculus.) Also-- it should be understood that the terms that can be created (from these basic computable terms plus lambda) are all the entities that exist within the logic. So, if the logic says things like "exists y . output((x x), y)", it should be understood that the "y" that exists is one of these terms.

Now, why doesn't the official version of lambda logic need to avoid throwing existential statements inside lambda expressions? The reason is that strong predicate I use, "output(x, y)", that means "y is the result of evaluating x". Lambda logic proper only uses a function that represents the performance of a single computational step. If I try to define H, I get a statement that always evaluates to True, because there is always a result of performing a single computational step.