lambda calculus, definition of true and false

5.3k Views Asked by At

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?

2

There are 2 best solutions below

0
On

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.

3
On

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.