How can types represent both sets and propositions in Lambda calculus?

How do these two interpretations relate to each-other?

Going in the details would require a course in type theory, if you want to deepen your knowledge of the subject you should search reference on the Curry-Howard isomorphism.

An intuitive not too precise explanation of the relation between these interpretations is the following.

Generally to every proposition (not a predicate) can be associated a set: the set of its proofs.

This association has the property that it turns connectives into type formers: if we let $A$ be a proposition and denote with $[A]$ the associated set then we have that $[A \land B]=[A]\times[B]$, $[A \lor B]=[A] \amalg [B]$ and $[A \to B]=[A]\to[B]$.

There is more: the inference rules, that can be regarded as operations between proofs, correspond to special operations of the corresponding types. As an example the inference rules

1. if $p$ is a proof of $A \land B$ then there is a proof $\pi_A(p)$ of the proposition $A$
2. if $p$ is a proof of $A \land B$ then there is a proof $\pi_B(p)$ of the proposition $B$

become the canonical projections $\pi_{[A]} \colon A \times B \to A$ and $\pi_{[B]} \colon A \times B \to B$.

The interesting point is that these sets corresponding to propositions are those freely generated by a set of variables and closing for certain operations (the so called constructors).

So you get this correspondence between the propositions of propositional logic (and relative proofs) and these sets (and their elements), this correspondence turns out to be bijective.

This correspondence can be extended to include predicates by introducing family of sets (i.e. set-valued functions).

This brings us to the next question.

How could the proposition $P[x:=y]$ (i.e. "$y$ is a natural number") be interpreted as a set?

Predicates are not interpreted as sets, since they are not propositions.

A predicate is a family of propositions indexed by its possible arguments: a predicate $P(x)$ is a function that to every value $a$ (that can be assigned to $x$) associates the proposition $P(a)$.

If you get that, it should be obvious that a predicate should be interpreted not as a set but as a family of sets: i.e. a function sending every value of its argument into a set.

If $P(x)$ is a predicate, its interpretation is the function/family $[P(x)]$ defined by the equation $$[P(x)](a) = \text{ the set of proofs of } P(a)$$ that is a set-valued function.

How is nat a proposition in and of itself? And furthermore, how is 3 a "proof" of nat? Is nat equivalent to the proposition "N is non empty", and similarly, is producing an example of a member of N, such as 3, the "proof" of that proposition?

To answer this question one should first specify what is the type system and the logic you are considering here.

The point here is that $\mathbf{nat}$ is a simple type, so it should correspond to a proposition in some logic. The problem is that it does not correspond to any proposition of any common used logic system.

For instance there is no proposition in the propositional logic that correspond to it. That is because $\mathbf{nat}$ does not belong to simply typed lambda calculus (STLC), it belongs to an STLC with natural numbers (an extension of STLC).

You could extend the propositional logic in a way to give a proposition corresponding to $\mathbf{nat}$. This would be an extension of propositional logic with a new constant proposition ($\mathbf{nat}$) with the following inference rules:

• there is a proof of $\mathbf{nat}$ named $0$
• is $n$ is a proof of $\mathbf{nat}$ then there is also another proof of $\mathbf{nat}$ named $n+1$
• if $p$ is a proof of $A$ and if $g$ is a proof of $A \to A$ then there is a proof of $\mathbf{nat}\to A$.

Such logic would not have really useful applications, since usually when applying logic we are interested in finding one proof for a proposition, we do not necessarily need more proof, especially if the new proofs are more complex than the one we already have.

Hope this helps.

P.s. note that the type $\prod x\colon \mathbf{nat}. P(x)$ does not have type $\mathbf{nat} \to *$ but it has type $*$, in the very same way as $\forall x \in \mathbb N. P(x)$ is a proposition not a depending-predicate.