Propositions as types in Foundations to Constructive Analysis

Posted on by

I was reading Foundations of Constructive Analysis by Errett Bishop, and I came across this intersting passage:

It is not strictly correct to say that a real number \{x_n\} is an element of \mathbf{R}^+. An element of \mathbf{R}^+ consists of a real number \{x_n\} and a positive integer n, such that x_n > n^{-1}, because an element of \mathbf{R}^+ is not presented until both \{x_n\} and n are given. One and the same real number \{x_n\} can be associated with two distinct (but equal) elements of \mathbf{R}^+. Nevertheless we shall continue to refer loosely to a positive real number \{x_n\}. On those occasions when we need to refer to an n for which x_n > n^{-1}, we shall take the position that it was there implicitly all along.

In other words, the proposition x \in \mathbf{R}^+ really stands for the type
of all n with x_n > n^{-1}. Bishop does not appear to be aware of the
propositions-as-types interpretation in this book, but he uses it implicitly.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

Gravatar
WordPress.com Logo

You are commenting using your WordPress.com account. ( Log Out / Change )

Twitter picture

You are commenting using your Twitter account. ( Log Out / Change )

Facebook photo

You are commenting using your Facebook account. ( Log Out / Change )

Google+ photo

You are commenting using your Google+ account. ( Log Out / Change )

Cancel

Connecting to %s