Excluded Middle Almost Reasonable.


I almost convinced myself that AA is reasonable. Suppose one had a λ-term of type (A⇒⊥)⇒⊥ (i.e. of type A). What must this λ-term look like? Well, it must return something of type ⊥. Assuming our system is consistent then there is no way to construct ⊥ so it must use the its parameter f of type A⇒⊥ to get a ⊥. Therefore the λ-term must look something like λf:A⇒⊥.fe for some λ-term e of type A. Hence, every time there is a λ-term of type A, there exists (as a sub-expression) a λ-term of type A. One concludes that adding AA as an axiom would be as reasonable as adding the axiom that says that every function is continuous.

The above reasoning is clearly flawed because there is a λ-term of type (((AB)⇒A)⇒A) but there is no λ-term of type ((AB)⇒A)⇒A. The reason is because the (sub-)expression e in the above argument has access to the parameter f. As strange as it may sound, it is possible for the function f to use itself to make the parameter it needs to generate ⊥. This is exactly what happens in the proof of (((AB)⇒A)⇒A).

Suppose one had a function f of type (((AB)⇒A)⇒A)⇒⊥. Because ⊥ implies anything, there is a function g of type ⊥⇒B. Also it is easy to find a function h of type A⇒((AB)⇒A)⇒A. So one can compose these three functions together to get gfh of type AB. Now with this in hand, one can make a function of type ((AB)⇒A)⇒A. One takes a function s of type (AB)⇒A, and applies our composition to it, resulting in s(gfh) of type A.

This is how one can use f to generate a parameter to apply to itself. To get ⊥ from f one can use the λ-term fλs:(AB)⇒A.s(gfh). Notice how f is part of the term being passed into f.

This circularity of passing f into itself isn’t too troubling. There cannot be any functions of type (((AB)⇒A)⇒A)⇒⊥. Indeed that is the very thing being proved.


, ,

Russell O’Connor: contact me