3
$\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$

2 Answers 2

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$
5
  • $\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, 2016 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, 2016 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, 2016 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, 2016 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, 2016 at 16:41
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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