1
$\begingroup$

I am currently trying to wrap my head around intuitionistic logic and its interpretation using the curry-howard isomorphism and propositions as types.

I came about this explained relation between $\forall$ and $\rightarrow$:

A function type $s \rightarrow t$ is actually a function type $\forall x:s.t$ where the variable x does not occur in t. [..] Moreover, if we have a type $\forall x:s.t$ where x does not occur in t, we can omit x and just write $s\rightarrow t$ without losing information.

I do not get how this can work as I understand a $\rightarrow$ basically as "give me a proof of s and I give you a proof of t" - a mapping function. However, a function that maps needs a parameter, in this case the x which is a proof of s : $f(x):s\rightarrow t$. How can I still have a mapping if I am 'not allowed' to use x and thus any information contained in it anymore?

If I use an example: e.g. proof that every $\mathbb{N}$ is $\mathbb{R}$ I need to use the information contained in the proof that a given number is in $\mathbb{N}$ to show that $\mathbb{N}$ is more restrictive than $\mathbb{R}$ and thus any $\mathbb{N}$ has to be $\mathbb{R}$. However, I do not have 'access' to those information as x (the proof that the number is in $\mathbb{N}$) does not occur in my proof that the number is also $\mathbb{R}$.

$\endgroup$
1
$\begingroup$

The difference between $s\to t$ and $\forall x : s. t$ is that in the second case, the return type of the function depends on the input.

For example, in most languages, you can make a function that takes a natural number and returns an array of that size and it will have type $\operatorname{nat} \to \operatorname{nat} \operatorname{array}$. But if you want to specify it further and say that it doesn't return any array but really an array of that size, then you would want to type it as $\forall n :\operatorname{nat}. \{a : \operatorname{nat} \operatorname{array} | \operatorname{size}(a)=n\}$. In both cases the output of the function (the array of size $n$) depends on the input $n$ of the function but in the second case, the return type $\{a : \operatorname{nat} \operatorname{array} | \operatorname{size}(a)=n\}$ also depends on the input while in the first case it does not.

Another example would be a function that takes a proof that $m=2$ and returns a proof that $m\le 2$. All it has to do it use the reflexivity of $\le$, which I'll call $\operatorname{le\_refl}$. You can define $(\lambda (m:\Bbb N).\lambda (p:m=2).\operatorname{le\_refl}(p)):\forall (m:\Bbb N).(m=2\to m\le 2)$. Note that you could also write the type as $\forall (m:\Bbb N).(\forall(p:m=2). m\le 2)$ but since the return type $m\le 2$ of the inner function doesn't depend on the proof $p$ (even though its output does), you can simplify it and use the arrow notation.

Yet another way to think of is that $\forall(x:A).B(x)$ (where I write $B(x)$ instead of $B$ to emphasize that it can depend on $x$) is often written $\Pi(x:A).B(x)$ in type theory. And it makes sense because in a way, this expressions gives you a way to define a type $B$ given $x:A$. And the you look at the set of all functions that take an input $x:A$ and return an element of $B(x)$. Now think of the cartesian $\prod_{x\in A}B(x)$ product of the elements of the set $\{B(x)|x\in A\}$. An element of that is a big tuple indexed by $A$ and if you ask the element in the spot $x\in A$, it gives back an element that's in $B(x)$. So it's the exact same thing. Also note that when you take $B$ to be constant, you get $\prod_{x\in A}B$ which is usually denoted $B^A$ or $A\to B$.

$\endgroup$
  • $\begingroup$ why does the inner function not depend on the proof $p$? Isn't there a dependence as if there would not be a $=$ involved le_refl couldn't be applied? Or do you mean that the exact nature of the proof p is not needed as only the fact that $2 = m$ (the type of the proof) is relevant to be able to use le_ref? So the function does not work on the instance of the proof but the nature/denotation of the proof? $\endgroup$ – Sim Sep 17 '16 at 15:20
  • 1
    $\begingroup$ The output $\operatorname{le\_refl}(p)$ of the inner function $\lambda(p:m=2).\operatorname{le\_refl}(p)$ (which I'll call $f_m$) does depend on the input $p$ but its return type $m\le 2$ does not. On the contrary, the outer function $\lambda(m:\Bbb N).f_m$ has a return type $(m=2\to m\le 2)$ that does depend on the input $m$. $\endgroup$ – xavierm02 Sep 17 '16 at 15:25
  • $\begingroup$ Could you give a counter example with a proof (like m = 2) in which the return type depends on the input. The example you give about this is rather programming than logic. I think such a counter example would be helpful to grasp this distinction in logic. $\endgroup$ – Sim Sep 17 '16 at 15:50
  • $\begingroup$ @Sim : You could have something saying that there is a unique proof. For example $\forall (p:0\le 0), p=\operatorname{le\_n}(0)$ where $\le$ is defined by $\operatorname{le\_n}:\forall (n:\operatorname{nat}). n \le n$ and $\operatorname{le\_S}:\forall (n:\operatorname{nat}). \forall (m:\operatorname{nat}). n \le m \to n \le S m$. $\endgroup$ – xavierm02 Sep 17 '16 at 16:35
  • $\begingroup$ But it's a bit weird. Most of the time, you'll only need $\forall(x:A).B$ when $A$ is a "real" type (and not a proposition). $\endgroup$ – xavierm02 Sep 17 '16 at 16:41

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.