relation between $\forall$ and implication in intuitionistic logic using curry-howard and propositions as types

Question

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}$.

Answer 1

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$.

Answer 2

It seems that your primary issue is that the way the operators are rendered in the setting of higher order type theory and higher order logic seems a bit forced and conflationary. I tend to agree.

An extension of Curry-Howard that stays entirely within first order logic will use natural bijections on indexed categories. I lay out the general framework for including all the usual connectives here in my reply to Categorical semantics explained – what is an interpretation?, where quantifiers are treated with natural bijections involving indexed categories.

In particular, if $𝐗$ denotes a category, then $|𝐗|$ denotes its set (or class) of objects, and for each $A, B ∈ |𝐗|$, $𝐗(A, B)$ is set of morphisms $f: A → B$. So, if $𝐋$ is the Logic category, then included in it would be such natural bijections as $$ 𝐋(C, ⊤) ⇔ 1(0,0) = \{1_0\},\quad C ∈ |𝐋|\\ 𝐋(C, A ∧ B) ⇔ 𝐋(C, A) × 𝐋(C, B),\quad A, B, C ∈ |𝐋|\\ 𝐋(C, A ⊃ B) ⇔ 𝐋(C ∧ A, B),\quad A, B, C ∈ |𝐋|\\ 𝐋(C, ∀A) ⇔ 𝐋^T(K_TC, A),\quad A, C ∈ |𝐋| $$ where the category $1$ has $|1| = \{0\}$ and $1(0,0) = \{1_0\}$. This involves the product of categories (used for $A ∧ B$) and indexed categories (used for $∀A$). The universal quantifier is then re-conned into this by equating $(∀x:T)A(x)$ with $∀[x:T ↦ A(x)]$, i.e. with $∀[(λx:T)A(x)]$. I define the notation for $𝐋^T$ in the linked reply.

In this formulation, $T$ is just a set. For instance, it could be the set of terms, or it could denote a sort, if you're using a many-sorted logic.

As was pointed out to me (by another reply in that thread), I actually had to make a minor change to the treatment for the universal quantifier. The natural bijection for the universal quantifier I had in the original reply was: $𝐋(C, ∀A) ⇔ 𝐋^T(C, A)$; but $C ∉ |𝐋^T|$. Rather, $C ∈ |𝐋|$ has to be injected into $|𝐋^T|$ by the map $K_T: C ∈ |𝐋| ↦ K_T C ∈ |𝐋^T|$ (as the constant function that takes $t ∈ T$ and yields $C ∈ |𝐋|$).

This embodies the rule that $C ⊦ (∀x:T)A(x)$ if and only if $C ⊦ A(t)$, for all $t:T$, provided that $C$ is "constant in $x$" (i.e. independent of $x$).

Similar treatments apply to the dual connectives and their natural bijections are listed here for completeness: $$ 𝐋(⊥, D) ⇔ 1(0,0) = \{1_0\},\quad D ∈ |𝐋|\\ 𝐋(A ∨ B, D) ⇔ 𝐋(A, D) × 𝐋(B, D),\quad A, B, D ∈ |𝐋|\\ 𝐋(A ⊂ B, D) ⇔ 𝐋(A, B ∨ D),\quad A, B, D ∈ |𝐋|\\ 𝐋(∃B, D) ⇔ 𝐋^T(B, K_TD),\quad B, D ∈ |𝐋| $$ and a similar convention is adopted for the extential quantifier, equating $(∃x:T)B(x)$ with $∃[x:T ↦ B(x)]$, or just $∃[(λx:T)A(x)]$, if you will.

This embodies the similar rule that $(∃x:T)B(x) ⊦ D$ if and only if $B(t) ⊦ D$, for all $t:T$, provided that $D$ is "constant in $x$".

As I noted in the linked reply, the requirement that each of these be a natural bijection tow-ropes a bundle of operators and equational identities (a.k.a. commutative diagrams) ... but does so in a standard way, rather than by ad hoc impositions.

There are arguments for using higher order logic and higher order type theory. It provides a more direct cover for the way mathematics is normally expressed in the literature and things that can be proven in a few lines may require the size of the universe in spatial storage and massive tree-carnage in paper requirements to do the equivalent of in first order logic. Strictly speaking, however, it isn't part of the Curry-Howard correspondence, but is an independent development stemming largely from de Bruijn and the AutoMath project, and de Bruijn's discovery was independent of that of Curry and Howard (and Lambek). The two lines of development are often confused with one another, but they are separate, though parallel, lines.

The issue of "coherence" also arises: a category or sub-category $𝐗$ may be called coherent if $𝐗(A,B)$ has either 0 or 1 elements in it, so that from $f: A → B$ and $g: A → B$, one infers $f = g$. Depending on what combinations of connectives, in the list above, that you include, you may get "coherence"; but I don't see that as a problem. There are other ways to fit predicate logic into Curry-Howard that seem to evade this issue: using the idea of "continuations" (Curry-Howard With Predicate Logic And Continuations). I don't know if the method, described above, for handling quantifiers can be grafted onto this.