A pillow’s softness, from how it behaves:
To forces it reacts yet it conforms.
The patient repitition of a wave,
Transforming an atom from form to form.
How everything existing had begun,
Matter from matter moving fast away.
How everything is hidden in the sum
Of amplitudes of all the different ways.
Yet all the things I do ’till now express
Are mere fragments of a deeper core.
How would I love to faithfully address
The full wonders with all of their galore.
Yet when I try those feelings to compose
My poetry is hightened into prose.
Monthly Archives: January 2013
Propositions as types in Foundations to Constructive Analysis
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
is an element of
. An element of
consists of a real number
and a positive integer
, such that
, because an element of
is not presented until both
and
are given. One and the same real number
can be associated with two distinct (but equal) elements of
. Nevertheless we shall continue to refer loosely to a positive real number
. On those occasions when we need to refer to an
for which
, we shall take the position that it was there implicitly all along.
In other words, the proposition really stands for the type
of all with
. Bishop does not appear to be aware of the
propositions-as-types interpretation in this book, but he uses it implicitly.