Are the following lambda-calculus definitions axiomatic?

  • true: $\lambda xy.x$
  • false: $\lambda xy.y$

Is the definition truly arbitrary? In my impression, it looks like we could just swap the definitions for true and false around. Would an alternative definition such as the following one be ok:

  • true: $\lambda xy.y$
  • false: $\lambda xy.x$

Is it possible that "true" is just an arbitrary choice, while "false" then needs to be the opposite of "true" in a certain way?

Would the following definition by outright wrong:

  • true: $\lambda xy.xz$
  • false: $\lambda xy.yz$

If more than one definition for true and false is possible, how could we describe the class of "consistent" definitions for true and false?

  • $\begingroup$ The ability to switch arbitrarily between true and false is used extensively in digital design, read about "active low" logic. $\endgroup$ – DanielV Nov 2 '15 at 6:46

If you swap "true" and "false" you'll have to swap "and" and "or" too. If you having quantifiers you must swap "for all" and "exists" too. Basically this is what De Morgan laws says.

Then you of course has the interpretation of the "truth" that makes swapping something that doesn't work well with our intuitive concepts. You will be using another language that's consistent, but doesn't mean the same as in the language everybody else uses.


You're asking about what is known as Church Encoding. The definitions of true as $\lambda xy.x$ and of false as $\lambda xy.y$ were given in order to be used together with, e.g., the definitions of and as $\lambda x y. x y x$ and of or as $\lambda x y . x x y$.

In this sense they are somewhat arbitrary. If you swap the definitions for $true$ and $false$ you need to do as well for, e.g., the definitions of $or$ and $and$, as @skyking already pointed out.

Observe that for this to work, lambda terms must be considered equivalent under certain reduction procedures. Even so that there are two possible definitions for not, depending on the evaluation strategy used for the lambda terms (as you can see in the link).

I don't think it makes sense to say that some definition is outright wrong; maybe you can say it is not interesting for it lacks some important property. In order to see if the definitions of true and false you mention are adequate, try to define the other logical operators to work with them and see if the whole picture is better suited for your purposes.

  • $\begingroup$ I agree. The problem that I have is rather that I do not understand how to define the set of (true,false) definitions for which it would be possible to produce consistent definitions of the (and,or,not) operators. L = { (true: defTrue,false: defFalse,and: defAnd,or: defOr,not: defNot) } L is the set of tuples representing consistent definitions for (true,false,and,or,not). How can we create a function fL() that will recursively enumerate L? $\endgroup$ – erik Nov 3 '15 at 3:57
  • $\begingroup$ Let's see if I understand. You're seeking a enumeration of all "consistent" definitions (in terms of some lambda calculus) of the logical operators, right? I take you intentionally is not defining what is meant by consistent, maybe in order to arrive at this very notion, right? If that's so, maybe what you're trying to do would be better tackled if you consider all possible definitions - even the inconsistent ones - and try to single out the consistent in some way as the ones that are equivalent (in some sense) to a canonical definition of your choice. $\endgroup$ – Tarc Nov 3 '15 at 17:16
  • $\begingroup$ @user1471399, What I just said has a resemblance with the theory of Gödel Numberings, or admissible numberings, check this: en.wikipedia.org/wiki/Admissible_numbering $\endgroup$ – Tarc Nov 3 '15 at 17:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.